In [1]:

```
import proveit
from proveit import a, b, c, x
from proveit.logic import Boolean, Equals, NotEquals, InSet
from proveit.numbers import zero, Abs, RealNonZero, Complex, ComplexNonZero
%begin demonstrations
```

UNDER CONSTRUCTION. Something here about the importance of having and using specifically pre-defined number sets such as the Complex numbers ($\mathbb{C}$), the axiomatic definition, and perhaps the distinctiveness from other predefined NumberSet classes.

In [2]:

```
InSet(InSet(x, Complex), Boolean).prove()
```

In [3]:

```
InSet(InSet(x, ComplexNonZero), Boolean).prove()
```

In [4]:

```
NotEquals(x, zero).prove(assumptions=[InSet(x, ComplexNonZero)],
conclude_automation=False) # should be side-effect
```

In [5]:

```
InSet(x, Complex).prove(assumptions=[InSet(x, ComplexNonZero)])
```

In [6]:

```
InSet(x, ComplexNonZero).prove(assumptions=[InSet(x, Complex), NotEquals(x, zero)])
```

In [7]:

```
InSet(x, ComplexNonZero).prove(assumptions=[InSet(x, RealNonZero)])
```

`ComplexSet.abs_both_sides_of_equals()`

¶Applying absolute value to both sides of an equality.

In [8]:

```
# some example products of exponentials
a_equals_b = Equals(a, b)
```

In [9]:

```
Complex.abs_both_sides_of_equals(
a_equals_b, assumptions=[InSet(a, Complex), InSet(b, Complex), Equals(a, b)])
```

In [ ]:

```
```

In [10]:

```
%end demonstrations
```