Theorems (or conjectures) for the theory of proveit.numbers.number_sets.complex_numbers¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import r, x, theta
from proveit.logic import Forall, in_bool, Equals, NotEquals, InSet, Set, ProperSubset
from proveit.numbers import (
zero, two, e, i, pi,
ZeroSet, Natural, NaturalPos,
Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg,
RationalNonPos,
Real, RealNonZero, RealNeg, RealPos, RealNonNeg, RealNonPos,
Complex, ComplexNonZero)
from proveit.numbers import Add, Exp, frac, Mod, Mult, Neg
In [2]:
%begin theorems
Defining theorems for theory 'proveit.numbers.number_sets.complex_numbers'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
zero_is_complex = InSet(zero, Complex)
zero_is_complex (conjecture without proof):

In [4]:
zero_set_within_complex = ProperSubset(ZeroSet, Complex)
zero_set_within_complex (conjecture without proof):

In [5]:
i_is_complex = InSet(i, Complex)
i_is_complex (conjecture without proof):

In [6]:
i_is_complex_nonzero = InSet(i, ComplexNonZero)
i_is_complex_nonzero (conjecture without proof):

In [7]:
nat_within_complex = ProperSubset(Natural, Complex)
nat_within_complex (conjecture without proof):

In [8]:
int_within_complex = ProperSubset(Integer, Complex)
int_within_complex (conjecture without proof):

In [9]:
int_nonpos_within_complex = ProperSubset(IntegerNonPos, Complex)
int_nonpos_within_complex (conjecture without proof):

In [10]:
int_neg_within_complex_nonzero = ProperSubset(IntegerNeg, ComplexNonZero)
int_neg_within_complex_nonzero (conjecture without proof):

In [11]:
nat_pos_within_complex_nonzero = ProperSubset(NaturalPos, ComplexNonZero)
nat_pos_within_complex_nonzero (conjecture without proof):

In [12]:
int_nonzero_within_complex_nonzero = ProperSubset(IntegerNonZero, ComplexNonZero)
int_nonzero_within_complex_nonzero (conjecture without proof):

In [13]:
rational_within_complex = ProperSubset(Rational, Complex)
rational_within_complex (conjecture without proof):

In [14]:
rational_nonneg_within_complex = ProperSubset(RationalNonNeg, Complex)
rational_nonneg_within_complex (conjecture without proof):

In [15]:
rational_nonpos_within_complex = ProperSubset(RationalNonPos, Complex)
rational_nonpos_within_complex (conjecture without proof):

In [16]:
rational_pos_within_complex_nonzero = ProperSubset(RationalNonPos, ComplexNonZero)
rational_pos_within_complex_nonzero (conjecture without proof):

In [17]:
rational_neg_within_complex_nonzero = ProperSubset(RationalNonPos, ComplexNonZero)
rational_neg_within_complex_nonzero (conjecture without proof):

(alternate proof for rational_pos_within_complex_nonzero)
In [18]:
rational_nonzero_within_complex_nonzero = ProperSubset(RationalNonZero, ComplexNonZero)
rational_nonzero_within_complex_nonzero (conjecture without proof):

In [19]:
real_within_complex = ProperSubset(Real, Complex)
real_within_complex (conjecture without proof):

In [20]:
real_nonneg_within_complex = ProperSubset(RealNonNeg, Complex)
real_nonneg_within_complex (conjecture without proof):

In [21]:
real_nonpos_within_complex = ProperSubset(RealNonPos, Complex)
real_nonpos_within_complex (conjecture without proof):

In [22]:
real_pos_within_complex_nonzero = ProperSubset(RealNonPos, ComplexNonZero)
real_pos_within_complex_nonzero (conjecture without proof):

In [23]:
real_neg_within_complex_nonzero = ProperSubset(RealNonPos, ComplexNonZero)
real_neg_within_complex_nonzero (conjecture without proof):

(alternate proof for real_pos_within_complex_nonzero)
In [24]:
real_nonzero_within_complex_nonzero = ProperSubset(RealNonZero, ComplexNonZero)
real_nonzero_within_complex_nonzero (conjecture without proof):

In [25]:
complex_nonzero_within_complex = ProperSubset(ComplexNonZero, Complex)
complex_nonzero_within_complex (conjecture without proof):

In [26]:
nonzero_if_in_complex_nonzero = Forall(
x,
NotEquals(x, zero),
domain=ComplexNonZero)
nonzero_if_in_complex_nonzero (conjecture without proof):

In [27]:
nonzero_complex_is_complex_nonzero = Forall(
x, InSet(x, ComplexNonZero), condition=NotEquals(x, zero),
domain=Complex)
nonzero_complex_is_complex_nonzero (conjecture without proof):

An in_bool theorem, which is accessed by the respective ComplexSet NumberSet to implement its deduce_membership_in_bool() method:

In [28]:
complex_membership_is_bool = Forall(x, in_bool(InSet(x, Complex)))
complex_membership_is_bool (conjecture without proof):

In [29]:
complex_nonzero_membership_is_bool = Forall(x, in_bool(InSet(x, ComplexNonZero)))
complex_nonzero_membership_is_bool (conjecture without proof):

Complex numbers in polar form¶

In [30]:
unit_length_complex_polar_negation = Forall(
Neg(Exp(e, Mult(i, theta)))),
domain=Real)
unit_length_complex_polar_negation (conjecture without proof):

In [31]:
complex_polar_negation = Forall(
(r, theta), Equals(Mult(r, Exp(e, Mult(i, Add(theta, pi)))),
Neg(Mult(r, Exp(e, Mult(i, theta))))),
domain=Real)
complex_polar_negation (conjecture without proof):

In [32]:
(r, theta), Equals(Mult(Neg(r), Exp(e, Mult(i, Add(theta, pi)))),
Mult(r, Exp(e, Mult(i, theta)))),
domain=Real)

In [33]:
exp_2pi_i_x = Forall((x, r), Equals(Exp(e, frac(Mult(two, pi, i, Mod(x, r)), r)),
Exp(e, frac(Mult(two, pi, i, x), r))), domain=Real)
exp_2pi_i_x (conjecture without proof):

In [34]:
exp_neg2pi_i_x = Forall((x, r), Equals(Exp(e, frac(Neg(Mult(two, pi, i, Mod(x, r))), r)),
Exp(e, frac(Neg(Mult(two, pi, i, x)), r))), domain=Real)
exp_neg2pi_i_x (conjecture without proof):

In [35]:
%end theorems
These theorems may now be imported from the theory package: proveit.numbers.number_sets.complex_numbers