P. 108 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10701-10800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	leexp2a 10701	Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) <_ ( A ^ N ) )
Theorem	leexp2r 10702	Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|- ( ( ( A e. RR /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ N ) <_ ( A ^ M ) )
Theorem	leexp1a 10703	Weak base ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005.)
|- ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ N ) <_ ( B ^ N ) )
Theorem	exple1 10704	A real between 0 and 1 inclusive raised to a nonnegative integer is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ N e. NN0 ) -> ( A ^ N ) <_ 1 )
Theorem	expubnd 10705	An upper bound on A ^ N when 2 <_ A. (Contributed by NM, 19-Dec-2005.)
|- ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( A ^ N ) <_ ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )
Theorem	sqval 10706	Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
|- ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqneg 10707	The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
Theorem	sqsubswap 10708	Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( B - A ) ^ 2 ) )
Theorem	sqcl 10709	Closure of square. (Contributed by NM, 10-Aug-1999.)
|- ( A e. CC -> ( A ^ 2 ) e. CC )
Theorem	sqmul 10710	Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ 2 ) = ( ( A ^ 2 ) x. ( B ^ 2 ) ) )
Theorem	sqeq0 10711	A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.)
|- ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
Theorem	sqdivap 10712	Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
Theorem	sqdividap 10713	The square of a complex number apart from zero divided by itself equals that number. (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. CC /\ A # 0 ) -> ( ( A ^ 2 ) / A ) = A )
Theorem	sqne0 10714	A number is nonzero iff its square is nonzero. See also sqap0 10715 which is the same but with not equal changed to apart. (Contributed by NM, 11-Mar-2006.)
|- ( A e. CC -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )
Theorem	sqap0 10715	A number is apart from zero iff its square is apart from zero. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( A e. CC -> ( ( A ^ 2 ) # 0 <-> A # 0 ) )
Theorem	resqcl 10716	Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> ( A ^ 2 ) e. RR )
Theorem	sqgt0ap 10717	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( A e. RR /\ A # 0 ) -> 0 < ( A ^ 2 ) )
Theorem	nnsqcl 10718	The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( A e. NN -> ( A ^ 2 ) e. NN )
Theorem	zsqcl 10719	Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
Theorem	qsqcl 10720	The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( A ^ 2 ) e. QQ )
Theorem	sq11 10721	The square function is one-to-one for nonnegative reals. Also see sq11ap 10816 which would easily follow from this given excluded middle, but which for us is proved another way. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )
Theorem	lt2sq 10722	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( A ^ 2 ) < ( B ^ 2 ) ) )
Theorem	le2sq 10723	The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
Theorem	le2sq2 10724	The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ A <_ B ) ) -> ( A ^ 2 ) <_ ( B ^ 2 ) )
Theorem	sqge0 10725	A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> 0 <_ ( A ^ 2 ) )
Theorem	zsqcl2 10726	The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> ( A ^ 2 ) e. NN0 )
Theorem	sumsqeq0 10727	Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 28-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 ) )
Theorem	sqvali 10728	Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) = ( A x. A )
Theorem	sqcli 10729	Closure of square. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) e. CC
Theorem	sqeq0i 10730	A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( A ^ 2 ) = 0 <-> A = 0 )
Theorem	sqmuli 10731	Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A x. B ) ^ 2 ) = ( ( A ^ 2 ) x. ( B ^ 2 ) )
Theorem	sqdivapi 10732	Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- A e. CC   &    |- B e. CC   &    |- B # 0   =>    |- ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) )
Theorem	resqcli 10733	Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( A ^ 2 ) e. RR
Theorem	sqgt0api 10734	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- A e. RR   =>    |- ( A # 0 -> 0 < ( A ^ 2 ) )
Theorem	sqge0i 10735	A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- 0 <_ ( A ^ 2 )
Theorem	lt2sqi 10736	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( A ^ 2 ) < ( B ^ 2 ) ) )
Theorem	le2sqi 10737	The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
Theorem	sq11i 10738	The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )
Theorem	sq0 10739	The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|- ( 0 ^ 2 ) = 0
Theorem	sq0i 10740	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
|- ( A = 0 -> ( A ^ 2 ) = 0 )
Theorem	sq0id 10741	If a number is zero, its square is zero. Deduction form of sq0i 10740. Converse of sqeq0d 10781. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = 0 )   =>    |- ( ph -> ( A ^ 2 ) = 0 )
Theorem	sq1 10742	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|- ( 1 ^ 2 ) = 1
Theorem	neg1sqe1 10743	-u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( -u 1 ^ 2 ) = 1
Theorem	sq2 10744	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|- ( 2 ^ 2 ) = 4
Theorem	sq3 10745	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|- ( 3 ^ 2 ) = 9
Theorem	sq4e2t8 10746	The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|- ( 4 ^ 2 ) = ( 2 x. 8 )
Theorem	cu2 10747	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|- ( 2 ^ 3 ) = 8
Theorem	irec 10748	The reciprocal of _i. (Contributed by NM, 11-Oct-1999.)
|- ( 1 / _i ) = -u _i
Theorem	i2 10749	_i squared. (Contributed by NM, 6-May-1999.)
|- ( _i ^ 2 ) = -u 1
Theorem	i3 10750	_i cubed. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 3 ) = -u _i
Theorem	i4 10751	_i to the fourth power. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 4 ) = 1
Theorem	nnlesq 10752	A positive integer is less than or equal to its square. For general integers, see zzlesq 10817. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( N e. NN -> N <_ ( N ^ 2 ) )
Theorem	iexpcyc 10753	Taking _i to the K-th power is the same as using the K mod 4 -th power instead, by i4 10751. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )
Theorem	expnass 10754	A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
|- ( ( 3 ^ 3 ) ^ 3 ) < ( 3 ^ ( 3 ^ 3 ) )
Theorem	subsq 10755	Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) )
Theorem	subsq2 10756	Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( ( A - B ) ^ 2 ) + ( ( 2 x. B ) x. ( A - B ) ) ) )
Theorem	binom2i 10757	The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) )
Theorem	subsqi 10758	Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) )
Theorem	qsqeqor 10759	The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )
Theorem	binom2 10760	The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
Theorem	binom21 10761	Special case of binom2 10760 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
Theorem	binom2sub 10762	Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
Theorem	binom2sub1 10763	Special case of binom2sub 10762 where B = 1. (Contributed by AV, 2-Aug-2021.)
|- ( A e. CC -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
Theorem	binom2subi 10764	Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A - B ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) )
Theorem	mulbinom2 10765	The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( C x. A ) + B ) ^ 2 ) = ( ( ( ( C x. A ) ^ 2 ) + ( ( 2 x. C ) x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
Theorem	binom3 10766	The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 3 ) = ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) )
Theorem	zesq 10767	An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) )
Theorem	nnesq 10768	A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( N e. NN -> ( ( N / 2 ) e. NN <-> ( ( N ^ 2 ) / 2 ) e. NN ) )
Theorem	bernneq 10769	Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
|- ( ( A e. RR /\ N e. NN0 /\ -u 1 <_ A ) -> ( 1 + ( A x. N ) ) <_ ( ( 1 + A ) ^ N ) )
Theorem	bernneq2 10770	Variation of Bernoulli's inequality bernneq 10769. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 10771	A corollary of bernneq 10769. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 10772*	Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
|- ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. k e. NN A < ( B ^ k ) )
Theorem	expnlbnd 10773*	The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.)
|- ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> E. k e. NN ( 1 / ( B ^ k ) ) < A )
Theorem	expnlbnd2 10774*	The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
|- ( ( A e. RR+ /\ B e. RR /\ 1 < B ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( 1 / ( B ^ k ) ) < A )
Theorem	modqexp 10775	Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. QQ )   &    |- ( ph -> 0 < D )   &    |- ( ph -> ( A mod D ) = ( B mod D ) )   =>    |- ( ph -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) )
Theorem	exp0d 10776	Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 0 ) = 1 )
Theorem	exp1d 10777	Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 1 ) = A )
Theorem	expeq0d 10778	Positive integer exponentiation is 0 iff its base is 0. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( A ^ N ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	sqvald 10779	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqcld 10780	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) e. CC )
Theorem	sqeq0d 10781	A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( A ^ 2 ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	expcld 10782	Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ^ N ) e. CC )
Theorem	expp1d 10783	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
Theorem	expaddd 10784	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expmuld 10785	Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
Theorem	sqrecapd 10786	Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( ( 1 / A ) ^ 2 ) = ( 1 / ( A ^ 2 ) ) )
Theorem	expclzapd 10787	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ N ) e. CC )
Theorem	expap0d 10788	Nonnegative integer exponentiation is nonzero if its base is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ N ) # 0 )
Theorem	expnegapd 10789	Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
Theorem	exprecapd 10790	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )
Theorem	expp1zapd 10791	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
Theorem	expm1apd 10792	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )
Theorem	expsubapd 10793	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( A ^ ( M - N ) ) = ( ( A ^ M ) / ( A ^ N ) ) )
Theorem	sqmuld 10794	Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A x. B ) ^ 2 ) = ( ( A ^ 2 ) x. ( B ^ 2 ) ) )
Theorem	sqdivapd 10795	Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
Theorem	expdivapd 10796	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ( A / B ) ^ N ) = ( ( A ^ N ) / ( B ^ N ) ) )
Theorem	mulexpd 10797	Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
Theorem	0expd 10798	Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> N e. NN )   =>    |- ( ph -> ( 0 ^ N ) = 0 )
Theorem	reexpcld 10799	Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ^ N ) e. RR )
Theorem	expge0d 10800	A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> 0 <_ ( A ^ N ) )