P. 368 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	int-add01d 36701	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A + 0 ) = B )
Theorem	int-add02d 36702	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( 0 + A ) = B )
Theorem	int-sqgeq0d 36703	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> 0 <_ ( A x. B ) )
Theorem	int-eqprincd 36704	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A + C ) = ( B + D ) )
Theorem	int-eqtransd 36705	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	int-eqmvtd 36706	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   &    |- ( ph -> A = ( C + D ) )   =>    |- ( ph -> C = ( B - D ) )
Theorem	int-eqineqd 36707	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> B <_ A )
Theorem	int-ineqmvtd 36708	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 36709	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 36710	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 36711	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 11088 addcomli 9843 00id 9826 addid1i 9838 addid2i 9839 eqid 2471 dec0h 11090 decadd 11115 decaddc 11116.
Theorem	unitadd 36712	Theorem used in conjunction with decaddc 11116 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 36713	5 + 5 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 5 + 5 ) = ; 1 0
Theorem	6p4e10b 36714	6 + 4 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 6 + 4 ) = ; 1 0
Theorem	7p3e10b 36715	7 + 3 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 7 + 3 ) = ; 1 0
Theorem	8p2e10b 36716	8 + 2 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 8 + 2 ) = ; 1 0
Theorem	9p1e10b 36717	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 36718	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 36719	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 36720	Arithmetic-geometric mean inequality for n = 2, derived from amgmlem 23994. (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 36721	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 36722	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 36723	'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 36724	Union of two disjoint restricted class abstractions; compare unrab 3705. (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 36725	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 36726	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 36727	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 36728	The infinity ball in the absolute value metric is just the whole space. S analogue of blpnf 21490. (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 36729*	The primes are unbounded. This generalizes prmunb 14937 to real A with arch 10890 and lttrd 9813: 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 36730*	One need only check prime divisors of P up to sqr P in order to ensure primality. This version of isprm5 14730 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 36731*	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 36732*	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 14016 and dvgrat 36731 directly uses the limit of the ratio. (It also demonstrates how to use climi2 13652 and absltd 13568 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 2918 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 2871 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 36733*	Let L be the limit, if one exists, of the ratio ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) (as in the ratio test cvgdvgrat 36732) 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 36734	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- Rel ||
Theorem	nznngen 36735	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 36736	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 36737	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 36738	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 36739	Special case of hashdvds 14802: 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 36740	Special case of hashnzfz 36739: 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 36741*	As the upper bound K of the constraint interval ( J ... K ) in hashnzfz 36739 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 36742*	Transfer a cancellation law like mulcan 10271 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 36743	Function analogue of subid 9913. (Contributed by Steve Rodriguez, 5-Nov-2015.)
|- ( ( A e. V /\ F : A --> CC ) -> ( F oF - F ) = ( A X. { 0 } ) )
Theorem	ofmul12 36744	Function analogue of mul12 9817. (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 36745	Function analogue of divrec 10308, a division analogue of ofnegsub 10629. (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 36746	Function analogue of divcan4 10317. (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 36747	Function analogue of divdiv2 10341. (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 36748	Example of the Fundamental Theorem of Calculus, part two (ftc2 23075): S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 ). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 23075 as simply the "Fundamental Theorem of Calculus", then ftc1 23073 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 36749	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 36750	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 36751	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 36752*	Exponential growth and decay model. See expgrowth 36754 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 36753*	The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analogue of dvconst 22950 and dveq0 23031. 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 36754*	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 36752 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 36752 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 36755	Extend class notation to include the generalized binomial coefficient operation.
class C𝑐
Definition	df-bcc 36756*	Define a generalized binomial coefficient operation, which unlike df-bc 12526 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 36757	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 36758	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 36759	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 36760	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 36761	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 36762	Generalized binomial coefficient: C choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 0 ) = 1 )
Theorem	bccn1 36763	Generalized binomial coefficient: C choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 1 ) = C )
Theorem	bccbc 36764	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 36765*	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 36766*	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 23455 uses a shifted version of H to match the sum form of ( CC _D F ) in pserdv2 23464 (and shows how to use uzmptshftfval 36765 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 36767	Lemma for binomcxp 36776. 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 36768*	Lemma for binomcxp 36776. When C is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 13965 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 36769*	Lemma for binomcxp 36776. 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 36770*	Lemma for binomcxp 36776. binomcxplemrat 36769 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 36771*	Lemma for binomcxp 36776. By binomcxplemfrat 36770 and radcnvrat 36733 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 36772*	Lemma for binomcxp 36776. 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 36774 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 36773*	Lemma for binomcxp 36776. The sum in binomcxplemnn0 36768 and its derivative (see the next theorem, binomcxplemdvsum 36774) 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 36774*	Lemma for binomcxp 36776. The derivative of the generalized sum in binomcxplemnn0 36768. 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 36775*	Lemma for binomcxp 36776. When C is not a nonnegative integer, the generalized sum in binomcxplemnn0 36768 —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 23464 gives the derivative of P, which by dvradcnv 23455 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 36776*	Generalize the binomial theorem binom 13965 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 36777*	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 36778	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 36779	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x -. ph -> -. A. x ph )
Theorem	pm10.252 36780	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 36781	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( -. A. x ph <-> E. x -. ph )
Theorem	albitr 36782	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 36783	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 36784*	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 36785	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x ph -> A. x ( ph -> ps ) )
Theorem	pm10.541 36786*	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 36787*	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 36788	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 36789	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 36790	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 36791	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 36792	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	pm11.11 36793	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 36794*	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 36795*	Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1794. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ps -> ph ) <-> ( ps -> A. x A. y ph ) )
Theorem	2alim 36796	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 36797	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 36798	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 36799	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 36800	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( [ z / x ] [ w / y ] ph -> E. x E. y ph )