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.
InSet(InSet(x, Complex), Boolean).prove()
InSet(InSet(x, ComplexNonZero), Boolean).prove()
NotEquals(x, zero).prove(assumptions=[InSet(x, ComplexNonZero)],
conclude_automation=False) # should be side-effect
InSet(x, Complex).prove(assumptions=[InSet(x, ComplexNonZero)])
InSet(x, ComplexNonZero).prove(assumptions=[InSet(x, Complex), NotEquals(x, zero)])
InSet(x, ComplexNonZero).prove(assumptions=[InSet(x, RealNonZero)])
ComplexSet.abs_both_sides_of_equals()
¶Applying absolute value to both sides of an equality.
# some example products of exponentials
a_equals_b = Equals(a, b)
Complex.abs_both_sides_of_equals(
a_equals_b, assumptions=[InSet(a, Complex), InSet(b, Complex), Equals(a, b)])
%end demonstrations