# Demonstrations for the theory of proveit.numbers.number_sets.complex_numbers¶

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


# Complex Numbers $\mathbb{C}$¶

## Introduction ¶

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)

a_equals_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