Home | Metamath
Proof Explorer Theorem List (p. 424 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | expandan 42301 | Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β π) & β’ (π β π) β β’ ((π β§ π) β Β¬ (π β Β¬ π)) | ||
Theorem | expandexn 42302 | Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β Β¬ π) β β’ (βπ₯π β Β¬ βπ₯π) | ||
Theorem | expandral 42303 | Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β π) β β’ (βπ₯ β π΄ π β βπ₯(π₯ β π΄ β π)) | ||
Theorem | expandrexn 42304 | Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β Β¬ π) β β’ (βπ₯ β π΄ π β Β¬ βπ₯(π₯ β π΄ β π)) | ||
Theorem | expandrex 42305 | Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β π) β β’ (βπ₯ β π΄ π β Β¬ βπ₯(π₯ β π΄ β Β¬ π)) | ||
Theorem | expanduniss 42306* | Expand βͺ π΄ β π΅ to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (βͺ π΄ β π΅ β βπ₯(π₯ β π΄ β βπ¦(π¦ β π₯ β π¦ β π΅))) | ||
Theorem | ismnuprim 42307* | Express the predicate on π in ismnu 42274 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (βπ§ β π (π« π§ β π β§ βπβπ€ β π (π« π§ β π€ β§ βπ β π§ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) β βπ§(π§ β π β βπ Β¬ βπ€(π€ β π β Β¬ βπ£ Β¬ ((βπ‘(π‘ β π£ β π‘ β π§) β Β¬ (π£ β π β Β¬ π£ β π€)) β Β¬ βπ(π β π§ β (π£ β π β (π β π£ β (π£ β π β Β¬ βπ’(π’ β π β (π β π’ β Β¬ βπ(π β π’ β βπ (π β π β π β π€)))))))))))) | ||
Theorem | rr-grothprimbi 42308* | Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim 42313. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (βπ₯βπ¦ β Univ π₯ β π¦ β βπ₯ Β¬ βπ¦(π₯ β π¦ β Β¬ βπ§(π§ β π¦ β βπ Β¬ βπ€(π€ β π¦ β Β¬ βπ£ Β¬ ((βπ‘(π‘ β π£ β π‘ β π§) β Β¬ (π£ β π¦ β Β¬ π£ β π€)) β Β¬ βπ(π β π§ β (π£ β π¦ β (π β π£ β (π£ β π β Β¬ βπ’(π’ β π β (π β π’ β Β¬ βπ(π β π’ β βπ (π β π β π β π€))))))))))))) | ||
Theorem | inagrud 42309 | Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β πΌ β Inacc) β β’ (π β (π 1βπΌ) β Univ) | ||
Theorem | inaex 42310* | Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π΄ β On β βπ₯ β Inacc π΄ β π₯) | ||
Theorem | gruex 42311* | Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ βπ¦ β Univ π₯ β π¦ | ||
Theorem | rr-groth 42312* | An equivalent of ax-groth 10693 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ βπ¦(π₯ β π¦ β§ βπ§ β π¦ (π« π§ β π¦ β§ βπβπ€ β π¦ (π« π§ β π€ β§ βπ β π§ (βπ£ β π¦ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) | ||
Theorem | rr-grothprim 42313* | An equivalent of ax-groth 10693 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10704 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ Β¬ βπ¦(π₯ β π¦ β Β¬ βπ§(π§ β π¦ β βπ Β¬ βπ€(π€ β π¦ β Β¬ βπ£ Β¬ ((βπ‘(π‘ β π£ β π‘ β π§) β Β¬ (π£ β π¦ β Β¬ π£ β π€)) β Β¬ βπ(π β π§ β (π£ β π¦ β (π β π£ β (π£ β π β Β¬ βπ’(π’ β π β (π β π’ β Β¬ βπ(π β π’ β βπ (π β π β π β π€)))))))))))) | ||
Theorem | ismnushort 42314* | Express the predicate on π and π§ in ismnu 42274 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.) |
β’ (βπ β π« πβπ€ β π (π« π§ β (π β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€)) β (π« π§ β π β§ βπβπ€ β π (π« π§ β π€ β§ βπ β π§ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) | ||
Theorem | dfuniv2 42315* | Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024.) |
β’ Univ = {π¦ β£ βπ§ β π¦ βπ β π« π¦βπ€ β π¦ (π« π§ β (π¦ β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€))} | ||
Theorem | rr-grothshortbi 42316* | Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024.) |
β’ (βπ₯βπ¦ β Univ π₯ β π¦ β βπ₯βπ¦(π₯ β π¦ β§ βπ§ β π¦ βπ β π« π¦βπ€ β π¦ (π« π§ β (π¦ β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€)))) | ||
Theorem | rr-grothshort 42317* | A shorter equivalent of ax-groth 10693 than rr-groth 42312 using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024.) |
β’ βπ¦(π₯ β π¦ β§ βπ§ β π¦ βπ β π« π¦βπ€ β π¦ (π« π§ β (π¦ β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€))) | ||
Theorem | nanorxor 42318 | 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ ((π βΌ π) β ((π β¨ π) β (π β» π))) | ||
Theorem | undisjrab 42319 | Union of two disjoint restricted class abstractions; compare unrab 4264. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ (({π₯ β π΄ β£ π} β© {π₯ β π΄ β£ π}) = β β ({π₯ β π΄ β£ π} βͺ {π₯ β π΄ β£ π}) = {π₯ β π΄ β£ (π β» π)}) | ||
Theorem | iso0 42320 | The empty set is an π , π isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
β’ β Isom π , π (β , β ) | ||
Theorem | ssrecnpr 42321 | β is a subset of both β and β. (Contributed by Steve Rodriguez, 22-Nov-2015.) |
β’ (π β {β, β} β β β π) | ||
Theorem | seff 42322 | Let set π be the real or complex numbers. Then the exponential function restricted to π is a mapping from π to π. (Contributed by Steve Rodriguez, 6-Nov-2015.) |
β’ (π β π β {β, β}) β β’ (π β (exp βΎ π):πβΆπ) | ||
Theorem | sblpnf 42323 | The infinity ball in the absolute value metric is just the whole space. π analogue of blpnf 23672. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
β’ (π β π β {β, β}) & β’ π· = ((abs β β ) βΎ (π Γ π)) β β’ ((π β§ π β π) β (π(ballβπ·)+β) = π) | ||
Theorem | prmunb2 42324* | The primes are unbounded. This generalizes prmunb 16721 to real π΄ with arch 12344 and lttrd 11250: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π΄ β β β βπ β β π΄ < π) | ||
Theorem | dvgrat 42325* | Ratio test for divergence of a complex infinite series. See e.g. remark "if (absβ((πβ(π + 1)) / (πβπ))) β₯ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β 0) & β’ ((π β§ π β π) β (absβ(πΉβπ)) β€ (absβ(πΉβ(π + 1)))) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Theorem | cvgdvgrat 42326* |
Ratio test for convergence and divergence of a complex infinite series.
If the ratio π
of the absolute values of successive
terms in an
infinite sequence πΉ converges to less than one, then the
infinite
sum of the terms of πΉ converges to a complex number; and
if π
converges greater then the sum diverges. This combined form of
cvgrat 15703 and dvgrat 42325 directly uses the limit of the ratio.
(It also demonstrates how to use climi2 15328 and absltd 15249 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15249, and how to use r19.29a 3158 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3151 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3151.) (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β 0) & β’ π = (π β π β¦ (absβ((πΉβ(π + 1)) / (πΉβπ)))) & β’ (π β π β πΏ) & β’ (π β πΏ β 1) β β’ (π β (πΏ < 1 β seqπ( + , πΉ) β dom β )) | ||
Theorem | radcnvrat 42327* | Let πΏ be the limit, if one exists, of the ratio (absβ((π΄β(π + 1)) / (π΄βπ))) (as in the ratio test cvgdvgrat 42326) as π increases. Then the radius of convergence of power series Ξ£π β β0((π΄βπ) Β· (π₯βπ)) is (1 / πΏ) if πΏ is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 42326 βa few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π· = (π β β0 β¦ (absβ((π΄β(π + 1)) / (π΄βπ)))) & β’ π = (β€β₯βπ) & β’ (π β π β β0) & β’ ((π β§ π β π) β (π΄βπ) β 0) & β’ (π β π· β πΏ) & β’ (π β πΏ β 0) β β’ (π β π = (1 / πΏ)) | ||
Theorem | reldvds 42328 | The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ Rel β₯ | ||
Theorem | nznngen 42329 | 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.) |
β’ (π β π β β€) β β’ (π β (( β₯ β {π}) β© β) β (β€β₯β(absβπ))) | ||
Theorem | nzss 42330 | 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.) |
β’ (π β π β β€) & β’ (π β π β π) β β’ (π β (( β₯ β {π}) β ( β₯ β {π}) β π β₯ π)) | ||
Theorem | nzin 42331 | 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.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (( β₯ β {π}) β© ( β₯ β {π})) = ( β₯ β {(π lcm π)})) | ||
Theorem | nzprmdif 42332 | Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β π) β β’ (π β (( β₯ β {π}) β ( β₯ β {π})) = (( β₯ β {π}) β ( β₯ β {(π Β· π)}))) | ||
Theorem | hashnzfz 42333 | Special case of hashdvds 16582: the count of multiples in nβ€ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β β) & β’ (π β π½ β β€) & β’ (π β πΎ β (β€β₯β(π½ β 1))) β β’ (π β (β―β(( β₯ β {π}) β© (π½...πΎ))) = ((ββ(πΎ / π)) β (ββ((π½ β 1) / π)))) | ||
Theorem | hashnzfz2 42334 | Special case of hashnzfz 42333: the count of multiples in nβ€, n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β (β€β₯β2)) & β’ (π β πΎ β β) β β’ (π β (β―β(( β₯ β {π}) β© (2...πΎ))) = (ββ(πΎ / π))) | ||
Theorem | hashnzfzclim 42335* | As the upper bound πΎ of the constraint interval (π½...πΎ) in hashnzfz 42333 increases, the resulting count of multiples tends to (πΎ / π) βthat is, there are approximately (πΎ / π) multiples of π in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β β) & β’ (π β π½ β β€) β β’ (π β (π β (β€β₯β(π½ β 1)) β¦ ((β―β(( β₯ β {π}) β© (π½...π))) / π)) β (1 / π)) | ||
Theorem | caofcan 42336* | Transfer a cancellation law like mulcan 11726 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ:π΄βΆπ) & β’ (π β π»:π΄βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯π π¦) = (π₯π π§) β π¦ = π§)) β β’ (π β ((πΉ βf π πΊ) = (πΉ βf π π») β πΊ = π»)) | ||
Theorem | ofsubid 42337 | Function analogue of subid 11354. (Contributed by Steve Rodriguez, 5-Nov-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ) β (πΉ βf β πΉ) = (π΄ Γ {0})) | ||
Theorem | ofmul12 42338 | Function analogue of mul12 11254. (Contributed by Steve Rodriguez, 13-Nov-2015.) |
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆβ β§ π»:π΄βΆβ)) β (πΉ βf Β· (πΊ βf Β· π»)) = (πΊ βf Β· (πΉ βf Β· π»))) | ||
Theorem | ofdivrec 42339 | Function analogue of divrec 11763, a division analogue of ofnegsub 12085. (Contributed by Steve Rodriguez, 3-Nov-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β (πΉ βf Β· ((π΄ Γ {1}) βf / πΊ)) = (πΉ βf / πΊ)) | ||
Theorem | ofdivcan4 42340 | Function analogue of divcan4 11774. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β ((πΉ βf Β· πΊ) βf / πΊ) = πΉ) | ||
Theorem | ofdivdiv2 42341 | Function analogue of divdiv2 11801. (Contributed by Steve Rodriguez, 23-Nov-2015.) |
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β (πΉ βf / (πΊ βf / π»)) = ((πΉ βf Β· π») βf / πΊ)) | ||
Theorem | lhe4.4ex1a 42342 | Example of the Fundamental Theorem of Calculus, part two (ftc2 25330): β«(1(,)2)((π₯β2) β 3) dπ₯ = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 25330 as simply the "Fundamental Theorem of Calculus", then ftc1 25328 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.) |
β’ β«(1(,)2)((π₯β2) β 3) dπ₯ = -(2 / 3) | ||
Theorem | dvsconst 42343 | Derivative of a constant function on the real or complex numbers. The function may return a complex π΄ even if π is β. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
β’ ((π β {β, β} β§ π΄ β β) β (π D (π Γ {π΄})) = (π Γ {0})) | ||
Theorem | dvsid 42344 | Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
β’ (π β {β, β} β (π D ( I βΎ π)) = (π Γ {1})) | ||
Theorem | dvsef 42345 | Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.) |
β’ (π β {β, β} β (π D (exp βΎ π)) = (exp βΎ π)) | ||
Theorem | expgrowthi 42346* | Exponential growth and decay model. See expgrowth 42348 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
β’ (π β π β {β, β}) & β’ (π β πΎ β β) & β’ (π β πΆ β β) & β’ π = (π‘ β π β¦ (πΆ Β· (expβ(πΎ Β· π‘)))) β β’ (π β (π D π) = ((π Γ {πΎ}) βf Β· π)) | ||
Theorem | dvconstbi 42347* | The derivative of a function on π is zero iff it is a constant function. Roughly a biconditional π analogue of dvconst 25203 and dveq0 25286. Corresponds to integration formula "β«0 dπ₯ = πΆ " in section 4.1 of [LarsonHostetlerEdwards] p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
β’ (π β π β {β, β}) & β’ (π β π:πβΆβ) & β’ (π β dom (π D π) = π) β β’ (π β ((π D π) = (π Γ {0}) β βπ β β π = (π Γ {π}))) | ||
Theorem | expgrowth 42348* |
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 42346 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 42346); 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 (π D π), C as π, and ky as ((π Γ {πΎ}) βf Β· π). (π Γ {πΎ}) is the constant function that maps any real or complex input to k and βf Β· 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 42346 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 42346. Statements for this and expgrowthi 42346 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.) |
β’ (π β π β {β, β}) & β’ (π β πΎ β β) & β’ (π β π:πβΆβ) & β’ (π β dom (π D π) = π) β β’ (π β ((π D π) = ((π Γ {πΎ}) βf Β· π) β βπ β β π = (π‘ β π β¦ (π Β· (expβ(πΎ Β· π‘)))))) | ||
Syntax | cbcc 42349 | Extend class notation to include the generalized binomial coefficient operation. |
class Cπ | ||
Definition | df-bcc 42350* | Define a generalized binomial coefficient operation, which unlike df-bc 14131 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ Cπ = (π β β, π β β0 β¦ ((π FallFac π) / (!βπ))) | ||
Theorem | bccval 42351 | Value of the generalized binomial coefficient, πΆ choose πΎ. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β (πΆCππΎ) = ((πΆ FallFac πΎ) / (!βπΎ))) | ||
Theorem | bcccl 42352 | Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β (πΆCππΎ) β β) | ||
Theorem | bcc0 42353 | The generalized binomial coefficient πΆ choose πΎ is zero iff πΆ is an integer between zero and (πΎ β 1) inclusive. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β ((πΆCππΎ) = 0 β πΆ β (0...(πΎ β 1)))) | ||
Theorem | bccp1k 42354 | Generalized binomial coefficient: πΆ choose (πΎ + 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β (πΆCπ(πΎ + 1)) = ((πΆCππΎ) Β· ((πΆ β πΎ) / (πΎ + 1)))) | ||
Theorem | bccm1k 42355 | Generalized binomial coefficient: πΆ choose (πΎ β 1), when πΆ is not (πΎ β 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β (β β {(πΎ β 1)})) & β’ (π β πΎ β β) β β’ (π β (πΆCπ(πΎ β 1)) = ((πΆCππΎ) / ((πΆ β (πΎ β 1)) / πΎ))) | ||
Theorem | bccn0 42356 | Generalized binomial coefficient: πΆ choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) β β’ (π β (πΆCπ0) = 1) | ||
Theorem | bccn1 42357 | Generalized binomial coefficient: πΆ choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) β β’ (π β (πΆCπ1) = πΆ) | ||
Theorem | bccbc 42358 | The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π β β0) & β’ (π β πΎ β β0) β β’ (π β (πCππΎ) = (πCπΎ)) | ||
Theorem | uzmptshftfval 42359* | When πΉ is a maps-to function on some set of upper integers π that returns a set π΅, (πΉ shift π) is another maps-to function on the shifted set of upper integers π. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ πΉ = (π₯ β π β¦ π΅) & β’ π΅ β V & β’ (π₯ = (π¦ β π) β π΅ = πΆ) & β’ π = (β€β₯βπ) & β’ π = (β€β₯β(π + π)) & β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (πΉ shift π) = (π¦ β π β¦ πΆ)) | ||
Theorem | dvradcnv2 42360* | The radius of convergence of the (formal) derivative π» of the power series πΊ is (at least) as large as the radius of convergence of πΊ. This version of dvradcnv 25702 uses a shifted version of π» to match the sum form of (β D πΉ) in pserdv2 25711 (and shows how to use uzmptshftfval 42359 to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β β¦ ((π Β· (π΄βπ)) Β· (πβ(π β 1)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β (absβπ) < π ) β β’ (π β seq1( + , π») β dom β ) | ||
Theorem | binomcxplemwb 42361 | Lemma for binomcxp 42370. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β) β β’ (π β (((πΆ β πΎ) Β· (πΆCππΎ)) + ((πΆ β (πΎ β 1)) Β· (πΆCπ(πΎ β 1)))) = (πΆ Β· (πΆCππΎ))) | ||
Theorem | binomcxplemnn0 42362* | Lemma for binomcxp 42370. When πΆ is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 15650 equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set (0...πΆ), and when the index set is widened beyond πΆ the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) β β’ ((π β§ πΆ β β0) β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) | ||
Theorem | binomcxplemrat 42363* | Lemma for binomcxp 42370. As π 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.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) β β’ (π β (π β β0 β¦ (absβ((πΆ β π) / (π + 1)))) β 1) | ||
Theorem | binomcxplemfrat 42364* | Lemma for binomcxp 42370. binomcxplemrat 42363 implies that when πΆ is not a nonnegative integer, the absolute value of the ratio ((πΉβ(π + 1)) / (πΉβπ)) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) β β’ ((π β§ Β¬ πΆ β β0) β (π β β0 β¦ (absβ((πΉβ(π + 1)) / (πΉβπ)))) β 1) | ||
Theorem | binomcxplemradcnv 42365* | Lemma for binomcxp 42370. By binomcxplemfrat 42364 and radcnvrat 42327 the radius of convergence of power series Ξ£π β β0((πΉβπ) Β· (πβπ)) is one. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) & β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) & β’ π = sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*, < ) β β’ ((π β§ Β¬ πΆ β β0) β π = 1) | ||
Theorem | binomcxplemdvbinom 42366* | Lemma for binomcxp 42370. By the power and chain rules, calculate the derivative of ((1 + π)βπ-πΆ), with respect to π in the disk of convergence π·. We later multiply the derivative in the later binomcxplemdvsum 42368 by this derivative to show that ((1 + π)βππΆ) (with a nonnegated πΆ) and the later sum, since both at π = 0 equal one, are the same. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) & β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) & β’ π = sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*, < ) & β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) & β’ π· = (β‘abs β (0[,)π )) β β’ ((π β§ Β¬ πΆ β β0) β (β D (π β π· β¦ ((1 + π)βπ-πΆ))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))) | ||
Theorem | binomcxplemcvg 42367* | Lemma for binomcxp 42370. The sum in binomcxplemnn0 42362 and its derivative (see the next theorem, binomcxplemdvsum 42368) converge, as long as their base π½ 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.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) & β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) & β’ π = sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*, < ) & β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) & β’ π· = (β‘abs β (0[,)π )) β β’ ((π β§ π½ β π·) β (seq0( + , (πβπ½)) β dom β β§ seq1( + , (πΈβπ½)) β dom β )) | ||
Theorem | binomcxplemdvsum 42368* | Lemma for binomcxp 42370. The derivative of the generalized sum in binomcxplemnn0 42362. Part of remark "This convergence allows to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) & β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) & β’ π = sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*, < ) & β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) & β’ π· = (β‘abs β (0[,)π )) & β’ π = (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) β β’ (π β (β D π) = (π β π· β¦ Ξ£π β β ((πΈβπ)βπ))) | ||
Theorem | binomcxplemnotnn0 42369* |
Lemma for binomcxp 42370. When πΆ is not a nonnegative integer, the
generalized sum in binomcxplemnn0 42362 βwhich we will call π
βis a convergent power series: its base π is always of
smaller absolute value than the radius of convergence.
pserdv2 25711 gives the derivative of π, which by dvradcnv 25702 also converges in that radius. When π΄ is fixed at one, (π΄ + π) times that derivative equals (πΆ Β· π) and fraction (π / ((π΄ + π)βππΆ)) is always defined with derivative zero, so the fraction is a constantβspecifically one, because ((1 + 0)βππΆ) = 1. Thus ((1 + π)βππΆ) = (πβπ). Finally, let π be (π΅ / π΄), and multiply both the binomial ((1 + (π΅ / π΄))βππΆ) and the sum (πβ(π΅ / π΄)) by (π΄βππΆ) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) & β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) & β’ π = sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*, < ) & β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) & β’ π· = (β‘abs β (0[,)π )) & β’ π = (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) β β’ ((π β§ Β¬ πΆ β β0) β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) | ||
Theorem | binomcxp 42370* | Generalize the binomial theorem binom 15650 to positive real summand π΄, real summand π΅, and complex exponent πΆ. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus 15650; see also https://en.wikipedia.org/wiki/Binomial_series 15650, https://en.wikipedia.org/wiki/Binomial_theorem 15650 (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem 15650. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) | ||
Theorem | pm10.12 42371* | 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.) |
β’ (βπ₯(π β¨ π) β (π β¨ βπ₯π)) | ||
Theorem | pm10.14 42372 | Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ ((βπ₯π β§ βπ₯π) β ([π¦ / π₯]π β§ [π¦ / π₯]π)) | ||
Theorem | pm10.251 42373 | Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (βπ₯ Β¬ π β Β¬ βπ₯π) | ||
Theorem | pm10.252 42374 | Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.) |
β’ (Β¬ βπ₯π β βπ₯ Β¬ π) | ||
Theorem | pm10.253 42375 | Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (Β¬ βπ₯π β βπ₯ Β¬ π) | ||
Theorem | albitr 42376 | Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯(π β π) β§ βπ₯(π β π)) β βπ₯(π β π)) | ||
Theorem | pm10.42 42377 | Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ ((βπ₯π β¨ βπ₯π) β βπ₯(π β¨ π)) | ||
Theorem | pm10.52 42378* | Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯π β (βπ₯(π β π) β π)) | ||
Theorem | pm10.53 42379 | Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (Β¬ βπ₯π β βπ₯(π β π)) | ||
Theorem | pm10.541 42380* | Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯(π β (π β¨ π)) β (π β¨ βπ₯(π β π))) | ||
Theorem | pm10.542 42381* | Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯(π β (π β π)) β (π β βπ₯(π β π))) | ||
Theorem | pm10.55 42382 | Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯(π β§ π) β§ βπ₯(π β π)) β (βπ₯π β§ βπ₯(π β π))) | ||
Theorem | pm10.56 42383 | Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯(π β π) β§ βπ₯(π β§ π)) β βπ₯(π β§ π)) | ||
Theorem | pm10.57 42384 | Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯(π β (π β¨ π)) β (βπ₯(π β π) β¨ βπ₯(π β§ π))) | ||
Theorem | 2alanimi 42385 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((π β§ π) β π) β β’ ((βπ₯βπ¦π β§ βπ₯βπ¦π) β βπ₯βπ¦π) | ||
Theorem | 2al2imi 42386 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (π β (π β π)) β β’ (βπ₯βπ¦π β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | pm11.11 42387 | Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ π β β’ βπ§βπ€[π§ / π₯][π€ / π¦]π | ||
Theorem | pm11.12 42388* | Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (βπ₯βπ¦(π β¨ π) β (π β¨ βπ₯βπ¦π)) | ||
Theorem | 19.21vv 42389* | Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1943. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (π β βπ₯βπ¦π)) | ||
Theorem | 2alim 42390 | Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | 2albi 42391 | Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | 2exim 42392 | Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | 2exbi 42393 | Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | spsbce-2 42394 | Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ([π§ / π₯][π€ / π¦]π β βπ₯βπ¦π) | ||
Theorem | 19.33-2 42395 | Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯βπ¦π β¨ βπ₯βπ¦π) β βπ₯βπ¦(π β¨ π)) | ||
Theorem | 19.36vv 42396* | Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β π)) | ||
Theorem | 19.31vv 42397* | Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β¨ π) β (βπ₯βπ¦π β¨ π)) | ||
Theorem | 19.37vv 42398* | Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (π β βπ₯βπ¦π)) | ||
Theorem | 19.28vv 42399* | Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β§ π) β (π β§ βπ₯βπ¦π)) | ||
Theorem | pm11.52 42400 | Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β§ π) β Β¬ βπ₯βπ¦(π β Β¬ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |