P. 109 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expm1t 10801	Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.)
|- ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )
Theorem	1exp 10802	Value of one raised to a nonnegative integer power. (Contributed by NM, 15-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( N e. ZZ -> ( 1 ^ N ) = 1 )
Theorem	expap0 10803	Positive integer exponentiation is apart from zero iff its base is apart from zero. That it is easier to prove this first, and then prove expeq0 10804 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." (Remark of [Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) # 0 <-> A # 0 ) )
Theorem	expeq0 10804	Positive integer exponentiation is 0 iff its base is 0. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) = 0 <-> A = 0 ) )
Theorem	expap0i 10805	Integer exponentiation is apart from zero if its base is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ N ) # 0 )
Theorem	expgt0 10806	A positive real raised to an integer power is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. ZZ /\ 0 < A ) -> 0 < ( A ^ N ) )
Theorem	expnegzap 10807	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
Theorem	0exp 10808	Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
|- ( N e. NN -> ( 0 ^ N ) = 0 )
Theorem	expge0 10809	A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> 0 <_ ( A ^ N ) )
Theorem	expge1 10810	A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ N ) )
Theorem	expgt1 10811	A real greater than 1 raised to a positive integer is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 < ( A ^ N ) )
Theorem	mulexp 10812	Nonnegative integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
Theorem	mulexpzap 10813	Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) /\ N e. ZZ ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
Theorem	exprecap 10814	Integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )
Theorem	expadd 10815	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by NM, 30-Nov-2004.)
|- ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expaddzaplem 10816	Lemma for expaddzap 10817. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expaddzap 10817	Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expmul 10818	Product of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006.)
|- ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
Theorem	expmulzap 10819	Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
Theorem	m1expeven 10820	Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018.)
|- ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = 1 )
Theorem	expsubap 10821	Exponent subtraction law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M - N ) ) = ( ( A ^ M ) / ( A ^ N ) ) )
Theorem	expp1zap 10822	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
Theorem	expm1ap 10823	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )
Theorem	expdivap 10824	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ( ( A e. CC /\ ( B e. CC /\ B # 0 ) /\ N e. NN0 ) -> ( ( A / B ) ^ N ) = ( ( A ^ N ) / ( B ^ N ) ) )
Theorem	ltexp2a 10825	Ordering relationship for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ M ) < ( A ^ N ) )
Theorem	leexp2a 10826	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 10827	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 10828	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 10829	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 10830	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 10831	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 10832	The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
Theorem	sqsubswap 10833	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 10834	Closure of square. (Contributed by NM, 10-Aug-1999.)
|- ( A e. CC -> ( A ^ 2 ) e. CC )
Theorem	sqmul 10835	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 10836	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 10837	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 10838	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 10839	A number is nonzero iff its square is nonzero. See also sqap0 10840 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 10840	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 10841	Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> ( A ^ 2 ) e. RR )
Theorem	sqgt0ap 10842	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 10843	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 10844	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 10845	The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( A ^ 2 ) e. QQ )
Theorem	sq11 10846	The square function is one-to-one for nonnegative reals. Also see sq11ap 10941 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 10847	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 10848	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 10849	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 10850	A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> 0 <_ ( A ^ 2 ) )
Theorem	zsqcl2 10851	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 10852	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 10853	Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) = ( A x. A )
Theorem	sqcli 10854	Closure of square. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) e. CC
Theorem	sqeq0i 10855	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 10856	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 10857	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 10858	Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( A ^ 2 ) e. RR
Theorem	sqgt0api 10859	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 10860	A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- 0 <_ ( A ^ 2 )
Theorem	lt2sqi 10861	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 10862	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 10863	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 10864	The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|- ( 0 ^ 2 ) = 0
Theorem	sq0i 10865	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
|- ( A = 0 -> ( A ^ 2 ) = 0 )
Theorem	sq0id 10866	If a number is zero, its square is zero. Deduction form of sq0i 10865. Converse of sqeq0d 10906. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = 0 )   =>    |- ( ph -> ( A ^ 2 ) = 0 )
Theorem	sq1 10867	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|- ( 1 ^ 2 ) = 1
Theorem	neg1sqe1 10868	-u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( -u 1 ^ 2 ) = 1
Theorem	sq2 10869	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|- ( 2 ^ 2 ) = 4
Theorem	sq3 10870	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|- ( 3 ^ 2 ) = 9
Theorem	sq4e2t8 10871	The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|- ( 4 ^ 2 ) = ( 2 x. 8 )
Theorem	cu2 10872	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|- ( 2 ^ 3 ) = 8
Theorem	irec 10873	The reciprocal of _i. (Contributed by NM, 11-Oct-1999.)
|- ( 1 / _i ) = -u _i
Theorem	i2 10874	_i squared. (Contributed by NM, 6-May-1999.)
|- ( _i ^ 2 ) = -u 1
Theorem	i3 10875	_i cubed. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 3 ) = -u _i
Theorem	i4 10876	_i to the fourth power. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 4 ) = 1
Theorem	nnlesq 10877	A positive integer is less than or equal to its square. For general integers, see zzlesq 10942. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( N e. NN -> N <_ ( N ^ 2 ) )
Theorem	iexpcyc 10878	Taking _i to the K-th power is the same as using the K mod 4 -th power instead, by i4 10876. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )
Theorem	expnass 10879	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 10880	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 10881	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 10882	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 10883	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 10884	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 10885	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 10886	Special case of binom2 10885 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
Theorem	binom2sub 10887	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 10888	Special case of binom2sub 10887 where B = 1. (Contributed by AV, 2-Aug-2021.)
|- ( A e. CC -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
Theorem	binom2subi 10889	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 10890	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 10891	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 10892	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 10893	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 10894	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 10895	Variation of Bernoulli's inequality bernneq 10894. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 10896	A corollary of bernneq 10894. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 10897*	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 10898*	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 10899*	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 10900	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 ) )