P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	int-eqmvtd 36001	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 36002	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> B <_ A )
Theorem	int-ineqmvtd 36003	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 36004	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 36005	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 36006	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 11032 addcomli 9805 00id 9788 addid1i 9800 addid2i 9801 eqid 2402 dec0h 11034 decadd 11059 decaddc 11060.
Theorem	unitadd 36007	Theorem used in conjunction with decaddc 11060 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 36008	5 + 5 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 5 + 5 ) = ; 1 0
Theorem	6p4e10b 36009	6 + 4 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 6 + 4 ) = ; 1 0
Theorem	7p3e10b 36010	7 + 3 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 7 + 3 ) = ; 1 0
Theorem	8p2e10b 36011	8 + 2 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 8 + 2 ) = ; 1 0
Theorem	9p1e10b 36012	9 + 1 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 9 + 1 ) = ; 1 0
21.27  Mathbox for Steve Rodriguez
21.27.1  Miscellanea
Theorem	nanorxor 36013	'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 36014	Union of two disjoint restricted class abstractions; compare unrab 3720. (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 36015	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 36016	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 36017	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 36018	The infinity ball in the absolute value metric is just the whole space. S analog of blpnf 21190. (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 36019*	The primes are unbounded. This generalizes prmunb 14639 to real A with arch 10832 and lttrd 9776: 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 36020*	One need only check prime divisors of P up to sqr P in order to ensure primality. This version of isprm5 14460 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 36021*	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 36022*	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 13842 and dvgrat 36021 directly uses the limit of the ratio. (It also demonstrates how to use climi2 13481 and absltd 13408 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 2948 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 2895 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 36023*	Let L be the limit, if one exists, of the ratio ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) (as in the ratio test cvgdvgrat 36022) 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  The least common multiple operator
Syntax	clcm 36024	Extend the definition of a class to include the least common multiple operator.
class lcm
Definition	df-lcm 36025*	Define the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , sup ( { n e. NN | ( x || n /\ y || n ) } , RR , `' < ) ) )
Theorem	lcmval 36026*	Value of the lcm operator. ( M lcm N ) is the least common multiple of M and N. If either M or N is 0, the result is defined conventionally as 0. Contrast with df-gcd 14352 and gcdval 14353. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , sup ( { n e. NN | ( M || n /\ N || n ) } , RR , `' < ) ) )
Theorem	lcmcom 36027	The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = ( N lcm M ) )
Theorem	lcm0val 36028	The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 36027 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( M e. ZZ -> ( M lcm 0 ) = 0 )
Theorem	lcmn0val 36029*	The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = sup ( { n e. NN | ( M || n /\ N || n ) } , RR , `' < ) )
Theorem	lcmcllem 36030*	Lemma for lcmn0cl 36031 and dvdslcm 36032. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } )
Theorem	lcmn0cl 36031	Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN )
Theorem	dvdslcm 36032	The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
Theorem	lcmledvds 36033	A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) <_ K ) )
Theorem	lcmeq0 36034	The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = 0 <-> ( M = 0 \/ N = 0 ) ) )
Theorem	lcmcl 36035	Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
Theorem	gcddvdslcm 36036	The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || ( M lcm N ) )
Theorem	lcmneg 36037	Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm -u N ) = ( M lcm N ) )
Theorem	neglcm 36038	Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M lcm N ) = ( M lcm N ) )
Theorem	lcmabs 36039	The lcm of two integers is the same as that of their absolute values. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
Theorem	lcmgcdlem 36040	Lemma for lcmgcd 36041 and lcmdvds 36042. Prove them for positive M, N, and K. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. NN /\ N e. NN ) -> ( ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) /\ ( ( K e. NN /\ ( M || K /\ N || K ) ) -> ( M lcm N ) || K ) ) )
Theorem	lcmgcd 36041	The product of two numbers' least common multiple and greatest common divisor is the absolute value of the product of the two numbers. In particular, that absolute value is the least common multiple of two coprime numbers, for which ( M gcd N ) = 1. Multiple methods exist for proving this, and it is often proven either as a consequence of the fundamental theorem of arithmetic 1arith 14652 or of Bézout's identity bezout 14387; see e.g. https://proofwiki.org/wiki/Product_of_GCD_and_LCM and https://math.stackexchange.com/a/470827. This proof uses the latter to first confirm it for positive integer M and N (the "Second Proof" in the above Stack Exchange page), then shows that implies it for all nonzero integer inputs, then finally uses lcm0val 36028 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) )
Theorem	lcmdvds 36042	The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
Theorem	lcmid 36043	The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( M e. ZZ -> ( M lcm M ) = ( abs ` M ) )
Theorem	lcmgcdeq 36044	Two integers' absolute values are equal iff their least common multiple and greatest common divisor are equal. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = ( M gcd N ) <-> ( abs ` M ) = ( abs ` N ) ) )
Theorem	lcmdvdsb 36045	Biconditional form of lcmdvds 36042. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) <-> ( M lcm N ) || K ) )
Theorem	lcmass 36046	Associative law for lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) lcm P ) = ( N lcm ( M lcm P ) ) )
Theorem	3lcm2e6 36047	The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( 3 lcm 2 ) = 6
21.27.4  Multiples
Theorem	reldvds 36048	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- Rel ||
Theorem	nznngen 36049	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 36050	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 36051	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 36052	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 36053	Special case of hashdvds 14512: 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 36054	Special case of hashnzfz 36053: 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 36055*	As the upper bound K of the constraint interval ( J ... K ) in hashnzfz 36053 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.5  Function operations
Theorem	caofcan 36056*	Transfer a cancellation law like mulcan 10226 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 36057	Function analog of subid 9873. (Contributed by Steve Rodriguez, 5-Nov-2015.)
|- ( ( A e. V /\ F : A --> CC ) -> ( F oF - F ) = ( A X. { 0 } ) )
Theorem	ofmul12 36058	Function analog of mul12 9779. (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 36059	Function analog of divrec 10263, a division analog of ofnegsub 10573. (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 36060	Function analog of divcan4 10272. (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 36061	Function analog of divdiv2 10296. (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.6  Calculus
Theorem	lhe4.4ex1a 36062	Example of the Fundamental Theorem of Calculus, part two (ftc2 22735): S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 ). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 22735 as simply the "Fundamental Theorem of Calculus", then ftc1 22733 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 36063	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 36064	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 36065	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 36066*	Exponential growth and decay model. See expgrowth 36068 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 36067*	The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analog of dvconst 22610 and dveq0 22691. 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 36068*	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 36066 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 36066 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.7  The generalized binomial coefficient operation
Syntax	cbcc 36069	Extend class notation to include the generalized binomial coefficient operation.
class C𝑐
Definition	df-bcc 36070*	Define a generalized binomial coefficient operation, which unlike df-bc 12423 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 36071	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 36072	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 36073	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 36074	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 36075	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 36076	Generalized binomial coefficient: C choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 0 ) = 1 )
Theorem	bccn1 36077	Generalized binomial coefficient: C choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
|- ( ph -> C e. CC )   =>    |- ( ph -> ( CC𝑐 1 ) = C )
Theorem	bccbc 36078	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.8  Binomial series
Theorem	uzmptshftfval 36079*	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 36080*	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 23106 uses a shifted version of H to match the sum form of ( CC _D F ) in pserdv2 23115 (and shows how to use uzmptshftfval 36079 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 36081	Lemma for binomcxp 36090. 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 36082*	Lemma for binomcxp 36090. When C is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 13791 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 36083*	Lemma for binomcxp 36090. 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 36084*	Lemma for binomcxp 36090. binomcxplemrat 36083 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 36085*	Lemma for binomcxp 36090. By binomcxplemfrat 36084 and radcnvrat 36023 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 36086*	Lemma for binomcxp 36090. 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 36088 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 36087*	Lemma for binomcxp 36090. The sum in binomcxplemnn0 36082 and its derivative (see the next theorem, binomcxplemdvsum 36088) 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 36088*	Lemma for binomcxp 36090. The derivative of the generalized sum in binomcxplemnn0 36082. 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 36089*	Lemma for binomcxp 36090. When C is not a nonnegative integer, the generalized sum in binomcxplemnn0 36082 —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 23115 gives the derivative of P, which by dvradcnv 23106 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 36090*	Generalize the binomial theorem binom 13791 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 36091*	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 36092	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 36093	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x -. ph -> -. A. x ph )
Theorem	pm10.252 36094	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 36095	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( -. A. x ph <-> E. x -. ph )
Theorem	albitr 36096	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 36097	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 36098*	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 36099	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x ph -> A. x ( ph -> ps ) )
Theorem	pm10.541 36100*	Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ch \/ ps ) ) <-> ( ch \/ A. x ( ph -> ps ) ) )