P. 130 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12901-13000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exprec 12901	Nonnegative integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )
Theorem	expadd 12902	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	expaddzlem 12903	Lemma for expaddz 12904. (Contributed by Mario Carneiro, 4-Jun-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expaddz 12904	Sum of exponents law for integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 4-Jun-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expmul 12905	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	expmulz 12906	Product of exponents law for integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
Theorem	m1expeven 12907	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	expsub 12908	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M - N ) ) = ( ( A ^ M ) / ( A ^ N ) ) )
Theorem	expp1z 12909	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
Theorem	expm1 12910	Value of a complex number raised to an integer power minus one. (Contributed by NM, 25-Dec-2008.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )
Theorem	expdiv 12911	Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ N e. NN0 ) -> ( ( A / B ) ^ N ) = ( ( A ^ N ) / ( B ^ N ) ) )
Theorem	ltexp2a 12912	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	expcan 12913	Cancellation law 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 ) -> ( ( A ^ M ) = ( A ^ N ) <-> M = N ) )
Theorem	ltexp2 12914	Ordering law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( M < N <-> ( A ^ M ) < ( A ^ N ) ) )
Theorem	leexp2 12915	Ordering law for exponentiation. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( M <_ N <-> ( A ^ M ) <_ ( A ^ N ) ) )
Theorem	leexp2a 12916	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	ltexp2r 12917	The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( M < N <-> ( A ^ N ) < ( A ^ M ) ) )
Theorem	leexp2r 12918	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 12919	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 12920	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 12921	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 12922	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 12923	The square of the negative of a number. (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
Theorem	sqsubswap 12924	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 12925	Closure of square. (Contributed by NM, 10-Aug-1999.)
|- ( A e. CC -> ( A ^ 2 ) e. CC )
Theorem	sqmul 12926	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 12927	A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.)
|- ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
Theorem	sqdiv 12928	Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
Theorem	sqdivid 12929	The square of a nonzero number divided by itself yields the number itself. (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^ 2 ) / A ) = A )
Theorem	sqne0 12930	A number is nonzero iff its square is nonzero. (Contributed by NM, 11-Mar-2006.)
|- ( A e. CC -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )
Theorem	resqcl 12931	Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> ( A ^ 2 ) e. RR )
Theorem	sqgt0 12932	The square of a nonzero real is positive. (Contributed by NM, 8-Sep-2007.)
|- ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A ^ 2 ) )
Theorem	nnsqcl 12933	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 12934	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 12935	The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|- ( A e. QQ -> ( A ^ 2 ) e. QQ )
Theorem	sq11 12936	The square function is one-to-one for nonnegative reals. (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 12937	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 12938	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 12939	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 12940	A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|- ( A e. RR -> 0 <_ ( A ^ 2 ) )
Theorem	zsqcl2 12941	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 12942	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 12943	Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) = ( A x. A )
Theorem	sqcli 12944	Closure of square. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( A ^ 2 ) e. CC
Theorem	sqeq0i 12945	A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( A ^ 2 ) = 0 <-> A = 0 )
Theorem	sqrecii 12946	Square of reciprocal. (Contributed by NM, 17-Sep-1999.)
|- A e. CC   &    |- A =/= 0   =>    |- ( ( 1 / A ) ^ 2 ) = ( 1 / ( A ^ 2 ) )
Theorem	sqmuli 12947	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	sqdivi 12948	Distribution of square over division. (Contributed by NM, 20-Aug-2001.)
|- A e. CC   &    |- B e. CC   &    |- B =/= 0   =>    |- ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) )
Theorem	resqcli 12949	Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( A ^ 2 ) e. RR
Theorem	sqgt0i 12950	The square of a nonzero real is positive. (Contributed by NM, 17-Sep-1999.)
|- A e. RR   =>    |- ( A =/= 0 -> 0 < ( A ^ 2 ) )
Theorem	sqge0i 12951	A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- 0 <_ ( A ^ 2 )
Theorem	lt2sqi 12952	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 12953	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 12954	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 12955	The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|- ( 0 ^ 2 ) = 0
Theorem	sq0i 12956	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
|- ( A = 0 -> ( A ^ 2 ) = 0 )
Theorem	sq0id 12957	If a number is zero, its square is zero. Deduction form of sq0i 12956. Converse of sqeq0d 13007. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = 0 )   =>    |- ( ph -> ( A ^ 2 ) = 0 )
Theorem	sq1 12958	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|- ( 1 ^ 2 ) = 1
Theorem	neg1sqe1 12959	-u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( -u 1 ^ 2 ) = 1
Theorem	sq2 12960	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|- ( 2 ^ 2 ) = 4
Theorem	sq3 12961	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|- ( 3 ^ 2 ) = 9
Theorem	sq4e2t8 12962	The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|- ( 4 ^ 2 ) = ( 2 x. 8 )
Theorem	cu2 12963	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|- ( 2 ^ 3 ) = 8
Theorem	irec 12964	The reciprocal of _i. (Contributed by NM, 11-Oct-1999.)
|- ( 1 / _i ) = -u _i
Theorem	i2 12965	_i squared. (Contributed by NM, 6-May-1999.)
|- ( _i ^ 2 ) = -u 1
Theorem	i3 12966	_i cubed. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 3 ) = -u _i
Theorem	i4 12967	_i to the fourth power. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 4 ) = 1
Theorem	nnlesq 12968	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 12969	Taking _i to the K-th power is the same as using the K mod 4 -th power instead, by i4 12967. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )
Theorem	expnass 12970	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	sqlecan 12971	Cancel one factor of a square in a <_ comparison. Unlike lemul1 10875, the common factor A may be zero. (Contributed by NM, 17-Jan-2008.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) <_ ( B x. A ) <-> A <_ B ) )
Theorem	subsq 12972	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 12973	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 12974	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 12975	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	sqeqori 12976	The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by NM, 15-Jan-2006.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) )
Theorem	subsq0i 12977	The two solutions to the difference of squares set equal to zero. (Contributed by NM, 25-Apr-2006.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A = B \/ A = -u B ) )
Theorem	sqeqor 12978	The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )
Theorem	binom2 12979	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 12980	Special case of binom2 12979 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
Theorem	binom2sub 12981	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 12982	Special case of binom2sub 12981 where B = 1. (Contributed by AV, 2-Aug-2021.)
|- ( A e. CC -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
Theorem	binom2subi 12983	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 12984	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 12985	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	sq01 12986	If a complex number equals its square, it must be 0 or 1. (Contributed by NM, 6-Jun-2006.)
|- ( A e. CC -> ( ( A ^ 2 ) = A <-> ( A = 0 \/ A = 1 ) ) )
Theorem	zesq 12987	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 12988	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	crreczi 12989	Reciprocal of a complex number in terms of real and imaginary components. Remark in [Apostol] p. 361. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Jeff Hankins, 16-Dec-2013.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( A =/= 0 \/ B =/= 0 ) -> ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
Theorem	bernneq 12990	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 12991	Variation of Bernoulli's inequality bernneq 12990. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 12992	A corollary of bernneq 12990. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 12993*	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 12994*	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 12995*	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	expmulnbnd 12996*	Exponentiation with a mantissa greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( A x. k ) < ( B ^ k ) )
Theorem	digit2 12997	Two ways to express the K th digit in the decimal (when base B = 1 0) expansion of a number A. K = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008.)
|- ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( |_ ` ( ( B ^ K ) x. A ) ) - ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) ) )
Theorem	digit1 12998	Two ways to express the K th digit in the decimal expansion of a number A (when base B = 1 0). K = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009.)
|- ( ( A e. RR /\ B e. NN /\ K e. NN ) -> ( ( |_ ` ( ( B ^ K ) x. A ) ) mod B ) = ( ( ( |_ ` ( ( B ^ K ) x. A ) ) mod ( B ^ K ) ) - ( ( B x. ( |_ ` ( ( B ^ ( K - 1 ) ) x. A ) ) ) mod ( B ^ K ) ) ) )
Theorem	modexp 12999	Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) )
Theorem	discr1 13000*	A nonnegative quadratic form has nonnegative leading coefficient. (Contributed by Mario Carneiro, 4-Jun-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. RR ) -> 0 <_ ( ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) + C ) )   &    |- X = if ( 1 <_ ( ( ( B + if ( 0 <_ C , C , 0 ) ) + 1 ) / -u A ) , ( ( ( B + if ( 0 <_ C , C , 0 ) ) + 1 ) / -u A ) , 1 )   =>    |- ( ph -> 0 <_ A )