# Theorems (or conjectures) for the theory of proveit.numbers.exponentiation¶

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 IndexedVar, ExprRange
from proveit import a, b, c, d, k, m, n, r, x, y, z
from proveit.core_expr_types import a_1_to_m, a_1_to_n, b_1_to_m, k_1_to_m
from proveit.logic import And, Forall, Equals, InSet, NotInSet, NotEquals, Or
from proveit.numbers import (Abs, Add, Exp, frac,  greater, greater_eq, Less,
LessEq, Log, number_ordering, Mult, Neg, sqrt, subtract)
from proveit.numbers import (zero, one, two, three, e, i, ZeroSet, Natural, NaturalPos, Integer,
Rational, RationalPos, RationalNonZero,
Real, RealNonNeg, RealPos, Complex, ComplexNonZero)
from proveit.numbers.exponentiation import (
prod_a_raise_ki__1_to_m, prod_a_raise_bi__1_to_m,
prod_ai_raise_n__1_to_m, prod_ai_raise_b__1_to_m, nonzero_a_1_to_m)

In [2]:
%begin theorems

Defining theorems for theory 'proveit.numbers.exponentiation'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [3]:
exp_nat_pos_expansion = Forall(n, Forall(x, Equals(Exp(x, n), Mult(ExprRange(k, x, one, n))),
domain=Complex),
domain=NaturalPos)

exp_nat_pos_expansion (conjecture without proof):

In [4]:
exp_nat_pos_rev = Forall(n, Forall(x, Equals(Mult(ExprRange(k, x, one, n)), Exp(x, n)),
domain=Complex),
domain=NaturalPos)

exp_nat_pos_rev (conjecture without proof):

### Basic Operation Theorems¶

In [5]:
exponentiated_one = Forall([x], Equals(Exp(one, x), one), domain=Complex)

exponentiated_one (conjecture without proof):

In [6]:
exp_zero_eq_one = Forall([a], Equals(Exp(a, zero), one), domain=Complex)

exp_zero_eq_one (conjecture without proof):

In [7]:
exponentiated_zero = Forall([x], Equals(Exp(zero, x), zero), domain=RealPos)

exponentiated_zero (conjecture without proof):

In [8]:
exp_in_zero_set = Forall((a, b), InSet(Exp(a, b), ZeroSet), domains=(ZeroSet, RealPos))

exp_in_zero_set (conjecture without proof):

In [9]:
exp_rational_non_zero__not_zero = Forall(
[a, b],
NotEquals(Exp(a,b), zero),
domain=RationalNonZero)

exp_rational_non_zero__not_zero (conjecture without proof):

In [10]:
exp_not_eq_zero = Forall(
[a, b],
NotEquals(Exp(a,b), zero),
domain=Complex,
conditions=[NotEquals(a, zero)])

exp_not_eq_zero (conjecture without proof):

In [11]:
nat_x_to_first_power_is_x = Forall(
n,
Equals(Exp(n, one), n),
domain=Natural)

nat_x_to_first_power_is_x (conjecture without proof):

In [12]:
real_x_to_first_power_is_x = Forall(
x,
Equals(Exp(x, one), x),
domain=Real)

real_x_to_first_power_is_x (conjecture without proof):

In [13]:
complex_x_to_first_power_is_x = Forall([x],
Equals(Exp(x,one),
x),
domain = Complex)

complex_x_to_first_power_is_x (conjecture without proof):

In [14]:
exponent_log_with_same_base = (
Forall((a,x),
Equals(Exp(a, Log(a, x)), x),
domain=RealPos,
condition=NotEquals(a, one)))

exponent_log_with_same_base (conjecture without proof):

### Closure Theorems for General Exponentials¶

Note, we use the common convention to define $0^0 = 1$ for convenience, but it is important to note that $0^0$ is an indeterminant form with no well-defined limit for $f(t)^{g(t)}$ approaching $0^0$ (i.e. as $t \rightarrow 0$).

In [15]:
exp_natpos_closure = Forall(
(a, b),
InSet(Exp(a, b), NaturalPos),
domain=Natural)

exp_natpos_closure (conjecture without proof):

In [16]:
exp_int_closure = Forall(
(a, b),
InSet(Exp(a, b), Integer),
domains=(Integer, Natural))

exp_int_closure (conjecture without proof):

In [17]:
exp_rational_closure_nat_power = Forall(
(a, b), InSet(Exp(a, b), Rational),
domains=(Rational, Natural))

exp_rational_closure_nat_power (conjecture without proof):

In [18]:
exp_rational_nonzero_closure = Forall(
(a, b), InSet(Exp(a, b), RationalNonZero),
domains=(RationalNonZero, Integer))

exp_rational_nonzero_closure (conjecture without proof):

In [19]:
exp_rational_pos_closure = Forall(
(a, b), InSet(Exp(a, b), RationalPos),
domains=(RationalPos, Integer))

exp_rational_pos_closure (conjecture without proof):

In [20]:
exp_real_closure_nat_power = Forall(
(a, b), InSet(Exp(a, b), Real),
domains=(Real, Natural))

exp_real_closure_nat_power (conjecture without proof):

In [21]:
exp_real_pos_closure = Forall(
(a, b),
InSet(Exp(a, b), RealPos),
domains=(RealPos, Real))

exp_real_pos_closure (conjecture without proof):

In [22]:
exp_real_non_neg_closure = Forall(
(a, b),
InSet(Exp(a, b), RealNonNeg),
domains=(RealNonNeg, Real))

exp_real_non_neg_closure (conjecture without proof):

In [23]:
exp_complex_closure = Forall(
(a, b),
InSet(Exp(a, b), Complex),
domain=Complex)

exp_complex_closure (conjecture without proof):

In [24]:
exp_complex_nonzero_closure = Forall(
(a, b),
InSet(Exp(a, b), ComplexNonZero),
domains=(ComplexNonZero, Complex))

exp_complex_nonzero_closure (conjecture without proof):

### Closure theorems for sqrt and sqrd¶

In [25]:
sqrt_real_closure = Forall(
(a),
InSet(sqrt(a), Real),
domain=Real,
conditions=[greater_eq(a, zero)])

sqrt_real_closure (conjecture without proof):

In [26]:
sqrt_real_pos_closure = Forall(
(a),
InSet(sqrt(a), RealPos),
domain=RealPos)

sqrt_real_pos_closure (conjecture without proof):

In [27]:
sqrt_real_non_neg_closure = Forall(
(a),
InSet(sqrt(a), RealNonNeg),
domain=RealNonNeg)

sqrt_real_non_neg_closure (conjecture without proof):

In [28]:
sqrt_complex_closure = Forall(
(a),
InSet(sqrt(a), Complex),
domain=Complex)

sqrt_complex_closure (conjecture without proof):

In [29]:
sqrd_pos_closure = Forall(
a,
InSet(Exp(a, two), RealPos),
domain=Real,
conditions=[NotEquals(a, zero)])

sqrd_pos_closure (conjecture without proof):

In [30]:
sqrd_non_neg_closure = Forall(
a,
InSet(Exp(a, two), RealNonNeg),
domain=Real)

sqrd_non_neg_closure (conjecture without proof):

### Theorems for number relations¶

In [31]:
exp_eq_nat = Forall((a, x, y), Equals(Exp(x, a), Exp(y, a)), condition=Equals(x, y), domain=Natural)

exp_eq_nat (conjecture without proof):

In [32]:
exp_eq_int = Forall((a, x, y), Equals(Exp(x, a), Exp(y, a)), condition=Equals(x, y), domain=Integer)

exp_eq_int (conjecture without proof):

In [33]:
exp_eq_rational = Forall((a, x, y), Equals(Exp(x, a), Exp(y, a)), condition=Equals(x, y), domain=Rational)

exp_eq_rational (conjecture without proof):

In [34]:
exp_eq_real = Forall((a, x, y), Equals(Exp(x, a), Exp(y, a)), condition=Equals(x, y), domain=Real)

exp_eq_real (conjecture without proof):

In [35]:
# Note: does allow 0^0 = 0^0 where both sides are undefined.  That's okay -- "same" nonsense is
# equal in Prove-It.
exp_eq = Forall((a, x, y), Equals(Exp(x, a), Exp(y, a)), condition=Equals(x, y), domain=Complex)

exp_eq (established theorem):

In [36]:
exp_eq_for_eq_base_and_exp = (
Forall((a, x, y),
Equals(Exp(a, x), Exp(a, y)), condition=Equals(x, y), domain=Complex))

exp_eq_for_eq_base_and_exp (conjecture without proof):

In [37]:
# Note: this does not necessarily extend to the complex domain where
# exponentiation can have periodicity (e.g., exp(2 pi i )).
# ACTUALLY, this is a problem even for reals. For example,
# (-1)≠1 but (-1)^2 = 1^2, so this needs more careful thought — HC 9/28/20
#exp_neq = Forall((a, x, y), NotEquals(Exp(x, a), Exp(y, a)),
#                 conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Real)

In [38]:
exp_pos_less = Forall((a, x, y), Less(Exp(x, a), Exp(y, a)),
conditions=[number_ordering(LessEq(zero, x), Less(x, y)),
greater(a, zero)], domain=Real)

exp_pos_less (conjecture without proof):

In [39]:
exp_nonneg_less = Forall((a, x, y), LessEq(Exp(x, a), Exp(y, a)),
conditions=[number_ordering(Less(zero, x), Less(x, y)),
greater_eq(a, zero)], domain=Real)

exp_nonneg_less (conjecture without proof):

In [40]:
exp_neg_less = Forall((a, x, y), Less(Exp(y, a), Exp(x, a)),
conditions=[number_ordering(Less(zero, x), Less(x, y)),
Less(a, zero)], domain=Real)

exp_neg_less (conjecture without proof):

In [41]:
exp_nonpos_less = Forall((a, x, y), LessEq(Exp(y, a), Exp(x, a)),
conditions=[number_ordering(Less(zero, x), Less(x, y)),
LessEq(a, zero)], domain=Real)

exp_nonpos_less (conjecture without proof):

In [42]:
exp_pos_lesseq = Forall((a, x, y), LessEq(Exp(x, a), Exp(y, a)),
conditions=[number_ordering(LessEq(zero, x), LessEq(x, y)),
greater(a, zero)], domain=Real)

exp_pos_lesseq (conjecture without proof):

In [43]:
exp_nonneg_lesseq = Forall((a, x, y), LessEq(Exp(x, a), Exp(y, a)),
conditions=[number_ordering(Less(zero, x), LessEq(x, y)),
greater_eq(a, zero)], domain=Real)

exp_nonneg_lesseq (conjecture without proof):

In [44]:
exp_neg_lesseq = Forall((a, x, y), LessEq(Exp(y, a), Exp(x, a)),
conditions=[number_ordering(Less(zero, x), LessEq(x, y)),
Less(a, zero)], domain=Real)

exp_neg_lesseq (conjecture without proof):

In [45]:
exp_nonpos_lesseq = Forall((a, x, y), LessEq(Exp(y, a), Exp(x, a)),
conditions=[number_ordering(Less(zero, x), LessEq(x, y)),
LessEq(a, zero)], domain=Real)

exp_nonpos_lesseq (conjecture without proof):

In [46]:
# named and written for eventual even exponent,
# but exponent specified as 2 for now
exp_even_neg_base_less = Forall((a, x, y), Less(Exp(y, a), Exp(x, a)),
conditions=[number_ordering(Less(x, y), Less(y, zero)),
Equals(a, two)], domain=Real)

exp_even_neg_base_less (conjecture without proof):

In [47]:
# named and written for eventual even exponent,
# but exponent specified as 2 for now
exp_even_neg_base_lesseq = Forall((a, x, y), LessEq(Exp(y, a), Exp(x, a)),
conditions=[number_ordering(LessEq(x, y), Less(y, zero)),
Equals(a, two)], domain=Real)

exp_even_neg_base_lesseq (conjecture without proof):

In [48]:
exp_monotonicity_large_base_less = Forall(
(a, x, y),
Less(Exp(a, x), Exp(a, y)),
domain=Real,
conditions=[greater(a, one), Less(x, y)])

exp_monotonicity_large_base_less (conjecture without proof):

In [49]:
exp_monotonicity_large_base_less_eq = Forall(
(a, x, y),
LessEq(Exp(a, x), Exp(a, y)),
domain=Real,
conditions=[greater(a, one), LessEq(x, y)])

exp_monotonicity_large_base_less_eq (conjecture without proof):

### Even power exponentiation is a even function¶

In [50]:
even_pow_is_even_fn = Forall(
x, Forall(n, Equals(Exp(Neg(x), Mult(two, n)), Exp(x, Mult(two, n))),
domain=Natural),
domain=Complex)

even_pow_is_even_fn (conjecture without proof):

In [51]:
even_pow_is_even_fn_rev = Forall(
x, Forall(n, Equals(Exp(x, Mult(two, n)), Exp(Neg(x), Mult(two, n))),
domain=Natural),
domain=Complex)

even_pow_is_even_fn_rev (conjecture without proof):

## Exponentiation laws for positive whole number exponents¶

In [52]:
product_of_posnat_powers = Forall((a, m, n), Equals(Mult(Exp(a, m), Exp(a, n)), Exp(a, Add(m, n))),
domains=(Complex, NaturalPos, NaturalPos))

product_of_posnat_powers (conjecture without proof):

In [53]:
products_of_posnat_powers = Forall(m, Forall((a, k_1_to_m), Equals(prod_a_raise_ki__1_to_m, Exp(a, Add(k_1_to_m))),
domains=(Complex, NaturalPos)),
domain=NaturalPos)

products_of_posnat_powers (conjecture without proof):

In [54]:
quotient_of_posnat_powers = Forall((a, m, n), Equals(frac(Exp(a, m), Exp(a, n)), Exp(a, subtract(m, n))),
domains=(Complex, NaturalPos, NaturalPos),
condition=NotEquals(a, zero))

quotient_of_posnat_powers (conjecture without proof):

In [55]:
posnat_power_of_product = Forall((a, b, n), Equals(Exp(Mult(a, b), n), Mult(Exp(a, n), Exp(b, n))),
domains=(Complex, Complex, NaturalPos))

posnat_power_of_product (conjecture without proof):

In [56]:
posnat_power_of_products = Forall((m, n), Forall(a_1_to_m, Equals(Exp(Mult(a_1_to_m), n),
prod_ai_raise_n__1_to_m),
domain=Complex),
domain=NaturalPos)

posnat_power_of_products (conjecture without proof):

In [57]:
posnat_power_of_quotient = Forall((a, b, n), Equals(Exp(frac(a, b), n), frac(Exp(a, n), Exp(b, n))),
domains=(Complex, Complex, NaturalPos),
condition=NotEquals(b, zero))

posnat_power_of_quotient (conjecture without proof):

In [58]:
posnat_power_of_posnat_power = Forall((a, m, n), Equals(Exp(Exp(a, m), n), Exp(a, Mult(m, n))),
domains=(Complex, NaturalPos, NaturalPos))

posnat_power_of_posnat_power (conjecture without proof):

## Exponentiation laws for negative whole number exponents¶

In [59]:
neg_power_as_div = Forall((a, n), Equals(Exp(a, Neg(n)),
frac(one, Exp(a, n))),
domains=(ComplexNonZero, NaturalPos))

neg_power_as_div (conjecture without proof):

In [60]:
neg_power_of_quotient = Forall((a, b, n), Equals(Exp(frac(a, b), Neg(n)),
frac(Exp(b, n), Exp(a, n))),
domains=(ComplexNonZero, ComplexNonZero, NaturalPos))

neg_power_of_quotient (conjecture without proof):

## Exponentiation laws for positive, real exponents¶

These can be understood via $a = r \cdot e^{i \theta}$ for general $a \in \mathbb{C}$. Then $a^b = r^b \cdot e^{i b \theta}$ for $b \in \mathbb{R}$ and $b \neq 0$, and $e^{i b} \cdot e^{i c} = e^{i (b + c)}$.

In [61]:
product_of_pos_powers = Forall((a, b, c), Equals(Mult(Exp(a, b), Exp(a, c)), Exp(a, Add(b, c))),
domains=(Complex, RealPos, RealPos))

product_of_pos_powers (conjecture without proof):

In [62]:
products_of_pos_powers = Forall(m, Forall((a, b_1_to_m), Equals(prod_a_raise_bi__1_to_m, Exp(a, Add(b_1_to_m))),
domains=(Complex, RealPos)),
domain=NaturalPos)

products_of_pos_powers (conjecture without proof):

In [63]:
quotient_of_pos_powers = Forall((a, b, c), Equals(frac(Exp(a, b), Exp(a, c)), Exp(a, subtract(b, c))),
domains=(Complex, RealPos, RealPos),
condition=NotEquals(a, zero))

quotient_of_pos_powers (conjecture without proof):

In [64]:
pos_power_of_product = Forall((a, b, c), Equals(Exp(Mult(a, b), c), Mult(Exp(a, c), Exp(b, c))),
domains=(Complex, Complex, RealPos))

pos_power_of_product (conjecture without proof):

In [65]:
pos_power_of_products = Forall(m, Forall((a_1_to_m, b), Equals(Exp(Mult(a_1_to_m), b),
prod_ai_raise_b__1_to_m),
domains=(Complex, RealPos)),
domain=NaturalPos)

pos_power_of_products (conjecture without proof):

In [66]:
pos_power_of_quotient = Forall((a, b, c), Equals(Exp(frac(a, b), c), frac(Exp(a, c), Exp(b, c))),
domains=(Complex, Complex, RealPos),
condition=NotEquals(b, zero))

pos_power_of_quotient (conjecture without proof):

In [67]:
pos_power_of_pos_power = Forall((a, b, c), Equals(Exp(Exp(a, b), c), Exp(a, Mult(b, c))),
domains=(Complex, RealPos, RealPos))

pos_power_of_pos_power (conjecture without proof):

## Exponentiation laws for real exponents¶

Similar to the laws for positive exponents, but we need other means of avoiding $0^0$ which is undefined.

In [68]:
product_of_real_powers = Forall((a, b, c), Equals(Mult(Exp(a, b), Exp(a, c)), Exp(a, Add(b, c))),
domains=(Complex, Real, Real), condition=NotEquals(a, zero))

product_of_real_powers (conjecture without proof):

In [69]:
products_of_real_powers = Forall(m, Forall((a, b_1_to_m), Equals(prod_a_raise_bi__1_to_m, Exp(a, Add(b_1_to_m))),
domains=(Complex, Real), condition=NotEquals(a, zero)),
domain=NaturalPos)

products_of_real_powers (conjecture without proof):

In [70]:
quotient_of_real_powers = Forall((a, b, c), Equals(frac(Exp(a, b), Exp(a, c)), Exp(a, subtract(b, c))),
domains=(Complex, Real, Real), condition=NotEquals(a, zero))

quotient_of_real_powers (conjecture without proof):

In [71]:
real_power_of_product =(
Forall((a, b, c),
Equals(Exp(Mult(a, b), c), Mult(Exp(a, c), Exp(b, c))),
domains=(Complex, Complex, Real),
conditions = [NotEquals(a, zero), NotEquals(b, zero)]))

real_power_of_product (conjecture without proof):

In [72]:
real_power_of_products = (
Forall(m,
Forall((a_1_to_m, b),
Equals(Exp(Mult(a_1_to_m), b),
prod_ai_raise_b__1_to_m),
domains=(Complex, Real),
conditions=nonzero_a_1_to_m),
domain=NaturalPos))

real_power_of_products (conjecture without proof):

In [73]:
real_power_of_quotient = Forall((a, b, c), Equals(Exp(frac(a, b), c), frac(Exp(a, c), Exp(b, c))),
domains=(Complex, Complex, Real),
conditions = [NotEquals(a, zero), NotEquals(b, zero)])

real_power_of_quotient (conjecture without proof):

In [74]:
real_power_of_real_power = Forall((a, b, c), Equals(Exp(Exp(a, b), c), Exp(a, Mult(b, c))),
domains=(Complex, Real, Real),
condition = NotEquals(a, zero))

real_power_of_real_power (conjecture without proof):

In [75]:
negated_real_power_of_real_power = Forall((a, b, c), Equals(Exp(Exp(a, b), Neg(c)), Exp(a, Neg(Mult(b, c)))),
domains=(Complex, Real, Real),
condition = NotEquals(a, zero))

negated_real_power_of_real_power (conjecture without proof):

In [76]:
real_power_of_negated_real_power = Forall((a, b, c), Equals(Exp(Exp(a, Neg(b)), c), Exp(a, Neg(Mult(b, c)))),
domains=(Complex, Real, Real),
condition = NotEquals(a, zero))

real_power_of_negated_real_power (conjecture without proof):

In [77]:
negated_real_power_of_negated_real_power = Forall((a, b, c), Equals(Exp(Exp(a, Neg(b)), Neg(c)), Exp(a, Mult(b, c))),
domains=(Complex, Real, Real),
condition = NotEquals(a, zero))

negated_real_power_of_negated_real_power (conjecture without proof):

In [78]:
# if we don't know the exponents 'b' and 'c' are integers
# we need to constraint the real base a > 0
exp_factored_real = (
Forall(
(a, b, c, d),
Equals(
Exp(a, b),
Mult(Exp(a, c), Exp(a, d))),
domains=[RealPos, Real, Real, Real],

exp_factored_real (conjecture without proof):

In [79]:
# if we know the exponents are integers, we can relax
# the constraint on the base 'a' to include neg reals
exp_factored_int = Forall(
(a, b, c, d),
Equals(
Exp(a, b),
Mult(Exp(a, c), Exp(a, d))),
domains=[Real, Integer, Integer, Integer],

exp_factored_int (conjecture without proof):

## Complex exponentiation¶

$e^{a + b i} = e^a \cdot e^{bi}$

$a^{b + i c}$ = $e^{ln(a) \cdot (b + i c)}$ if $a \in \mathbb{R}^+$

$(a + i b)^{c + i d} = (a^2 + b^2)^{(c + i d)/2} \cdot e^{i (c + i d) arg(a + i b)}$

## Exponentiation laws for complex exponents and positive, real base¶

### Use $a^{b + i c}$ = $e^{ln(a) \cdot (b + i c)}$ if $a > 0$.¶

$a^b \cdot a^c = e^{ln(a) b} \cdot e^{ln(a) c} = e^{ln(a) (b + c)} = a^{b+c}$ if $a > 0$.

In [80]:
product_of_complex_powers = Forall((a, b, c), Equals(Mult(Exp(a, b), Exp(a, c)), Exp(a, Add(b, c))),
domains=(RealPos, Complex, Complex))

product_of_complex_powers (conjecture without proof):

In [81]:
products_of_complex_powers = Forall(m, Forall((a, b_1_to_m), Equals(prod_a_raise_bi__1_to_m, Exp(a, Add(b_1_to_m))),
domains=(RealPos, Complex)),
domain=NaturalPos)

products_of_complex_powers (conjecture without proof):

In [82]:
quotient_of_complex_powers = Forall((a, b, c), Equals(frac(Exp(a, b), Exp(a, c)), Exp(a, subtract(b, c))),
domains=(RealPos, Complex, Complex))

quotient_of_complex_powers (conjecture without proof):

$(a \cdot b)^c = e^{ln(a \cdot b) c} = e^{(ln(a) + ln(b)) c} = e^{ln(a) c} e^{ln(b) c} = a^c \cdot b^c$ if $a > 0$ and $b > 0$.

In [83]:
complex_power_of_product = Forall((a, b, c), Equals(Exp(Mult(a, b), c), Mult(Exp(a, c), Exp(b, c))),
domains=(RealPos, RealPos, Complex))

complex_power_of_product (conjecture without proof):

In [84]:
complex_power_of_products = Forall(m, Forall((a_1_to_m, b), Equals(Exp(Mult(a_1_to_m), b),
prod_ai_raise_b__1_to_m),
domains=(RealPos, Complex)),
domain=NaturalPos)

complex_power_of_products (conjecture without proof):

In [85]:
complex_power_of_quotient = Forall((a, b, c), Equals(Exp(frac(a, b), c), frac(Exp(a, c), Exp(b, c))),
domains=(RealPos, RealPos, Complex))

complex_power_of_quotient (conjecture without proof):

$(a^b)^c = (e^{ln(a) \cdot b})^c = e^{ln(a) \cdot b \cdot c} = a^{b \cdot c}$ if $a > 0$.

In [86]:
complex_power_of_complex_power = Forall((a, b, c), Equals(Exp(Exp(a, b), c), Exp(a, Mult(b, c))),
domains=(RealPos, Complex, Complex))

complex_power_of_complex_power (conjecture without proof):

In [87]:
from proveit import theta
from proveit.numbers import pi

In [88]:
# complex_power_not_one = Forall(
#        theta,
#        Equals(
#        NotEquals(Exp(e, Mult(i, theta)), one),
#        NotInSet(frac(theta, Mult(two, pi)), Integer)),
#        domain=Real)

In [89]:
unit_complex_polar_num_eq_one = Forall(
theta,
Equals(Exp(e, Mult(i, theta)), one),
domain=Real,
condition=InSet(frac(theta, Mult(two, pi)), Integer))

unit_complex_polar_num_eq_one (conjecture without proof):

In [90]:
complex_polar_num_eq_one = Forall(
(r, theta),
Equals(Mult(r, Exp(e, Mult(i, theta))), r),
domain=Real,
condition=InSet(frac(theta, Mult(two, pi)), Integer))

complex_polar_num_eq_one (conjecture without proof):

In [91]:
unit_complex_polar_num_neq_one = Forall(
theta,
NotEquals(Exp(e, Mult(i, theta)), one),
condition=NotInSet(frac(theta, Mult(two, pi)), Integer),
domain=Real)

unit_complex_polar_num_neq_one (conjecture without proof):

In [92]:
complex_polar_num_neq_mag = Forall(
(r, theta),
NotEquals(Mult(r, Exp(e, Mult(i, theta))), r),
condition=NotInSet(frac(theta, Mult(two, pi)), Integer),
domains=(RealPos, Real))

complex_polar_num_neq_mag (conjecture without proof):

### Other Misc Theorems¶

In [93]:
# lower bound for exponentials with natural positive base and natural positive exp
nat_pos_to_nat_pos_lower_bound = Forall(
(a, b),
greater_eq(Exp(a, b), a),
domain = NaturalPos)

nat_pos_to_nat_pos_lower_bound (conjecture without proof):

In [94]:
square_abs_rational_simp = Forall(
a,
Equals(Exp(Abs(a),two),Exp(a,two)),
domain = Rational)

square_abs_rational_simp (conjecture without proof):

In [95]:
square_abs_real_simp = Forall(
a,
Equals(Exp(Abs(a),two),Exp(a,two)),
domain = Real)

square_abs_real_simp (conjecture without proof):

In [96]:
# Note: if |a| <= b then b >= 0 and |b| = b.
square_abs_ineq = Forall(
(a,b),
LessEq(Exp(Abs(a),two),Exp(b,two)),
domain = Real,
conditions = (LessEq(Abs(a),b),))

square_abs_ineq (conjecture without proof):

In [97]:
# covered by product_of_complex_powers
# # not true for general a in C, but true for a in R
# # except a = 0
# # noting $a^{b + i c}$ = $e^{ln(a) \cdot (b + i c)}$.
# sum_in_exp = Forall([a,b,c],
#     domains = (Real, Complex, Complex),
#     conditions=[NotEquals(a, zero)])

In [98]:
# true even for complex a = r exp(i theta),
# but exclude a = 0 to avoid 0^0 which is undefined.
[a,b],
domain = Complex,
conditions=[NotEquals(a, zero)])


In [99]:
# true even for complex a = r exp(i theta)
# but exclude a = 0 to avoid 0^0 which is undefined.
[a,b],
domain = Complex,
conditions=[NotEquals(a, zero)])


In [100]:
# here we allow for a 0 base but a non-zero exponent
[a,b],
domain = Complex,
conditions=[NotEquals(b, zero), NotEquals(b, Neg(one))])


In [101]:
# Redundant.  Handled by sum_in_exp.
# diff_in_exp = Forall(
#     [a,b,c],
#     Equals(Mult(Exp(a,b),Exp(a,Neg(c))), Exp(a,subtract(b,c))),
#     domains = [Real, Complex, Complex],
#     conditions=[NotEquals(a, zero)])

In [102]:
# diff_frac_in_exp = Forall(
#     [a,b,c,d],
#     Equals(Mult(Exp(a,b),Exp(a,frac(Neg(c), d))),
#            Exp(a, subtract(b,frac(c, d)))),
#     domain = Real,
#     conditions=[NotEquals(a, zero), NotEquals(d, zero)])

In [103]:
# same as complex_power_of_product
# exp_of_positives_prod = Forall(
#     c,
#     Forall((a, b),
#            Equals(Exp(Mult(a,b),c), Mult(Exp(a,c),Exp(b,c))),
#            domain=RealPos),
#     domain=Complex)

In [104]:
# covered by real_power_of_product
# int_exp_of_prod = Forall(
#     n,
#     Forall((a, b),
#            Equals(Exp(Mult(a,b),n), Mult(Exp(a,n),Exp(b,n))),
#            domain=Complex,
#            conditions=[NotEquals(a, zero), NotEquals(b, zero)]),
#     domain=Integer)

In [105]:
# same posnat_power_of_product
# nats_pos_exp_of_prod = Forall(
#     n,
#     Forall((a, b),
#            Equals(Exp(Mult(a,b),n), Mult(Exp(a,n),Exp(b,n))),
#            domain=Complex),
#     domain=NaturalPos)

In [106]:
# Not true in general
# same_exp_distribute = Forall(
#     [x,y,z],
#     Equals(Mult(Exp(x,y),Exp(z,y)), Exp(Mult(x,z),y)),
#     domain = Complex)

In [107]:
# Works for integers powers through repetition of a^b (or a^{-b}) and adding exponents.
# Does not work for fractional powers.  Consider sqrt[(-1)^2] = 1 not (-1)^{2*(1/2)} = -1.
int_exp_of_exp = Forall(
n,
Forall((a, b),
Equals(Exp(Exp(a, b), n), Exp(a, Mult(b, n))),
domain=Complex, conditions=[NotEquals(a, zero)]),
domain=Integer)

int_exp_of_exp (conjecture without proof):

In [108]:
int_exp_of_neg_exp = Forall(
n,
Forall((a, b),
Equals(Exp(Exp(a, Neg(b)), n), Exp(a, Neg(Mult(b, n)))),
domain=Complex, conditions=[NotEquals(a, zero)]),
domain=Integer)

int_exp_of_neg_exp (conjecture without proof):

In [109]:
neg_int_exp_of_exp = Forall(
n,
Forall((a, b),
Equals(Exp(Exp(a, b), Neg(n)), Exp(a, Neg(Mult(b, n)))),
domain=Complex, conditions=[NotEquals(a, zero)]),
domain=Integer)

neg_int_exp_of_exp (conjecture without proof):

In [110]:
neg_int_exp_of_neg_exp = Forall(
n,
Forall((a, b),
Equals(Exp(Exp(a, Neg(b)), Neg(n)), Exp(a, Mult(b, n))),
domain=Complex, conditions=[NotEquals(a, zero)]),
domain=Integer)

neg_int_exp_of_neg_exp (conjecture without proof):

In [111]:
diff_square_comm = Forall(
[a,b],
Equals(Exp(subtract(a,b),two),Exp(subtract(b,a),two)),
domain = Complex)

diff_square_comm (conjecture without proof):

In [112]:
sqrt_of_prod = Forall(
n,
Forall(ExprRange(k, IndexedVar(a, k), one, n),
Equals(sqrt(Mult(a_1_to_n)),
Mult(ExprRange(k, sqrt(IndexedVar(a, k)), one, n))),
domain = Complex),
domain = NaturalPos)

sqrt_of_prod (conjecture without proof):

In [113]:
sqrt_times_itself = Forall(
x,
Equals(Mult(sqrt(x), sqrt(x)), x),
domain=Real,
conditions=[greater_eq(x, zero)])

sqrt_times_itself (conjecture without proof):

In [114]:
nth_power_of_nth_root = Forall(
n, Forall(x, Equals(Exp(Exp(x, frac(one, n)), n), x),
condition=greater_eq(x, zero)),
domain=NaturalPos)

nth_power_of_nth_root (conjecture without proof):

In [115]:
nth_root_of_nth_power = Forall(
n, Forall(x, Equals(Exp(Exp(x, n), frac(one, n)), x),
condition=greater_eq(x, zero)),
domain=NaturalPos)

nth_root_of_nth_power (conjecture without proof):

In [116]:
sqrt_of_square = Forall(
x, Equals(sqrt(Exp(x, two)), x),
domain=Real)

sqrt_of_square (conjecture without proof):

In [ ]:



### Expansion Theorems¶

In [117]:
# until we have the more general "exp_expansion"
square_expansion = Forall(
x,
Equals(Exp(x, two), Mult(x, x)),
domain=Complex)

square_expansion (conjecture without proof):

In [118]:
# until we have the more general "exp_expansion"
cube_expansion = Forall(
x,
Equals(Exp(x, three), Mult(x, x, x)),
domain=Complex)

cube_expansion (conjecture without proof):

Note: Could eventually include generalizations to “even power closure,” etc, but need to define and implement an Evens set to do this

### Sqrt(2) is not rational¶

In [119]:
sqrt2_is_not_rational = NotInSet(sqrt(two), Rational)

sqrt2_is_not_rational (conjecture with conjecture-based proof):

In [120]:
%end theorems

These theorems may now be imported from the theory package: proveit.numbers.exponentiation