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	zesq 10801	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 10802	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 10803	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 10804	Variation of Bernoulli's inequality bernneq 10803. (Contributed by NM, 18-Oct-2007.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. N ) + 1 ) <_ ( A ^ N ) )
Theorem	bernneq3 10805	A corollary of bernneq 10803. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )
Theorem	expnbnd 10806*	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 10807*	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 10808*	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 10809	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 10810	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 10811	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 10812	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 10813	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqcld 10814	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) e. CC )
Theorem	sqeq0d 10815	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 10816	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 10817	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 10818	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 10819	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 10820	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 10821	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 10822	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 10823	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 10824	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 10825	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 10826	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 10827	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 10828	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 10829	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 10830	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 10831	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 10832	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 10833	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 10834	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 10835	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 10836	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 10837	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( A ^ 2 ) e. NN )
Theorem	nnexpcld 10838	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 10839	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 10840	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 10841	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 10842	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A ^ 2 ) e. RR )
Theorem	sqge0d 10843	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> 0 <_ ( A ^ 2 ) )
Theorem	sqgt0apd 10844	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 10845	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 10846	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 10847	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 10848	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 10849	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 10850	Analogue to sq11 10755 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 10851	An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.)
|- ( N e. ZZ -> N <_ ( N ^ 2 ) )
Theorem	nn0ltexp2 10852	Special case of ltexp2 15355 which we use here because we haven't yet defined df-rpcxp 15273 which is used in the current proof of ltexp2 15355. (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 10853	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 10854	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 10855	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 10856	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 10857	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 10858	Lemma for expcan 10859. 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 10859	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 10860	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 10861	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 10862	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 10863	A rather pretty lemma for nn0opth2 10867. (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 10864	Lemma for nn0opth2 10867. (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 10865	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 3641 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 10866	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 10865. (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 10867	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 10865. (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 10868	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 10869	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 15597). 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 10870	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 10871	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 0 ) = 1
Theorem	fac1 10872	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 1 ) = 1
Theorem	facp1 10873	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 10874	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 2 ) = 2
Theorem	fac3 10875	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 3 ) = 6
Theorem	fac4 10876	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ! ` 4 ) = ; 2 4
Theorem	facnn2 10877	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
Theorem	faccl 10878	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN0 -> ( ! ` N ) e. NN )
Theorem	faccld 10879	Closure of the factorial function, deduction version of faccl 10878. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ! ` N ) e. NN )
Theorem	facne0 10880	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|- ( N e. NN0 -> ( ! ` N ) =/= 0 )
Theorem	facdiv 10881	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 10882	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 10883	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )
Theorem	faclbnd 10884	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 10885	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )
Theorem	faclbnd3 10886	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 10887	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 10888	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( N e. NN0 -> ( ! ` N ) <_ ( N ^ N ) )
Theorem	facavg 10889	The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) )
4.6.9  The binomial coefficient operation
Syntax	cbc 10890	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class _C
Definition	df-bc 10891*	Define the binomial coefficient operation. For example, ( 5 _C 3 ) = 1 0 (ex-bc 15598). In the literature, this function is often written as a column vector of the two arguments, or with the arguments as subscripts before and after the letter "C". ( N _C K ) is read " N choose K." Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ k <_ n does not hold. (Contributed by NM, 10-Jul-2005.)
|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
Theorem	bcval 10892	Value of the binomial coefficient, N choose K. Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ K <_ N does not hold. See bcval2 10893 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )
Theorem	bcval2 10893	Value of the binomial coefficient, N choose K, in its standard domain. (Contributed by NM, 9-Jun-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
Theorem	bcval3 10894	Value of the binomial coefficient, N choose K, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
Theorem	bcval4 10895	Value of the binomial coefficient, N choose K, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ /\ ( K < 0 \/ N < K ) ) -> ( N _C K ) = 0 )
Theorem	bcrpcl 10896	Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 10911.) (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
Theorem	bccmpl 10897	"Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = ( N _C ( N - K ) ) )
Theorem	bcn0 10898	N choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( N _C 0 ) = 1 )
Theorem	bc0k 10899	The binomial coefficient " 0 choose K " is 0 for a positive integer K. Note that ( 0 _C 0 ) = 1 (see bcn0 10898). (Contributed by Alexander van der Vekens, 1-Jan-2018.)
|- ( K e. NN -> ( 0 _C K ) = 0 )
Theorem	bcnn 10900	N choose N is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( N _C N ) = 1 )