P. 98 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sq0id 9701	If a number is zero, its square is zero. Deduction form of sq0i 9700. Converse of sqeq0d 9737. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = 0 )   =>    |- ( ph -> ( A ^ 2 ) = 0 )
Theorem	sq1 9702	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|- ( 1 ^ 2 ) = 1
Theorem	neg1sqe1 9703	-u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( -u 1 ^ 2 ) = 1
Theorem	sq2 9704	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|- ( 2 ^ 2 ) = 4
Theorem	sq3 9705	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|- ( 3 ^ 2 ) = 9
Theorem	cu2 9706	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|- ( 2 ^ 3 ) = 8
Theorem	irec 9707	The reciprocal of _i. (Contributed by NM, 11-Oct-1999.)
|- ( 1 / _i ) = -u _i
Theorem	i2 9708	_i squared. (Contributed by NM, 6-May-1999.)
|- ( _i ^ 2 ) = -u 1
Theorem	i3 9709	_i cubed. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 3 ) = -u _i
Theorem	i4 9710	_i to the fourth power. (Contributed by NM, 31-Jan-2007.)
|- ( _i ^ 4 ) = 1
Theorem	nnlesq 9711	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 9712	Taking _i to the K-th power is the same as using the K mod 4 -th power instead, by i4 9710. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )
Theorem	expnass 9713	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 9714	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 9715	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 9716	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 9717	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 9718	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 9719	Special case of binom2 9718 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
Theorem	binom2sub 9720	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	binom2subi 9721	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 9722	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 9723	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 9724	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 9725	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 9726	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 9727	Variation of Bernoulli's inequality bernneq 9726. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 9728	A corollary of bernneq 9726. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 9729*	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 9730*	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 9731*	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 9732	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 9733	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 9734	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 9735	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqcld 9736	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) e. CC )
Theorem	sqeq0d 9737	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 9738	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 9739	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 9740	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 9741	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 9742	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 9743	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 9744	Nonnegative integer exponentiation is nonzero if its mantissa 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 9745	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 9746	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 9747	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 9748	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 9749	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 9750	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 9751	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 9752	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 9753	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 9754	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 9755	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 9756	Nonnegative integer exponentiation with a nonnegative mantissa 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 9757	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> 1 <_ ( A ^ N ) )
Theorem	sqoddm1div8 9758	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 9759	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( A ^ 2 ) e. NN )
Theorem	nnexpcld 9760	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 9761	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 9762	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 9763	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 9764	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A ^ 2 ) e. RR )
Theorem	sqge0d 9765	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> 0 <_ ( A ^ 2 ) )
Theorem	sqgt0apd 9766	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 9767	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 9768	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 9769	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 9770	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 9771	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 9772	Analogue to sq11 9681 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	sq10 9773	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 9774	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 9775	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 9776	Lemma for expcan 9777. 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 9777	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 9778	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 )
3.6.7  Ordered pair theorem for nonnegative integers
Theorem	nn0le2msqd 9779	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 9780	A rather pretty lemma for nn0opth2 9784. (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 9781	Lemma for nn0opth2 9784. (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 9782	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 3426 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 9783	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 9782. (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 9784	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 9782. (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 ) ) )
3.6.8  Factorial function
Syntax	cfa 9785	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 9786	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 10809). 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 , CC ) )
Theorem	facnn 9787	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 , CC ) ` N ) )
Theorem	fac0 9788	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 0 ) = 1
Theorem	fac1 9789	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 1 ) = 1
Theorem	facp1 9790	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 9791	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 2 ) = 2
Theorem	fac3 9792	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 3 ) = 6
Theorem	fac4 9793	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ! ` 4 ) = ; 2 4
Theorem	facnn2 9794	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
Theorem	faccl 9795	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN0 -> ( ! ` N ) e. NN )
Theorem	faccld 9796	Closure of the factorial function, deduction version of faccl 9795. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ! ` N ) e. NN )
Theorem	facne0 9797	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|- ( N e. NN0 -> ( ! ` N ) =/= 0 )
Theorem	facdiv 9798	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 9799	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 9800	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )