P. 367 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36601-36700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	extoimad 36601*	If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ C )   =>    |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ C )
Theorem	imo72b2lem0 36602*	Lemma for imo72b2 36613. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   =>    |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
Theorem	suprleubrd 36603*	Natural deduction form of specialized suprleub 10570. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A. z e. A z <_ B )   =>    |- ( ph -> sup ( A , RR , < ) <_ B )
Theorem	imo72b2lem2 36604*	Lemma for imo72b2 36613. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A. z e. RR ( abs ` ( F ` z ) ) <_ C )   =>    |- ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) <_ C )
Theorem	syldbl2 36605	Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ ps ) -> ( ps -> th ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	funfvima2d 36606	A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : A --> B )   =>    |- ( ( ph /\ x e. A ) -> ( F ` x ) e. ( F " A ) )
Theorem	suprlubrd 36607*	Natural deduction form of specialized suprlub 10568. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- ( ph -> E. z e. A B < z )   =>    |- ( ph -> B < sup ( A , RR , < ) )
Theorem	imo72b2lem1 36608*	Lemma for imo72b2 36613. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   =>    |- ( ph -> 0 < sup ( ( abs " ( F " RR ) ) , RR , < ) )
Theorem	lemuldiv3d 36609	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( B x. A ) <_ C )   &    |- ( ph -> 0 < A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> B <_ ( C / A ) )
Theorem	lemuldiv4d 36610	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> B <_ ( C / A ) )   &    |- ( ph -> 0 < A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B x. A ) <_ C )
Theorem	hypstkd 36611	Natural deductionm, stacks an hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   &    |- ( ph -> ch )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	rspcdvinvd 36612*	If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   &    |- ( ph -> A e. B )   &    |- ( ph -> A. x e. B ps )   =>    |- ( ph -> ch )
Theorem	imo72b2 36613*	IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   &    |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )   =>    |- ( ph -> ( abs ` ( G ` B ) ) <_ 1 )
21.26.2  INT Inequalities Proof Generator This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 9641 1red 9655 readdcld 9667 remulcld 9668 eqcomd 2456.
Theorem	int-addcomd 36614	AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B + C ) = ( C + A ) )
Theorem	int-addassocd 36615	AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B + ( C + D ) ) = ( ( A + C ) + D ) )
Theorem	int-addsimpd 36616	AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> 0 = ( A - B ) )
Theorem	int-mulcomd 36617	MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. C ) = ( C x. A ) )
Theorem	int-mulassocd 36618	MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. ( C x. D ) ) = ( ( A x. C ) x. D ) )
Theorem	int-mulsimpd 36619	MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> 1 = ( A / B ) )
Theorem	int-leftdistd 36620	AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( ( C + D ) x. B ) = ( ( C x. A ) + ( D x. A ) ) )
Theorem	int-rightdistd 36621	AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. ( C + D ) ) = ( ( A x. C ) + ( A x. D ) ) )
Theorem	int-sqdefd 36622	SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A x. B ) = ( A ^ 2 ) )
Theorem	int-mul11d 36623	First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A x. 1 ) = B )
Theorem	int-mul12d 36624	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( 1 x. A ) = B )
Theorem	int-add01d 36625	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 36626	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 36627	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 36628	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A + C ) = ( B + D ) )
Theorem	int-eqtransd 36629	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	int-eqmvtd 36630	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 36631	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> B <_ A )
Theorem	int-ineqmvtd 36632	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 36633	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 36634	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 36635	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 11062 addcomli 9822 00id 9805 addid1i 9817 addid2i 9818 eqid 2450 dec0h 11064 decadd 11089 decaddc 11090.
Theorem	unitadd 36636	Theorem used in conjunction with decaddc 11090 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 36637	5 + 5 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 5 + 5 ) = ; 1 0
Theorem	6p4e10b 36638	6 + 4 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 6 + 4 ) = ; 1 0
Theorem	7p3e10b 36639	7 + 3 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 7 + 3 ) = ; 1 0
Theorem	8p2e10b 36640	8 + 2 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 8 + 2 ) = ; 1 0
Theorem	9p1e10b 36641	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 36642	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 36643	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 36644	Arithmetic-geometric mean inequality for n = 2, derived from amgmlem 23908. (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 36645	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 36646	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 36647	'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 36648	Union of two disjoint restricted class abstractions; compare unrab 3713. (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 36649	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 36650	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 36651	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 36652	The infinity ball in the absolute value metric is just the whole space. S analogue of blpnf 21405. (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 36653*	The primes are unbounded. This generalizes prmunb 14851 to real A with arch 10863 and lttrd 9793: 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 36654*	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 36655*	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 36656*	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 36655 directly uses the limit of the ratio. (It also demonstrates how to use climi2 13568 and absltd 13484 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 2931 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 2878 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 36657*	Let L be the limit, if one exists, of the ratio ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) (as in the ratio test cvgdvgrat 36656) 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 36658	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- Rel ||
Theorem	nznngen 36659	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 36660	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 36661	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 36662	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 36663	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 36664	Special case of hashnzfz 36663: 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 36665*	As the upper bound K of the constraint interval ( J ... K ) in hashnzfz 36663 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 36666*	Transfer a cancellation law like mulcan 10246 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 36667	Function analogue of subid 9890. (Contributed by Steve Rodriguez, 5-Nov-2015.)
|- ( ( A e. V /\ F : A --> CC ) -> ( F oF - F ) = ( A X. { 0 } ) )
Theorem	ofmul12 36668	Function analogue of mul12 9796. (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 36669	Function analogue of divrec 10283, a division analogue of ofnegsub 10604. (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 36670	Function analogue of divcan4 10292. (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 36671	Function analogue of divdiv2 10316. (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 36672	Example of the Fundamental Theorem of Calculus, part two (ftc2 22989): S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 ). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 22989 as simply the "Fundamental Theorem of Calculus", then ftc1 22987 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 36673	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 36674	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 36675	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 36676*	Exponential growth and decay model. See expgrowth 36678 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 36677*	The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analogue of dvconst 22864 and dveq0 22945. 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 36678*	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 36676 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 36676 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 36679	Extend class notation to include the generalized binomial coefficient operation.
class C𝑐
Definition	df-bcc 36680*	Define a generalized binomial coefficient operation, which unlike df-bc 12485 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 36681	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 36682	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 36683	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 36684	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 36685	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 36686	Generalized binomial coefficient: C choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 0 ) = 1 )
Theorem	bccn1 36687	Generalized binomial coefficient: C choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 1 ) = C )
Theorem	bccbc 36688	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 36689*	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 36690*	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 23369 uses a shifted version of H to match the sum form of ( CC _D F ) in pserdv2 23378 (and shows how to use uzmptshftfval 36689 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 36691	Lemma for binomcxp 36700. 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 36692*	Lemma for binomcxp 36700. 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 36693*	Lemma for binomcxp 36700. 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 36694*	Lemma for binomcxp 36700. binomcxplemrat 36693 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 36695*	Lemma for binomcxp 36700. By binomcxplemfrat 36694 and radcnvrat 36657 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 36696*	Lemma for binomcxp 36700. 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 36698 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 36697*	Lemma for binomcxp 36700. The sum in binomcxplemnn0 36692 and its derivative (see the next theorem, binomcxplemdvsum 36698) 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 36698*	Lemma for binomcxp 36700. The derivative of the generalized sum in binomcxplemnn0 36692. 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 36699*	Lemma for binomcxp 36700. When C is not a nonnegative integer, the generalized sum in binomcxplemnn0 36692 —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 23378 gives the derivative of P, which by dvradcnv 23369 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 36700*	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 ) ) ) )