Home | Metamath
Proof Explorer Theorem List (p. 254 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 | lhop2 25301* | L'HΓ΄pital's Rule for limits from the left. If πΉ and πΊ are differentiable real functions on (π΄, π΅), and πΉ and πΊ both approach 0 at π΅, and πΊ(π₯) and πΊ' (π₯) are not zero on (π΄, π΅), and the limit of πΉ' (π₯) / πΊ' (π₯) at π΅ is πΆ, then the limit πΉ(π₯) / πΊ(π₯) at π΅ also exists and equals πΆ. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β πΊ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β dom (β D πΊ) = (π΄(,)π΅)) & β’ (π β 0 β (πΉ limβ π΅)) & β’ (π β 0 β (πΊ limβ π΅)) & β’ (π β Β¬ 0 β ran πΊ) & β’ (π β Β¬ 0 β ran (β D πΊ)) & β’ (π β πΆ β ((π§ β (π΄(,)π΅) β¦ (((β D πΉ)βπ§) / ((β D πΊ)βπ§))) limβ π΅)) β β’ (π β πΆ β ((π§ β (π΄(,)π΅) β¦ ((πΉβπ§) / (πΊβπ§))) limβ π΅)) | ||
Theorem | lhop 25302* | L'HΓ΄pital's Rule. If πΌ is an open set of the reals, πΉ and πΊ are real functions on π΄ containing all of πΌ except possibly π΅, which are differentiable everywhere on πΌ β {π΅}, πΉ and πΊ both approach 0, and the limit of πΉ' (π₯) / πΊ' (π₯) at π΅ is πΆ, then the limit πΉ(π₯) / πΊ(π₯) at π΅ also exists and equals πΆ. This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) & β’ (π β πΌ β (topGenβran (,))) & β’ (π β π΅ β πΌ) & β’ π· = (πΌ β {π΅}) & β’ (π β π· β dom (β D πΉ)) & β’ (π β π· β dom (β D πΊ)) & β’ (π β 0 β (πΉ limβ π΅)) & β’ (π β 0 β (πΊ limβ π΅)) & β’ (π β Β¬ 0 β (πΊ β π·)) & β’ (π β Β¬ 0 β ((β D πΊ) β π·)) & β’ (π β πΆ β ((π§ β π· β¦ (((β D πΉ)βπ§) / ((β D πΊ)βπ§))) limβ π΅)) β β’ (π β πΆ β ((π§ β π· β¦ ((πΉβπ§) / (πΊβπ§))) limβ π΅)) | ||
Theorem | dvcnvrelem1 25303 | Lemma for dvcnvre 25305. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β dom (β D πΉ) = π) & β’ (π β Β¬ 0 β ran (β D πΉ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β πΆ β π) & β’ (π β π β β+) & β’ (π β ((πΆ β π )[,](πΆ + π )) β π) β β’ (π β (πΉβπΆ) β ((intβ(topGenβran (,)))β(πΉ β ((πΆ β π )[,](πΆ + π ))))) | ||
Theorem | dvcnvrelem2 25304 | Lemma for dvcnvre 25305. (Contributed by Mario Carneiro, 19-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β dom (β D πΉ) = π) & β’ (π β Β¬ 0 β ran (β D πΉ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β πΆ β π) & β’ (π β π β β+) & β’ (π β ((πΆ β π )[,](πΆ + π )) β π) & β’ π = (topGenβran (,)) & β’ π½ = (TopOpenββfld) & β’ π = (π½ βΎt π) & β’ π = (π½ βΎt π) β β’ (π β ((πΉβπΆ) β ((intβπ)βπ) β§ β‘πΉ β ((π CnP π)β(πΉβπΆ)))) | ||
Theorem | dvcnvre 25305* | The derivative rule for inverse functions. If πΉ is a continuous and differentiable bijective function from π to π which never has derivative 0, then β‘πΉ is also differentiable, and its derivative is the reciprocal of the derivative of πΉ. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β dom (β D πΉ) = π) & β’ (π β Β¬ 0 β ran (β D πΉ)) & β’ (π β πΉ:πβ1-1-ontoβπ) β β’ (π β (β D β‘πΉ) = (π₯ β π β¦ (1 / ((β D πΉ)β(β‘πΉβπ₯))))) | ||
Theorem | dvcvx 25306 | A real function with strictly increasing derivative is strictly convex. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ) Isom < , < ((π΄(,)π΅), π)) & β’ (π β π β (0(,)1)) & β’ πΆ = ((π Β· π΄) + ((1 β π) Β· π΅)) β β’ (π β (πΉβπΆ) < ((π Β· (πΉβπ΄)) + ((1 β π) Β· (πΉβπ΅)))) | ||
Theorem | dvfsumle 25307* | Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β€ π΅) β β’ (π β Ξ£π β (π..^π)π β€ (π· β πΆ)) | ||
Theorem | dvfsumge 25308* | Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π΅ β€ π) β β’ (π β (π· β πΆ) β€ Ξ£π β (π..^π)π) | ||
Theorem | dvfsumabs 25309* | Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β (absβ(π β π΅)) β€ π) β β’ (π β (absβ(Ξ£π β (π..^π)π β (π· β πΆ))) β€ Ξ£π β (π..^π)π) | ||
Theorem | dvmptrecl 25310* | Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ ((π β§ π₯ β π) β π΅ β β) | ||
Theorem | dvfsumrlimf 25311* | Lemma for dvfsumrlim 25317. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) β β’ (π β πΊ:πβΆβ) | ||
Theorem | dvfsumlem1 25312* | Lemma for dvfsumrlim 25317. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β (π»βπ) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ)) | ||
Theorem | dvfsumlem2 25313* | Lemma for dvfsumrlim 25317. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | dvfsumlem3 25314* | Lemma for dvfsumrlim 25317. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | dvfsumlem4 25315* | Lemma for dvfsumrlim 25317. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ ((π β§ (π₯ β π β§ π· β€ π₯ β§ π₯ β€ π)) β 0 β€ π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) β β’ (π β (absβ((πΊβπ) β (πΊβπ))) β€ β¦π / π₯β¦π΅) | ||
Theorem | dvfsumrlimge0 25316* | Lemma for dvfsumrlim 25317. Satisfy the assumption of dvfsumlem4 25315. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ (π β (π₯ β π β¦ π΅) βπ 0) β β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β 0 β€ π΅) | ||
Theorem | dvfsumrlim 25317* | Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if π₯ β π β¦ π΅ is a decreasing function with antiderivative π΄ converging to zero, then the difference between Ξ£π β (π...(ββπ₯))π΅(π) and π΄(π₯) = β«π’ β (π[,]π₯)π΅(π’) dπ’ converges to a constant limit value, with the remainder term bounded by π΅(π₯). (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ (π β (π₯ β π β¦ π΅) βπ 0) β β’ (π β πΊ β dom βπ ) | ||
Theorem | dvfsumrlim2 25318* | Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if π₯ β π β¦ π΅ is a decreasing function with antiderivative π΄ converging to zero, then the difference between Ξ£π β (π...(ββπ₯))π΅(π) and β«π’ β (π[,]π₯)π΅(π’) dπ’ = π΄(π₯) converges to a constant limit value, with the remainder term bounded by π΅(π₯). (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ (π β (π₯ β π β¦ π΅) βπ 0) & β’ (π β π β π) & β’ (π β π· β€ π) β β’ ((π β§ πΊ βπ πΏ) β (absβ((πΊβπ) β πΏ)) β€ β¦π / π₯β¦π΅) | ||
Theorem | dvfsumrlim3 25319* | Conjoin the statements of dvfsumrlim 25317 and dvfsumrlim2 25318. (This is useful as a target for lemmas, because the hypotheses to this theorem are complex, and we don't want to repeat ourselves.) (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ (π β (π₯ β π β¦ π΅) βπ 0) & β’ (π₯ = π β π΅ = πΈ) β β’ (π β (πΊ:πβΆβ β§ πΊ β dom βπ β§ ((πΊ βπ πΏ β§ π β π β§ π· β€ π) β (absβ((πΊβπ) β πΏ)) β€ πΈ))) | ||
Theorem | dvfsum2 25320* | The reverse of dvfsumrlim 25317, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β β*) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β π΅ β€ πΆ) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β 0 β€ π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π₯ = π β π΅ = πΈ) β β’ (π β (absβ((πΊβπ) β (πΊβπ))) β€ πΈ) | ||
Theorem | ftc1lem1 25321* | Lemma for ftc1a 25323 and ftc1 25328. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π β (π΄[,]π΅)) β β’ ((π β§ π β€ π) β ((πΊβπ) β (πΊβπ)) = β«(π(,)π)(πΉβπ‘) dπ‘) | ||
Theorem | ftc1lem2 25322* | Lemma for ftc1 25328. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ (π β πΊ:(π΄[,]π΅)βΆβ) | ||
Theorem | ftc1a 25323* | The Fundamental Theorem of Calculus, part one. The function πΊ formed by varying the right endpoint of an integral of πΉ is continuous if πΉ is integrable. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | ftc1lem3 25324* | Lemma for ftc1 25328. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) β β’ (π β πΉ:π·βΆβ) | ||
Theorem | ftc1lem4 25325* | Lemma for ftc1 25328. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) & β’ π» = (π§ β ((π΄[,]π΅) β {πΆ}) β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) & β’ (π β πΈ β β+) & β’ (π β π β β+) & β’ ((π β§ π¦ β π·) β ((absβ(π¦ β πΆ)) < π β (absβ((πΉβπ¦) β (πΉβπΆ))) < πΈ)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β πΆ)) < π ) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β πΆ)) < π ) β β’ ((π β§ π < π) β (absβ((((πΊβπ) β (πΊβπ)) / (π β π)) β (πΉβπΆ))) < πΈ) | ||
Theorem | ftc1lem5 25326* | Lemma for ftc1 25328. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) & β’ π» = (π§ β ((π΄[,]π΅) β {πΆ}) β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) & β’ (π β πΈ β β+) & β’ (π β π β β+) & β’ ((π β§ π¦ β π·) β ((absβ(π¦ β πΆ)) < π β (absβ((πΉβπ¦) β (πΉβπΆ))) < πΈ)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β πΆ)) < π ) β β’ ((π β§ π β πΆ) β (absβ((π»βπ) β (πΉβπΆ))) < πΈ) | ||
Theorem | ftc1lem6 25327* | Lemma for ftc1 25328. (Contributed by Mario Carneiro, 14-Aug-2014.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) & β’ π» = (π§ β ((π΄[,]π΅) β {πΆ}) β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) β β’ (π β (πΉβπΆ) β (π» limβ πΆ)) | ||
Theorem | ftc1 25328* | The Fundamental Theorem of Calculus, part one. The function formed by varying the right endpoint of an integral is differentiable at πΆ with derivative πΉ(πΆ) if the original function is continuous at πΆ. This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) β β’ (π β πΆ(β D πΊ)(πΉβπΆ)) | ||
Theorem | ftc1cn 25329* | Strengthen the assumptions of ftc1 25328 to when the function πΉ is continuous on the entire interval (π΄, π΅); in this case we can calculate D πΊ exactly. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΉ β πΏ1) β β’ (π β (β D πΊ) = πΉ) | ||
Theorem | ftc2 25330* | The Fundamental Theorem of Calculus, part two. If πΉ is a function continuous on [π΄, π΅] and continuously differentiable on (π΄, π΅), then the integral of the derivative of πΉ is equal to πΉ(π΅) β πΉ(π΄). This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (β D πΉ) β ((π΄(,)π΅)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | ftc2ditglem 25331* | Lemma for ftc2ditg 25332. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β (π[,]π)) & β’ (π β π΅ β (π[,]π)) & β’ (π β (β D πΉ) β ((π(,)π)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π[,]π)βcnββ)) β β’ ((π β§ π΄ β€ π΅) β β¨[π΄ β π΅]((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | ftc2ditg 25332* | Directed integral analogue of ftc2 25330. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β (π[,]π)) & β’ (π β π΅ β (π[,]π)) & β’ (π β (β D πΉ) β ((π(,)π)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π[,]π)βcnββ)) β β’ (π β β¨[π΄ β π΅]((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | itgparts 25333* | Integration by parts. If π΅(π₯) is the derivative of π΄(π₯) and π·(π₯) is the derivative of πΆ(π₯), and πΈ = (π΄ Β· π΅)(π) and πΉ = (π΄ Β· π΅)(π), then under suitable integrability and differentiability assumptions, the integral of π΄ Β· π· from π to π is equal to πΉ β πΈ minus the integral of π΅ Β· πΆ. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ (π β (π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ π·) β ((π(,)π)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ (π΄ Β· π·)) β πΏ1) & β’ (π β (π₯ β (π(,)π) β¦ (π΅ Β· πΆ)) β πΏ1) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π β (β D (π₯ β (π[,]π) β¦ πΆ)) = (π₯ β (π(,)π) β¦ π·)) & β’ ((π β§ π₯ = π) β (π΄ Β· πΆ) = πΈ) & β’ ((π β§ π₯ = π) β (π΄ Β· πΆ) = πΉ) β β’ (π β β«(π(,)π)(π΄ Β· π·) dπ₯ = ((πΉ β πΈ) β β«(π(,)π)(π΅ Β· πΆ) dπ₯)) | ||
Theorem | itgsubstlem 25334* | Lemma for itgsubst 25335. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) & β’ (π β π β (π(,)π)) & β’ (π β π β (π(,)π)) & β’ ((π β§ π₯ β (π[,]π)) β π΄ β (π(,)π)) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubst 25335* | Integration by π’-substitution. If π΄(π₯) is a continuous, differentiable function from [π, π] to (π, π), whose derivative is continuous and integrable, and πΆ(π’) is a continuous function on (π, π), then the integral of πΆ(π’) from πΎ = π΄(π) to πΏ = π΄(π) is equal to the integral of πΆ(π΄(π₯)) D π΄(π₯) from π to π. In this part of the proof we discharge the assumptions in itgsubstlem 25334, which use the fact that (π, π) is open to shrink the interval a little to (π, π) where π < π < π < π- this is possible because π΄(π₯) is a continuous function on a closed interval, so its range is in fact a closed interval, and we have some wiggle room on the edges. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgpowd 25336* | The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β0) β β’ (π β β«(π΄[,]π΅)(π₯βπ) dπ₯ = (((π΅β(π + 1)) β (π΄β(π + 1))) / (π + 1))) | ||
Syntax | cmdg 25337 | Multivariate polynomial degree. |
class mDeg | ||
Syntax | cdg1 25338 | Univariate polynomial degree. |
class deg1 | ||
Definition | df-mdeg 25339* | Define the degree of a polynomial. Note (SO): as an experiment I am using a definition which makes the degree of the zero polynomial -β, contrary to the convention used in df-dgr 25474. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ mDeg = (π β V, π β V β¦ (π β (Baseβ(π mPoly π)) β¦ sup(ran (β β (π supp (0gβπ)) β¦ (βfld Ξ£g β)), β*, < ))) | ||
Definition | df-deg1 25340 | Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ deg1 = (π β V β¦ (1o mDeg π)) | ||
Theorem | reldmmdeg 25341 | Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ Rel dom mDeg | ||
Theorem | tdeglem1 25342* | Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ π»:π΄βΆβ0 | ||
Theorem | tdeglem1OLD 25343* | Obsolete version of tdeglem1 25342 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ (πΌ β π β π»:π΄βΆβ0) | ||
Theorem | tdeglem3 25344* | Additivity of the total degree helper function. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((π β π΄ β§ π β π΄) β (π»β(π βf + π)) = ((π»βπ) + (π»βπ))) | ||
Theorem | tdeglem3OLD 25345* | Obsolete version of tdeglem3 25344 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((πΌ β π β§ π β π΄ β§ π β π΄) β (π»β(π βf + π)) = ((π»βπ) + (π»βπ))) | ||
Theorem | tdeglem4 25346* | There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ (π β π΄ β ((π»βπ) = 0 β π = (πΌ Γ {0}))) | ||
Theorem | tdeglem4OLD 25347* | Obsolete version of tdeglem4 25346 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 29-Mar-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((πΌ β π β§ π β π΄) β ((π»βπ) = 0 β π = (πΌ Γ {0}))) | ||
Theorem | tdeglem2 25348 | Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ (β β (β0 βm 1o) β¦ (βββ )) = (β β (β0 βm 1o) β¦ (βfld Ξ£g β)) | ||
Theorem | mdegfval 25349* | Value of the multivariate degree function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ π· = (π β π΅ β¦ sup((π» β (π supp 0 )), β*, < )) | ||
Theorem | mdegval 25350* | Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ (πΉ β π΅ β (π·βπΉ) = sup((π» β (πΉ supp 0 )), β*, < )) | ||
Theorem | mdegleb 25351* | Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((πΉ β π΅ β§ πΊ β β*) β ((π·βπΉ) β€ πΊ β βπ₯ β π΄ (πΊ < (π»βπ₯) β (πΉβπ₯) = 0 ))) | ||
Theorem | mdeglt 25352* | If there is an upper limit on the degree of a polynomial that is lower than the degree of some exponent bag, then that exponent bag is unrepresented in the polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) & β’ (π β πΉ β π΅) & β’ (π β π β π΄) & β’ (π β (π·βπΉ) < (π»βπ)) β β’ (π β (πΉβπ) = 0 ) | ||
Theorem | mdegldg 25353* | A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) & β’ π = (0gβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β π) β βπ₯ β π΄ ((πΉβπ₯) β 0 β§ (π»βπ₯) = (π·βπΉ))) | ||
Theorem | mdegxrcl 25354 | Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β β*) | ||
Theorem | mdegxrf 25355 | Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ π·:π΅βΆβ* | ||
Theorem | mdegcl 25356 | Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β (β0 βͺ {-β})) | ||
Theorem | mdeg0 25357 | Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ 0 = (0gβπ) β β’ ((πΌ β π β§ π β Ring) β (π·β 0 ) = -β) | ||
Theorem | mdegnn0cl 25358 | Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π·βπΉ) β β0) | ||
Theorem | degltlem1 25359 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ ((π β (β0 βͺ {-β}) β§ π β β€) β (π < π β π β€ (π β 1))) | ||
Theorem | degltp1le 25360 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ ((π β (β0 βͺ {-β}) β§ π β β€) β (π < (π + 1) β π β€ π)) | ||
Theorem | mdegaddle 25361 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) | ||
Theorem | mdegvscale 25362 | The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π·βπΊ)) | ||
Theorem | mdegvsca 25363 | The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΈ = (RLRegβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΈ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) = (π·βπΊ)) | ||
Theorem | mdegle0 25364 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β πΉ β π΅) β β’ (π β ((π·βπΉ) β€ 0 β πΉ = (π΄β(πΉβ(πΌ Γ {0}))))) | ||
Theorem | mdegmullem 25365* | Lemma for mdegmulle2 25366. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β πΎ β β0) & β’ (π β (π·βπΉ) β€ π½) & β’ (π β (π·βπΊ) β€ πΎ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (π β π΄ β¦ (βfld Ξ£g π)) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) | ||
Theorem | mdegmulle2 25366 | The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β πΎ β β0) & β’ (π β (π·βπΉ) β€ π½) & β’ (π β (π·βπΊ) β€ πΎ) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) | ||
Theorem | deg1fval 25367 | Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ π· = ( deg1 βπ ) β β’ π· = (1o mDeg π ) | ||
Theorem | deg1xrf 25368 | Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ π·:π΅βΆβ* | ||
Theorem | deg1xrcl 25369 | Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β β*) | ||
Theorem | deg1cl 25370 | Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β (β0 βͺ {-β})) | ||
Theorem | mdegpropd 25371* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β (πΌ mDeg π ) = (πΌ mDeg π)) | ||
Theorem | deg1fvi 25372 | Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ ( deg1 βπ ) = ( deg1 β( I βπ )) | ||
Theorem | deg1propd 25373* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β ( deg1 βπ ) = ( deg1 βπ)) | ||
Theorem | deg1z 25374 | Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) β β’ (π β Ring β (π·β 0 ) = -β) | ||
Theorem | deg1nn0cl 25375 | Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π·βπΉ) β β0) | ||
Theorem | deg1n0ima 25376 | Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β (π· β (π΅ β { 0 })) β β0) | ||
Theorem | deg1nn0clb 25377 | A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅) β (πΉ β 0 β (π·βπΉ) β β0)) | ||
Theorem | deg1lt0 25378 | A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅) β ((π·βπΉ) < 0 β πΉ = 0 )) | ||
Theorem | deg1ldg 25379 | A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π΄β(π·βπΉ)) β π) | ||
Theorem | deg1ldgn 25380 | An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ π΄ = (coe1βπΉ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β π β β0) & β’ (π β (π΄βπ) = π) β β’ (π β (π·βπΉ) β π) | ||
Theorem | deg1ldgdomn 25381 | A nonzero univariate polynomial over a domain always has a nonzero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ πΈ = (RLRegβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((π β Domn β§ πΉ β π΅ β§ πΉ β 0 ) β (π΄β(π·βπΉ)) β πΈ) | ||
Theorem | deg1leb 25382* | Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((πΉ β π΅ β§ πΊ β β*) β ((π·βπΉ) β€ πΊ β βπ₯ β β0 (πΊ < π₯ β (π΄βπ₯) = 0 ))) | ||
Theorem | deg1val 25383 | Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Jul-2019.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ (πΉ β π΅ β (π·βπΉ) = sup((π΄ supp 0 ), β*, < )) | ||
Theorem | deg1lt 25384 | If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((πΉ β π΅ β§ πΊ β β0 β§ (π·βπΉ) < πΊ) β (π΄βπΊ) = 0 ) | ||
Theorem | deg1ge 25385 | Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((πΉ β π΅ β§ πΊ β β0 β§ (π΄βπΊ) β 0 ) β πΊ β€ (π·βπΉ)) | ||
Theorem | coe1mul3 25386 | The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΌ β β0) & β’ (π β (π·βπΉ) β€ πΌ) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β (π·βπΊ) β€ π½) β β’ (π β ((coe1β(πΉ β πΊ))β(πΌ + π½)) = (((coe1βπΉ)βπΌ) Β· ((coe1βπΊ)βπ½))) | ||
Theorem | coe1mul4 25387 | Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΉ β 0 ) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) β β’ (π β ((coe1β(πΉ β πΊ))β((π·βπΉ) + (π·βπΊ))) = (((coe1βπΉ)β(π·βπΉ)) Β· ((coe1βπΊ)β(π·βπΊ)))) | ||
Theorem | deg1addle 25388 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) | ||
Theorem | deg1addle2 25389 | If both factors have degree bounded by πΏ, then the sum of the polynomials also has degree bounded by πΏ. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΏ β β*) & β’ (π β (π·βπΉ) β€ πΏ) & β’ (π β (π·βπΊ) β€ πΏ) β β’ (π β (π·β(πΉ + πΊ)) β€ πΏ) | ||
Theorem | deg1add 25390 | Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β (π·βπΊ) < (π·βπΉ)) β β’ (π β (π·β(πΉ + πΊ)) = (π·βπΉ)) | ||
Theorem | deg1vscale 25391 | The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π·βπΊ)) | ||
Theorem | deg1vsca 25392 | The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΈ = (RLRegβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΈ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) = (π·βπΊ)) | ||
Theorem | deg1invg 25393 | The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ (π β πΉ β π΅) β β’ (π β (π·β(πβπΉ)) = (π·βπΉ)) | ||
Theorem | deg1suble 25394 | The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ β πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) | ||
Theorem | deg1sub 25395 | Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β (π·βπΊ) < (π·βπΉ)) β β’ (π β (π·β(πΉ β πΊ)) = (π·βπΉ)) | ||
Theorem | deg1mulle2 25396 | Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β πΎ β β0) & β’ (π β (π·βπΉ) β€ π½) & β’ (π β (π·βπΊ) β€ πΎ) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) | ||
Theorem | deg1sublt 25397 | Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ (π β πΏ β β0) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β (π·βπΉ) β€ πΏ) & β’ (π β πΊ β π΅) & β’ (π β (π·βπΊ) β€ πΏ) & β’ π΄ = (coe1βπΉ) & β’ πΆ = (coe1βπΊ) & β’ (π β ((coe1βπΉ)βπΏ) = ((coe1βπΊ)βπΏ)) β β’ (π β (π·β(πΉ β πΊ)) < πΏ) | ||
Theorem | deg1le0 25398 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β π΅) β ((π·βπΉ) β€ 0 β πΉ = (π΄β((coe1βπΉ)β0)))) | ||
Theorem | deg1sclle 25399 | A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β πΎ) β (π·β(π΄βπΉ)) β€ 0) | ||
Theorem | deg1scl 25400 | A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΉ β πΎ β§ πΉ β 0 ) β (π·β(π΄βπΉ)) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |