logo

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(
    theta, Equals(Exp(e, Mult(i, Add(theta, pi))),
                  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]:
complex_polar_radius_negation = Forall(
    (r, theta), Equals(Mult(Neg(r), Exp(e, Mult(i, Add(theta, pi)))),
                       Mult(r, Exp(e, Mult(i, theta)))),
    domain=Real)
complex_polar_radius_negation (conjecture without proof):
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