P. 110 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10901-11000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subsq 10901	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 10902	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 10903	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 10904	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 10905	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 10906	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 10907	Special case of binom2 10906 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
Theorem	binom2sub 10908	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 10909	Special case of binom2sub 10908 where B = 1. (Contributed by AV, 2-Aug-2021.)
|- ( A e. CC -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
Theorem	binom2subi 10910	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 10911	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 10912	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 10913	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 10914	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 10915	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 10916	Variation of Bernoulli's inequality bernneq 10915. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 10917	A corollary of bernneq 10915. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 10918*	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 10919*	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 10920*	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 10921	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 10922	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 10923	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 10924	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 10925	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqcld 10926	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) e. CC )
Theorem	sqeq0d 10927	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 10928	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 10929	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 10930	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 10931	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 10932	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 10933	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 10934	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 10935	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 10936	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 10937	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 10938	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 10939	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 10940	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 10941	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 10942	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 10943	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 10944	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 10945	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 10946	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 ) )
Theorem	expge1d 10947	A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> 1 <_ ( A ^ N ) )
Theorem	sqoddm1div8 10948	A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021.)
|- ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( ( M ^ 2 ) - 1 ) / 8 ) = ( ( N x. ( N + 1 ) ) / 2 ) )
Theorem	nnsqcld 10949	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( A ^ 2 ) e. NN )
Theorem	nnexpcld 10950	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ^ N ) e. NN )
Theorem	nn0expcld 10951	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ^ N ) e. NN0 )
Theorem	rpexpcld 10952	Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ N ) e. RR+ )
Theorem	reexpclzapd 10953	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A # 0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( A ^ N ) e. RR )
Theorem	resqcld 10954	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A ^ 2 ) e. RR )
Theorem	sqge0d 10955	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> 0 <_ ( A ^ 2 ) )
Theorem	sqgt0apd 10956	The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> 0 < ( A ^ 2 ) )
Theorem	leexp2ad 10957	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 <_ A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( A ^ M ) <_ ( A ^ N ) )
Theorem	leexp2rd 10958	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A <_ 1 )   =>    |- ( ph -> ( A ^ N ) <_ ( A ^ M ) )
Theorem	lt2sqd 10959	The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A < B <-> ( A ^ 2 ) < ( B ^ 2 ) ) )
Theorem	le2sqd 10960	The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A <_ B <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
Theorem	sq11d 10961	The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> ( A ^ 2 ) = ( B ^ 2 ) )   =>    |- ( ph -> A = B )
Theorem	sq11ap 10962	Analogue to sq11 10867 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) # ( B ^ 2 ) <-> A # B ) )
Theorem	zzlesq 10963	An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.)
|- ( N e. ZZ -> N <_ ( N ^ 2 ) )
Theorem	nn0ltexp2 10964	Special case of ltexp2 15658 which we use here because we haven't yet defined df-rpcxp 15576 which is used in the current proof of ltexp2 15658. (Contributed by Jim Kingdon, 7-Oct-2024.)
|- ( ( ( A e. RR /\ M e. NN0 /\ N e. NN0 ) /\ 1 < A ) -> ( M < N <-> ( A ^ M ) < ( A ^ N ) ) )
Theorem	nn0leexp2 10965	Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
|- ( ( ( A e. RR /\ M e. NN0 /\ N e. NN0 ) /\ 1 < A ) -> ( M <_ N <-> ( A ^ M ) <_ ( A ^ N ) ) )
Theorem	mulsubdivbinom2ap 10966	The square of a binomial with factor minus a number divided by a number apart from zero. (Contributed by AV, 19-Jul-2021.)
|- ( ( ( A e. CC /\ B e. CC /\ D e. CC ) /\ ( C e. CC /\ C # 0 ) ) -> ( ( ( ( ( C x. A ) + B ) ^ 2 ) - D ) / C ) = ( ( ( C x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - D ) / C ) ) )
Theorem	sq10 10967	The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|- (; 1 0 ^ 2 ) = ;; 1 0 0
Theorem	sq10e99m1 10968	The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|- (; 1 0 ^ 2 ) = (; 9 9 + 1 )
Theorem	3dec 10969	A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|- A e. NN0   &    |- B e. NN0   =>    |- ;; A B C = ( ( ( (; 1 0 ^ 2 ) x. A ) + (; 1 0 x. B ) ) + C )
Theorem	expcanlem 10970	Lemma for expcan 10971. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> 1 < A )   =>    |- ( ph -> ( ( A ^ M ) <_ ( A ^ N ) -> M <_ N ) )
Theorem	expcan 10971	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	expcand 10972	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> 1 < A )   &    |- ( ph -> ( A ^ M ) = ( A ^ N ) )   =>    |- ( ph -> M = N )
Theorem	apexp1 10973	Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN ) -> ( ( A ^ N ) # ( B ^ N ) -> A # B ) )
4.6.7  Ordered pair theorem for nonnegative integers
Theorem	nn0le2msqd 10974	The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   =>    |- ( ph -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	nn0opthlem1d 10975	A rather pretty lemma for nn0opth2 10979. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> C e. NN0 )   =>    |- ( ph -> ( A < C <-> ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) ) )
Theorem	nn0opthlem2d 10976	Lemma for nn0opth2 10979. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> ( ( A + B ) < C -> ( ( C x. C ) + D ) =/= ( ( ( A + B ) x. ( A + B ) ) + B ) ) )
Theorem	nn0opthd 10977	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers A and B by ( ( ( A + B ) x. ( A + B ) ) + B ). If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 3676 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) <-> ( A = C /\ B = D ) ) )
Theorem	nn0opth2d 10978	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 10977. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) )
Theorem	nn0opth2 10979	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 10977. (Contributed by NM, 22-Jul-2004.)
|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) )
4.6.8  Factorial function
Syntax	cfa 10980	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 10981	Define the factorial function on nonnegative integers. For example, ( ! ` 5 ) = 1 2 0 because 1 x. 2 x. 3 x. 4 x. 5 = 1 2 0 (ex-fac 16274). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.)
|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
Theorem	facnn 10982	Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
Theorem	fac0 10983	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 0 ) = 1
Theorem	fac1 10984	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 1 ) = 1
Theorem	facp1 10985	The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
Theorem	fac2 10986	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 2 ) = 2
Theorem	fac3 10987	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 3 ) = 6
Theorem	fac4 10988	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ! ` 4 ) = ; 2 4
Theorem	facnn2 10989	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
Theorem	faccl 10990	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN0 -> ( ! ` N ) e. NN )
Theorem	faccld 10991	Closure of the factorial function, deduction version of faccl 10990. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ! ` N ) e. NN )
Theorem	facne0 10992	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|- ( N e. NN0 -> ( ! ` N ) =/= 0 )
Theorem	facdiv 10993	A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.)
|- ( ( M e. NN0 /\ N e. NN /\ N <_ M ) -> ( ( ! ` M ) / N ) e. NN )
Theorem	facndiv 10994	No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.)
|- ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> -. ( ( ( ! ` M ) + 1 ) / N ) e. ZZ )
Theorem	facwordi 10995	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )
Theorem	faclbnd 10996	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
Theorem	faclbnd2 10997	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )
Theorem	faclbnd3 10998	A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
Theorem	faclbnd6 10999	Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.)
|- ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ M ) ) <_ ( ! ` ( N + M ) ) )
Theorem	facubnd 11000	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( N e. NN0 -> ( ! ` N ) <_ ( N ^ N ) )