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

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)

%begin theorems

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

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):

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

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

exponentiated_one (conjecture without proof):

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

exp_zero_eq_one (conjecture without proof):

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

exponentiated_zero (conjecture without proof):

exp_in_zero_set = Forall((a, b), InSet(Exp(a, b), ZeroSet), domains=(ZeroSet, RealPos))

exp_in_zero_set (conjecture without proof):

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):

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):

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):

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):

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):

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$).

exp_natpos_closure = Forall(
    (a, b), 
    InSet(Exp(a, b), NaturalPos),
    domain=Natural)

exp_natpos_closure (conjecture without proof):

exp_int_closure = Forall(
    (a, b), 
    InSet(Exp(a, b), Integer),
    domains=(Integer, Natural))

exp_int_closure (conjecture without proof):

exp_rational_closure_nat_power = Forall(
    (a, b), InSet(Exp(a, b), Rational),
    domains=(Rational, Natural))

exp_rational_closure_nat_power (conjecture without proof):

exp_rational_nonzero_closure = Forall(
    (a, b), InSet(Exp(a, b), RationalNonZero),
    domains=(RationalNonZero, Integer))

exp_rational_nonzero_closure (conjecture without proof):

exp_rational_pos_closure = Forall(
    (a, b), InSet(Exp(a, b), RationalPos),
    domains=(RationalPos, Integer))

exp_rational_pos_closure (conjecture without proof):

exp_real_closure_nat_power = Forall(
    (a, b), InSet(Exp(a, b), Real),
    domains=(Real, Natural))

exp_real_closure_nat_power (conjecture without proof):

exp_real_pos_closure = Forall(
    (a, b),
    InSet(Exp(a, b), RealPos),
    domains=(RealPos, Real))

exp_real_pos_closure (conjecture without proof):

exp_real_non_neg_closure = Forall(
    (a, b),
    InSet(Exp(a, b), RealNonNeg),
    domains=(RealNonNeg, Real))

exp_real_non_neg_closure (conjecture without proof):

exp_complex_closure = Forall(
    (a, b),
    InSet(Exp(a, b), Complex),
    domain=Complex)

exp_complex_closure (conjecture without proof):

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

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

sqrt_real_closure (conjecture without proof):

sqrt_real_pos_closure = Forall(
    (a),
    InSet(sqrt(a), RealPos),
    domain=RealPos)

sqrt_real_pos_closure (conjecture without proof):

sqrt_real_non_neg_closure = Forall(
    (a),
    InSet(sqrt(a), RealNonNeg),
    domain=RealNonNeg)

sqrt_real_non_neg_closure (conjecture without proof):

sqrt_complex_closure = Forall(
    (a),
    InSet(sqrt(a), Complex),
    domain=Complex)

sqrt_complex_closure (conjecture without proof):

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

sqrd_pos_closure (conjecture without proof):

sqrd_non_neg_closure = Forall(
    a,
    InSet(Exp(a, two), RealNonNeg),
    domain=Real)

sqrd_non_neg_closure (conjecture without proof):

Theorems for number relations

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):

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):

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):

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):

# 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):

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):

# 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)

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):

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):

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):

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):

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):

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):

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):

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):

# 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):

# 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):

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):

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

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):

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

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):

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):

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):

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):

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):

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):

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

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):

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)}$.

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):

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):

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):

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):

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):

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):

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.

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

# 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],
    condition=Equals(b, Add(c, d))))

exp_factored_real (conjecture without proof):

# 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],
    conditions=[NotEquals(a, zero), Equals(b, Add(c, d))])

exp_factored_int (conjecture without proof):

Complex exponentiation

Note (to be added):

$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$.

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):

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):

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$.

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):

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):

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$.

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):

from proveit import theta
from proveit.numbers import pi

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

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):

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):

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):

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

# 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):

square_abs_rational_simp = Forall(
    a,
    Equals(Exp(Abs(a),two),Exp(a,two)),
    domain = Rational)

square_abs_rational_simp (conjecture without proof):

square_abs_real_simp = Forall(
    a,
    Equals(Exp(Abs(a),two),Exp(a,two)),
    domain = Real)

square_abs_real_simp (conjecture without proof):

# 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):

# 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],
#     Equals(Mult(Exp(a,b),Exp(a,c)), Exp(a,Add(b,c))),
#     domains = (Real, Complex, Complex),
#     conditions=[NotEquals(a, zero)])

# true even for complex a = r exp(i theta),
# but exclude a = 0 to avoid 0^0 which is undefined.
add_one_right_in_exp = Forall(
    [a,b],
    Equals(Mult(Exp(a,b),a), Exp(a,Add(b,one))),
    domain = Complex,
    conditions=[NotEquals(a, zero)])

add_one_right_in_exp (conjecture without proof):

# true even for complex a = r exp(i theta)
# but exclude a = 0 to avoid 0^0 which is undefined.
add_one_left_in_exp = Forall(
    [a,b],
    Equals(Mult(a, Exp(a,b)), Exp(a,Add(one, b))),
    domain = Complex,
    conditions=[NotEquals(a, zero)])

add_one_left_in_exp (conjecture without proof):

# here we allow for a 0 base but a non-zero exponent
add_one_left_in_exp_poss_zero_base = Forall(
    [a,b],
    Equals(Mult(a, Exp(a,b)), Exp(a,Add(one, b))),
    domain = Complex,
    conditions=[NotEquals(b, zero), NotEquals(b, Neg(one))])

add_one_left_in_exp_poss_zero_base (conjecture without proof):

# 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)])

# 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)])

# 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)

# 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)

# 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)

# 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)

# 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):

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):

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):

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):

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):

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):

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):

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):

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):

sqrt_of_square = Forall(
    x, Equals(sqrt(Exp(x, two)), x),
    domain=Real)

sqrt_of_square (conjecture without proof):

Expansion Theorems

# 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):

# 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

sqrt2_is_not_rational = NotInSet(sqrt(two), Rational)

sqrt2_is_not_rational (conjecture with conjecture-based proof):

%end theorems

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