P. 102 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10101-10200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expeq0 10101	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) = 0 <-> A = 0 ) )
Theorem	expap0i 10102	Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ N ) # 0 )
Theorem	expgt0 10103	Nonnegative integer exponentiation with a positive mantissa 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 10104	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 10105	Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
|- ( N e. NN -> ( 0 ^ N ) = 0 )
Theorem	expge0 10106	Nonnegative integer exponentiation with a nonnegative mantissa 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 10107	Nonnegative integer exponentiation with a mantissa greater than or equal to 1 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 10108	Positive integer exponentiation with a mantissa greater than 1 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 10109	Positive 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 10110	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 10111	Nonnegative 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 10112	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 10113	Lemma for expaddzap 10114. (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 10114	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 10115	Product of exponents law for positive 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 10116	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 10117	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 10118	Exponent subtraction law for nonnegative 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 10119	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 10120	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 10121	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 10122	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 10123	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 10124	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 10125	Weak mantissa 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 10126	Nonnegative integer exponentiation with a mantissa between 0 and 1 inclusive 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 10127	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 10128	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 10129	The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
Theorem	sqsubswap 10130	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 10131	Closure of square. (Contributed by NM, 10-Aug-1999.)
|- ( A e. CC -> ( A ^ 2 ) e. CC )
Theorem	sqmul 10132	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 10133	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 10134	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	sqne0 10135	A number is nonzero iff its square is nonzero. See also sqap0 10136 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 10136	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 10137	Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> ( A ^ 2 ) e. RR )
Theorem	sqgt0ap 10138	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 10139	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 10140	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 10141	The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( A ^ 2 ) e. QQ )
Theorem	sq11 10142	The square function is one-to-one for nonnegative reals. Also see sq11ap 10235 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 10143	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 10144	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 10145	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 10146	A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> 0 <_ ( A ^ 2 ) )
Theorem	zsqcl2 10147	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 10148	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 10149	Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) = ( A x. A )
Theorem	sqcli 10150	Closure of square. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) e. CC
Theorem	sqeq0i 10151	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 10152	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 10153	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 10154	Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( A ^ 2 ) e. RR
Theorem	sqgt0api 10155	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 10156	A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- 0 <_ ( A ^ 2 )
Theorem	lt2sqi 10157	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 10158	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 10159	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 10160	The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|- ( 0 ^ 2 ) = 0
Theorem	sq0i 10161	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
|- ( A = 0 -> ( A ^ 2 ) = 0 )
Theorem	sq0id 10162	If a number is zero, its square is zero. Deduction form of sq0i 10161. Converse of sqeq0d 10200. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = 0 )   =>    |- ( ph -> ( A ^ 2 ) = 0 )
Theorem	sq1 10163	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|- ( 1 ^ 2 ) = 1
Theorem	neg1sqe1 10164	-u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( -u 1 ^ 2 ) = 1
Theorem	sq2 10165	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|- ( 2 ^ 2 ) = 4
Theorem	sq3 10166	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|- ( 3 ^ 2 ) = 9
Theorem	sq4e2t8 10167	The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|- ( 4 ^ 2 ) = ( 2 x. 8 )
Theorem	cu2 10168	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|- ( 2 ^ 3 ) = 8
Theorem	irec 10169	The reciprocal of _i. (Contributed by NM, 11-Oct-1999.)
|- ( 1 / _i ) = -u _i
Theorem	i2 10170	_i squared. (Contributed by NM, 6-May-1999.)
|- ( _i ^ 2 ) = -u 1
Theorem	i3 10171	_i cubed. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 3 ) = -u _i
Theorem	i4 10172	_i to the fourth power. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 4 ) = 1
Theorem	nnlesq 10173	A positive integer is less than or equal to its square. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( N e. NN -> N <_ ( N ^ 2 ) )
Theorem	iexpcyc 10174	Taking _i to the K-th power is the same as using the K mod 4 -th power instead, by i4 10172. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )
Theorem	expnass 10175	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 10176	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 10177	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 10178	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 10179	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	binom2 10180	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 10181	Special case of binom2 10180 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
Theorem	binom2sub 10182	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 10183	Special case of binom2sub 10182 where B = 1. (Contributed by AV, 2-Aug-2021.)
|- ( A e. CC -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
Theorem	binom2subi 10184	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 10185	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 10186	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 10187	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 10188	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 10189	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 10190	Variation of Bernoulli's inequality bernneq 10189. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 10191	A corollary of bernneq 10189. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 10192*	Exponentiation with a mantissa 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 10193*	The reciprocal of exponentiation with a mantissa greater than 1 has no 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 10194*	The reciprocal of exponentiation with a mantissa greater than 1 has no 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	exp0d 10195	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 10196	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 10197	Positive integer exponentiation is 0 iff its mantissa 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 10198	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqcld 10199	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) e. CC )
Theorem	sqeq0d 10200	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 )