P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	int-eqineqd 36501	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> B <_ A )
Theorem	int-ineqmvtd 36502	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> A = ( C + D ) )   =>    |- ( ph -> ( B - D ) <_ C )
Theorem	int-ineq1stprincd 36503	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> D <_ C )   =>    |- ( ph -> ( B + D ) <_ ( A + C ) )
Theorem	int-ineq2ndprincd 36504	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> 0 <_ C )   =>    |- ( ph -> ( B x. C ) <_ ( A x. C ) )
Theorem	int-ineqtransd 36505	InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> C <_ B )   =>    |- ( ph -> C <_ A )
21.26.3  N-Digit Addition Proof Generator This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 11067 addcomli 9827 00id 9810 addid1i 9822 addid2i 9823 eqid 2423 dec0h 11069 decadd 11094 decaddc 11095.
Theorem	unitadd 36506	Theorem used in conjunction with decaddc 11095 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( A + B ) = F   &    |- ( C + 1 ) = B   &    |- A e. NN0   &    |- C e. NN0   =>    |- ( ( A + C ) + 1 ) = F
Theorem	5p5e10b 36507	5 + 5 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 5 + 5 ) = ; 1 0
Theorem	6p4e10b 36508	6 + 4 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 6 + 4 ) = ; 1 0
Theorem	7p3e10b 36509	7 + 3 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 7 + 3 ) = ; 1 0
Theorem	8p2e10b 36510	8 + 2 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 8 + 2 ) = ; 1 0
Theorem	9p1e10b 36511	9 + 1 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 9 + 1 ) = ; 1 0
21.26.4  AM-GM (for k = 2,3,4)
Theorem	gsumws3 36512	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsumg <" S T U "> ) = ( S .+ ( T .+ U ) ) )
Theorem	gsumws4 36513	Valuation of a length 4 word in a monoid (Contributed by Stanislas Polu, 10-Sep-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ ( U e. B /\ V e. B ) ) ) ) -> ( G gsumg <" S T U V "> ) = ( S .+ ( T .+ ( U .+ V ) ) ) )
Theorem	amgm2d 36514	Arithmetic-geometric mean inequality for n = 2, derived from amgmlem 23907. (Contributed by Stanislas Polu, 8-Sep-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( ( A x. B ) ^c ( 1 / 2 ) ) <_ ( ( A + B ) / 2 ) )
Theorem	amgm3d 36515	Arithmetic-geometric mean inequality for n = 3. (Contributed by Stanislas Polu, 11-Sep-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A x. ( B x. C ) ) ^c ( 1 / 3 ) ) <_ ( ( A + ( B + C ) ) / 3 ) )
Theorem	amgm4d 36516	Arithmetic-geometric mean inequality for n = 4. (Contributed by Stanislas Polu, 11-Sep-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> D e. RR+ )   =>    |- ( ph -> ( ( A x. ( B x. ( C x. D ) ) ) ^c ( 1 / 4 ) ) <_ ( ( A + ( B + ( C + D ) ) ) / 4 ) )
21.27  Mathbox for Steve Rodriguez
21.27.1  Miscellanea
Theorem	nanorxor 36517	'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- ( ( ph -/\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
Theorem	undisjrab 36518	Union of two disjoint restricted class abstractions; compare unrab 3745. (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- ( ( { x e. A | ph } i^i { x e. A | ps } ) = (/) <-> ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/_ ps ) } )
Theorem	iso0 36519	The empty set is an R , S isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
|- (/) Isom R , S ( (/) , (/) )
Theorem	ssrecnpr 36520	RR is a subset of both RR and CC. (Contributed by Steve Rodriguez, 22-Nov-2015.)
|- ( S e. { RR , CC } -> RR C_ S )
Theorem	seff 36521	Let set S be the real or complex numbers. Then the exponential function restricted to S is a mapping from S to S. (Contributed by Steve Rodriguez, 6-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   =>    |- ( ph -> ( exp |` S ) : S --> S )
Theorem	sblpnf 36522	The infinity ball in the absolute value metric is just the whole space. S analog of blpnf 21404. (Contributed by Steve Rodriguez, 8-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- D = ( ( abs o. - ) |` ( S X. S ) )   =>    |- ( ( ph /\ P e. S ) -> ( P ( ball ` D ) +oo ) = S )
Theorem	prmunb2 36523*	The primes are unbounded. This generalizes prmunb 14851 to real A with arch 10868 and lttrd 9798: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( A e. RR -> E. p e. Prime A < p )
Theorem	isprm7 36524*	One need only check prime divisors of P up to sqr P in order to ensure primality. This version of isprm5 14644 combines the primality and bound on z into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ( 2 ... ( |_ ` ( sqr ` P ) ) ) i^i Prime ) -. z || P ) )
21.27.2  Ratio test for infinite series convergence and divergence
Theorem	dvgrat 36525*	Ratio test for divergence of a complex infinite series. See e.g. remark "if ( abs ` ( ( a ` ( n + 1 ) ) / ( a ` n ) ) ) >_ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )   &    |- ( ( ph /\ k e. W ) -> ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )   =>    |- ( ph -> seq M ( + , F ) e/ dom ~~> )
Theorem	cvgdvgrat 36526*	Ratio test for convergence and divergence of a complex infinite series. If the ratio R of the absolute values of successive terms in an infinite sequence F converges to less than one, then the infinite sum of the terms of F converges to a complex number; and if R converges greater then the sum diverges. This combined form of cvgrat 13932 and dvgrat 36525 directly uses the limit of the ratio. (It also demonstrates how to use climi2 13568 and absltd 13485 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 2971 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 2918 at https://groups.google.com/forum/#!topic/metamath/2RPikOiXLMo.) (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )   &    |- R = ( k e. W |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )   &    |- ( ph -> R ~~> L )   &    |- ( ph -> L =/= 1 )   =>    |- ( ph -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) )
Theorem	radcnvrat 36527*	Let L be the limit, if one exists, of the ratio ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) (as in the ratio test cvgdvgrat 36526) as k increases. Then the radius of convergence of power series sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) is ( 1 / L ) if L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- D = ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. NN0 )   &    |- ( ( ph /\ k e. Z ) -> ( A ` k ) =/= 0 )   &    |- ( ph -> D ~~> L )   &    |- ( ph -> L =/= 0 )   =>    |- ( ph -> R = ( 1 / L ) )
21.27.3  Multiples
Theorem	reldvds 36528	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- Rel ||
Theorem	nznngen 36529	All positive integers in the set of multiples of n, nℤ, are the absolute value of n or greater. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> N e. ZZ )   =>    |- ( ph -> ( ( || " { N } ) i^i NN ) C_ ( ZZ>= ` ( abs ` N ) ) )
Theorem	nzss 36530	The set of multiples of m, mℤ, is a subset of those of n, nℤ, iff n divides m. Lemma 2.1(a) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. V )   =>    |- ( ph -> ( ( || " { M } ) C_ ( || " { N } ) <-> N || M ) )
Theorem	nzin 36531	The intersection of the set of multiples of m, mℤ, and those of n, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( ( || " { M } ) i^i ( || " { N } ) ) = ( || " { ( M lcm N ) } ) )
Theorem	nzprmdif 36532	Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> M e. Prime )   &    |- ( ph -> N e. Prime )   &    |- ( ph -> M =/= N )   =>    |- ( ph -> ( ( || " { M } ) \ ( || " { N } ) ) = ( ( || " { M } ) \ ( || " { ( M x. N ) } ) ) )
Theorem	hashnzfz 36533	Special case of hashdvds 14716: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ( ZZ>= ` ( J - 1 ) ) )   =>    |- ( ph -> ( # ` ( ( || " { N } ) i^i ( J ... K ) ) ) = ( ( |_ ` ( K / N ) ) - ( |_ ` ( ( J - 1 ) / N ) ) ) )
Theorem	hashnzfz2 36534	Special case of hashnzfz 36533: the count of multiples in nℤ, n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> N e. ( ZZ>= ` 2 ) )   &    |- ( ph -> K e. NN )   =>    |- ( ph -> ( # ` ( ( || " { N } ) i^i ( 2 ... K ) ) ) = ( |_ ` ( K / N ) ) )
Theorem	hashnzfzclim 36535*	As the upper bound K of the constraint interval ( J ... K ) in hashnzfz 36533 increases, the resulting count of multiples tends to ( K / M ) —that is, there are approximately ( K / M ) multiples of M in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ph -> M e. NN )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) ) ~~> ( 1 / M ) )
21.27.4  Function operations
Theorem	caofcan 36536*	Transfer a cancellation law like mulcan 10251 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> T )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x R y ) = ( x R z ) <-> y = z ) )   =>    |- ( ph -> ( ( F oF R G ) = ( F oF R H ) <-> G = H ) )
Theorem	ofsubid 36537	Function analog of subid 9895. (Contributed by Steve Rodriguez, 5-Nov-2015.)
|- ( ( A e. V /\ F : A --> CC ) -> ( F oF - F ) = ( A X. { 0 } ) )
Theorem	ofmul12 36538	Function analog of mul12 9801. (Contributed by Steve Rodriguez, 13-Nov-2015.)
|- ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> CC /\ H : A --> CC ) ) -> ( F oF x. ( G oF x. H ) ) = ( G oF x. ( F oF x. H ) ) )
Theorem	ofdivrec 36539	Function analog of divrec 10288, a division analog of ofnegsub 10609. (Contributed by Steve Rodriguez, 3-Nov-2015.)
|- ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( F oF x. ( ( A X. { 1 } ) oF / G ) ) = ( F oF / G ) )
Theorem	ofdivcan4 36540	Function analog of divcan4 10297. (Contributed by Steve Rodriguez, 4-Nov-2015.)
|- ( ( A e. V /\ F : A --> CC /\ G : A --> ( CC \ { 0 } ) ) -> ( ( F oF x. G ) oF / G ) = F )
Theorem	ofdivdiv2 36541	Function analog of divdiv2 10321. (Contributed by Steve Rodriguez, 23-Nov-2015.)
|- ( ( ( A e. V /\ F : A --> CC ) /\ ( G : A --> ( CC \ { 0 } ) /\ H : A --> ( CC \ { 0 } ) ) ) -> ( F oF / ( G oF / H ) ) = ( ( F oF x. H ) oF / G ) )
21.27.5  Calculus
Theorem	lhe4.4ex1a 36542	Example of the Fundamental Theorem of Calculus, part two (ftc2 22988): S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 ). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 22988 as simply the "Fundamental Theorem of Calculus", then ftc1 22986 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.)
|- S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 )
Theorem	dvsconst 36543	Derivative of a constant function on the real or complex numbers. The function may return a complex A even if S is RR. (Contributed by Steve Rodriguez, 11-Nov-2015.)
|- ( ( S e. { RR , CC } /\ A e. CC ) -> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) )
Theorem	dvsid 36544	Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.)
|- ( S e. { RR , CC } -> ( S _D ( _I |` S ) ) = ( S X. { 1 } ) )
Theorem	dvsef 36545	Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.)
|- ( S e. { RR , CC } -> ( S _D ( exp |` S ) ) = ( exp |` S ) )
Theorem	expgrowthi 36546*	Exponential growth and decay model. See expgrowth 36548 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> K e. CC )   &    |- ( ph -> C e. CC )   &    |- Y = ( t e. S |-> ( C x. ( exp ` ( K x. t ) ) ) )   =>    |- ( ph -> ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) )
Theorem	dvconstbi 36547*	The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analog of dvconst 22863 and dveq0 22944. Corresponds to integration formula " S. 0 _d x = C " in section 4.1 of [LarsonHostetlerEdwards] p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> Y : S --> CC )   &    |- ( ph -> dom ( S _D Y ) = S )   =>    |- ( ph -> ( ( S _D Y ) = ( S X. { 0 } ) <-> E. c e. CC Y = ( S X. { c } ) ) )
Theorem	expgrowth 36548*	Exponential growth and decay model. The derivative of a function y of variable t equals a constant k times y itself, iff y equals some constant C times the exponential of kt. This theorem and expgrowthi 36546 illustrate one of the simplest and most crucial classes of differential equations, equations that relate functions to their derivatives. Section 6.3 of [Strang] p. 242 calls y' = ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as the Malthusian growth model or exponential law, and C, k, and t correspond to initial population size, growth rate, and time respectively (https://en.wikipedia.org/wiki/Malthusian_growth_model); and in finance, the model appears in a similar role in continuous compounding with C as the initial amount of money. In exponential decay models, k is often expressed as the negative of a positive constant λ. Here y' is given as ( S _D Y ), C as c, and ky as ( ( S X. { K } ) oF x. Y ). ( S X. { K } ) is the constant function that maps any real or complex input to k and oF x. is multiplication as a function operation. The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of [LarsonHostetlerEdwards] p. 375 (which notes " C is the initial value of y, and k is the proportionality constant. Exponential growth occurs when k > 0, and exponential decay occurs when k < 0."); its proof here closely follows the proof of y' = y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case. Statements for this and expgrowthi 36546 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> K e. CC )   &    |- ( ph -> Y : S --> CC )   &    |- ( ph -> dom ( S _D Y ) = S )   =>    |- ( ph -> ( ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) <-> E. c e. CC Y = ( t e. S |-> ( c x. ( exp ` ( K x. t ) ) ) ) ) )
21.27.6  The generalized binomial coefficient operation
Syntax	cbcc 36549	Extend class notation to include the generalized binomial coefficient operation.
class C𝑐
Definition	df-bcc 36550*	Define a generalized binomial coefficient operation, which unlike df-bc 12489 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- C𝑐 = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) )
Theorem	bccval 36551	Value of the generalized binomial coefficient, C choose K. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   &    |- ( ph -> K e. NN0 )   =>    |- ( ph -> ( CC𝑐 K ) = ( ( C FallFac K ) / ( ! ` K ) ) )
Theorem	bcccl 36552	Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   &    |- ( ph -> K e. NN0 )   =>    |- ( ph -> ( CC𝑐 K ) e. CC )
Theorem	bcc0 36553	The generalized binomial coefficient C choose K is zero iff C is an integer between zero and ( K - 1 ) inclusive. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   &    |- ( ph -> K e. NN0 )   =>    |- ( ph -> ( ( CC𝑐 K ) = 0 <-> C e. ( 0 ... ( K - 1 ) ) ) )
Theorem	bccp1k 36554	Generalized binomial coefficient: C choose ( K + 1 ). (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   &    |- ( ph -> K e. NN0 )   =>    |- ( ph -> ( CC𝑐 ( K + 1 ) ) = ( ( CC𝑐 K ) x. ( ( C - K ) / ( K + 1 ) ) ) )
Theorem	bccm1k 36555	Generalized binomial coefficient: C choose ( K - 1 ), when C is not ( K - 1 ). (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. ( CC \ { ( K - 1 ) } ) )   &    |- ( ph -> K e. NN )   =>    |- ( ph -> ( CC𝑐 ( K - 1 ) ) = ( ( CC𝑐 K ) / ( ( C - ( K - 1 ) ) / K ) ) )
Theorem	bccn0 36556	Generalized binomial coefficient: C choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 0 ) = 1 )
Theorem	bccn1 36557	Generalized binomial coefficient: C choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 1 ) = C )
Theorem	bccbc 36558	The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> K e. NN0 )   =>    |- ( ph -> ( NC𝑐 K ) = ( N _C K ) )
21.27.7  Binomial series
Theorem	uzmptshftfval 36559*	When F is a maps-to function on some set of upper integers Z that returns a set B, ( F shift N ) is another maps-to function on the shifted set of upper integers W. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- F = ( x e. Z |-> B )   &    |- B e. _V   &    |- ( x = ( y - N ) -> B = C )   &    |- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` ( M + N ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( F shift N ) = ( y e. W |-> C ) )
Theorem	dvradcnv2 36560*	The radius of convergence of the (formal) derivative H of the power series G is (at least) as large as the radius of convergence of G. This version of dvradcnv 23368 uses a shifted version of H to match the sum form of ( CC _D F ) in pserdv2 23377 (and shows how to use uzmptshftfval 36559 to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- H = ( n e. NN |-> ( ( n x. ( A ` n ) ) x. ( X ^ ( n - 1 ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> ( abs ` X ) < R )   =>    |- ( ph -> seq 1 ( + , H ) e. dom ~~> )
Theorem	binomcxplemwb 36561	Lemma for binomcxp 36570. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   &    |- ( ph -> K e. NN )   =>    |- ( ph -> ( ( ( C - K ) x. ( CC𝑐 K ) ) + ( ( C - ( K - 1 ) ) x. ( CC𝑐 ( K - 1 ) ) ) ) = ( C x. ( CC𝑐 K ) ) )
Theorem	binomcxplemnn0 36562*	Lemma for binomcxp 36570. When C is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 13881 equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set ( 0 ... C ), and when the index set is widened beyond C the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   =>    |- ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( CC𝑐 k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
Theorem	binomcxplemrat 36563*	Lemma for binomcxp 36570. As k increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ~~> 1 )
Theorem	binomcxplemfrat 36564*	Lemma for binomcxp 36570. binomcxplemrat 36563 implies that when C is not a nonnegative integer, the absolute value of the ratio ( ( F ` ( k + 1 ) ) / ( F ` k ) ) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   &    |- F = ( j e. NN0 |-> ( CC𝑐 j ) )   =>    |- ( ( ph /\ -. C e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) ~~> 1 )
Theorem	binomcxplemradcnv 36565*	Lemma for binomcxp 36570. By binomcxplemfrat 36564 and radcnvrat 36527 the radius of convergence of power series sum_ k e. NN0 ( ( F ` k ) x. ( b ^ k ) ) is one. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   &    |- F = ( j e. NN0 |-> ( CC𝑐 j ) )   &    |- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )   =>    |- ( ( ph /\ -. C e. NN0 ) -> R = 1 )
Theorem	binomcxplemdvbinom 36566*	Lemma for binomcxp 36570. By the power and chain rules, calculate the derivative of ( ( 1 + b ) ^c -u C ), with respect to b in the disk of convergence D. We later multiply the derivative in the later binomcxplemdvsum 36568 by this derivative to show that ( ( 1 + b ) ^c C ) (with a non-negated C) and the later sum, since both at b = 0 equal one, are the same. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   &    |- F = ( j e. NN0 |-> ( CC𝑐 j ) )   &    |- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )   &    |- E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )   &    |- D = ( `' abs " ( 0 [,) R ) )   =>    |- ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( b e. D |-> ( ( 1 + b ) ^c -u C ) ) ) = ( b e. D |-> ( -u C x. ( ( 1 + b ) ^c ( -u C - 1 ) ) ) ) )
Theorem	binomcxplemcvg 36567*	Lemma for binomcxp 36570. The sum in binomcxplemnn0 36562 and its derivative (see the next theorem, binomcxplemdvsum 36568) converge, as long as their base J is within the disk of convergence. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   &    |- F = ( j e. NN0 |-> ( CC𝑐 j ) )   &    |- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )   &    |- E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )   &    |- D = ( `' abs " ( 0 [,) R ) )   =>    |- ( ( ph /\ J e. D ) -> ( seq 0 ( + , ( S ` J ) ) e. dom ~~> /\ seq 1 ( + , ( E ` J ) ) e. dom ~~> ) )
Theorem	binomcxplemdvsum 36568*	Lemma for binomcxp 36570. The derivative of the generalized sum in binomcxplemnn0 36562. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   &    |- F = ( j e. NN0 |-> ( CC𝑐 j ) )   &    |- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )   &    |- E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )   &    |- D = ( `' abs " ( 0 [,) R ) )   &    |- P = ( b e. D |-> sum_ k e. NN0 ( ( S ` b ) ` k ) )   =>    |- ( ph -> ( CC _D P ) = ( b e. D |-> sum_ k e. NN ( ( E ` b ) ` k ) ) )
Theorem	binomcxplemnotnn0 36569*	Lemma for binomcxp 36570. When C is not a nonnegative integer, the generalized sum in binomcxplemnn0 36562 —which we will call P —is a convergent power series: its base b is always of smaller absolute value than the radius of convergence. pserdv2 23377 gives the derivative of P, which by dvradcnv 23368 also converges in that radius. When A is fixed at one, ( A + b ) times that derivative equals ( C x. P ) and fraction ( P / ( ( A + b ) ^c C ) ) is always defined with derivative zero, so the fraction is a constant—specifically one, because ( ( 1 + 0 ) ^c C ) = 1. Thus ( ( 1 + b ) ^c C ) = ( P ` b ). Finally, let b be ( B / A ), and multiply both the binomial ( ( 1 + ( B / A ) ) ^c C ) and the sum ( P ` ( B / A ) ) by ( A ^c C ) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   &    |- F = ( j e. NN0 |-> ( CC𝑐 j ) )   &    |- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )   &    |- E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )   &    |- D = ( `' abs " ( 0 [,) R ) )   &    |- P = ( b e. D |-> sum_ k e. NN0 ( ( S ` b ) ` k ) )   =>    |- ( ( ph /\ -. C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( CC𝑐 k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
Theorem	binomcxp 36570*	Generalize the binomial theorem binom 13881 to positive real summand A, real summand B, and complex exponent C. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus; see also https://en.wikipedia.org/wiki/Binomial_series, https://en.wikipedia.org/wiki/Binomial_theorem (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` B ) < ( abs ` A ) )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( CC𝑐 k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
21.28  Mathbox for Andrew Salmon
21.28.1  Principia Mathematica * 10
Theorem	pm10.12 36571*	Theorem *10.12 in [WhiteheadRussell] p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x ( ph \/ ps ) -> ( ph \/ A. x ps ) )
Theorem	pm10.14 36572	Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( ( A. x ph /\ A. x ps ) -> ( [ y / x ] ph /\ [ y / x ] ps ) )
Theorem	pm10.251 36573	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x -. ph -> -. A. x ph )
Theorem	pm10.252 36574	Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.)
|- ( -. E. x ph <-> A. x -. ph )
Theorem	pm10.253 36575	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( -. A. x ph <-> E. x -. ph )
Theorem	albitr 36576	Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x ( ph <-> ps ) /\ A. x ( ps <-> ch ) ) -> A. x ( ph <-> ch ) )
Theorem	pm10.42 36577	Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( ( E. x ph \/ E. x ps ) <-> E. x ( ph \/ ps ) )
Theorem	pm10.52 36578*	Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x ph -> ( A. x ( ph -> ps ) <-> ps ) )
Theorem	pm10.53 36579	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x ph -> A. x ( ph -> ps ) )
Theorem	pm10.541 36580*	Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ch \/ ps ) ) <-> ( ch \/ A. x ( ph -> ps ) ) )
Theorem	pm10.542 36581*	Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ch -> ps ) ) <-> ( ch -> A. x ( ph -> ps ) ) )
Theorem	pm10.55 36582	Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( E. x ( ph /\ ps ) /\ A. x ( ph -> ps ) ) <-> ( E. x ph /\ A. x ( ph -> ps ) ) )
Theorem	pm10.56 36583	Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x ( ph -> ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ps /\ ch ) )
Theorem	pm10.57 36584	Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ps \/ ch ) ) -> ( A. x ( ph -> ps ) \/ E. x ( ph /\ ch ) ) )
21.28.2  Principia Mathematica * 11
Theorem	2alanimi 36585	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( A. x A. y ph /\ A. x A. y ps ) -> A. x A. y ch )
Theorem	2al2imi 36586	Removes two universal qunatifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( A. x A. y ph -> ( A. x A. y ps -> A. x A. y ch ) )
Theorem	pm11.11 36587	Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ph   =>    |- A. z A. w [ z / x ] [ w / y ] ph
Theorem	pm11.12 36588*	Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x A. y ( ph \/ ps ) -> ( ph \/ A. x A. y ps ) )
Theorem	19.21vv 36589*	Compare theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1776. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ps -> ph ) <-> ( ps -> A. x A. y ph ) )
Theorem	2alim 36590	Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph -> ps ) -> ( A. x A. y ph -> A. x A. y ps ) )
Theorem	2albi 36591	Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph <-> ps ) -> ( A. x A. y ph <-> A. x A. y ps ) )
Theorem	2exim 36592	Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph -> ps ) -> ( E. x E. y ph -> E. x E. y ps ) )
Theorem	2exbi 36593	Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph <-> ps ) -> ( E. x E. y ph <-> E. x E. y ps ) )
Theorem	spsbce-2 36594	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( [ z / x ] [ w / y ] ph -> E. x E. y ph )
Theorem	19.33-2 36595	Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x A. y ph \/ A. x A. y ps ) -> A. x A. y ( ph \/ ps ) )
Theorem	19.36vv 36596*	Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.)
|- ( E. x E. y ( ph -> ps ) <-> ( A. x A. y ph -> ps ) )
Theorem	19.31vv 36597*	Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph \/ ps ) <-> ( A. x A. y ph \/ ps ) )
Theorem	19.37vv 36598*	Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ps -> ph ) <-> ( ps -> E. x E. y ph ) )
Theorem	19.28vv 36599*	Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ps /\ ph ) <-> ( ps /\ A. x A. y ph ) )
Theorem	pm11.52 36600	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ph /\ ps ) <-> -. A. x A. y ( ph -> -. ps ) )