P. 107 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10601-10700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expnlbnd2 10601*	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 10602	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 10603	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 10604	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 10605	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 10606	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) = ( A x. A ) )
Theorem	sqcld 10607	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^ 2 ) e. CC )
Theorem	sqeq0d 10608	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 10609	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 10610	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 10611	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 10612	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 10613	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 10614	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 10615	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 10616	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 10617	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 10618	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 10619	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 10620	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 10621	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 10622	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 10623	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 10624	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 10625	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 10626	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 10627	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 10628	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 10629	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 10630	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> ( A ^ 2 ) e. NN )
Theorem	nnexpcld 10631	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 10632	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 10633	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 10634	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 10635	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A ^ 2 ) e. RR )
Theorem	sqge0d 10636	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> 0 <_ ( A ^ 2 ) )
Theorem	sqgt0apd 10637	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 10638	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 10639	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 10640	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 10641	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 10642	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 10643	Analogue to sq11 10548 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	nn0ltexp2 10644	Special case of ltexp2 13654 which we use here because we haven't yet defined df-rpcxp 13574 which is used in the current proof of ltexp2 13654. (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 10645	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	sq10 10646	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 10647	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 10648	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 10649	Lemma for expcan 10650. 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 10650	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 10651	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 10652	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 10653	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 10654	A rather pretty lemma for nn0opth2 10658. (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 10655	Lemma for nn0opth2 10658. (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 10656	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 3592 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 10657	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 10656. (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 10658	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 10656. (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 10659	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 10660	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 13763). 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 10661	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 10662	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 0 ) = 1
Theorem	fac1 10663	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 1 ) = 1
Theorem	facp1 10664	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 10665	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 2 ) = 2
Theorem	fac3 10666	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 3 ) = 6
Theorem	fac4 10667	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ! ` 4 ) = ; 2 4
Theorem	facnn2 10668	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
Theorem	faccl 10669	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN0 -> ( ! ` N ) e. NN )
Theorem	faccld 10670	Closure of the factorial function, deduction version of faccl 10669. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ! ` N ) e. NN )
Theorem	facne0 10671	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|- ( N e. NN0 -> ( ! ` N ) =/= 0 )
Theorem	facdiv 10672	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 10673	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 10674	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )
Theorem	faclbnd 10675	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 10676	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )
Theorem	faclbnd3 10677	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 10678	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 10679	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( N e. NN0 -> ( ! ` N ) <_ ( N ^ N ) )
Theorem	facavg 10680	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 10681	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class _C
Definition	df-bc 10682*	Define the binomial coefficient operation. For example, ( 5 _C 3 ) = 1 0 (ex-bc 13764). 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 10683	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 10684 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 10684	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 10685	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 10686	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 10687	Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 10702.) (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
Theorem	bccmpl 10688	"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 10689	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 10690	The binomial coefficient " 0 choose K " is 0 for a positive integer K. Note that ( 0 _C 0 ) = 1 (see bcn0 10689). (Contributed by Alexander van der Vekens, 1-Jan-2018.)
|- ( K e. NN -> ( 0 _C K ) = 0 )
Theorem	bcnn 10691	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 )
Theorem	bcn1 10692	Binomial coefficient: N choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( N _C 1 ) = N )
Theorem	bcnp1n 10693	Binomial coefficient: N + 1 choose N. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( ( N + 1 ) _C N ) = ( N + 1 ) )
Theorem	bcm1k 10694	The proportion of one binomial coefficient to another with K decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 1 ... N ) -> ( N _C K ) = ( ( N _C ( K - 1 ) ) x. ( ( N - ( K - 1 ) ) / K ) ) )
Theorem	bcp1n 10695	The proportion of one binomial coefficient to another with N increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C K ) = ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )
Theorem	bcp1nk 10696	The proportion of one binomial coefficient to another with N and K increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( K + 1 ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )
Theorem	bcval5 10697	Write out the top and bottom parts of the binomial coefficient ( N _C K ) = ( N x. ( N - 1 ) x. ... x. ( ( N - K ) + 1 ) ) / K ! explicitly. In this form, it is valid even for N < K, although it is no longer valid for nonpositive K. (Contributed by Mario Carneiro, 22-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.)
|- ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
Theorem	bcn2 10698	Binomial coefficient: N choose 2. (Contributed by Mario Carneiro, 22-May-2014.)
|- ( N e. NN0 -> ( N _C 2 ) = ( ( N x. ( N - 1 ) ) / 2 ) )
Theorem	bcp1m1 10699	Compute the binomial coefficient of ( N + 1 ) over ( N - 1 ) (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- ( N e. NN0 -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )
Theorem	bcpasc 10700	Pascal's rule for the binomial coefficient, generalized to all integers K. Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( N _C K ) + ( N _C ( K - 1 ) ) ) = ( ( N + 1 ) _C K ) )