![]() |
Metamath
Proof Explorer Theorem List (p. 260 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvsin 25901 | Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (β D sin) = cos | ||
Theorem | dvcos 25902 | Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (β D cos) = (π₯ β β β¦ -(sinβπ₯)) | ||
Theorem | dvferm1lem 25903* | Lemma for dvferm 25907. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π΄(,)π΅) β π) & β’ (π β π β dom (β D πΉ)) & β’ (π β βπ¦ β (π(,)π΅)(πΉβπ¦) β€ (πΉβπ)) & β’ (π β 0 < ((β D πΉ)βπ)) & β’ (π β π β β+) & β’ (π β βπ§ β (π β {π})((π§ β π β§ (absβ(π§ β π)) < π) β (absβ((((πΉβπ§) β (πΉβπ)) / (π§ β π)) β ((β D πΉ)βπ))) < ((β D πΉ)βπ))) & β’ π = ((π + if(π΅ β€ (π + π), π΅, (π + π))) / 2) β β’ Β¬ π | ||
Theorem | dvferm1 25904* | One-sided version of dvferm 25907. A point π which is the local maximum of its right neighborhood has derivative at most zero. (Contributed by Mario Carneiro, 24-Feb-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π΄(,)π΅) β π) & β’ (π β π β dom (β D πΉ)) & β’ (π β βπ¦ β (π(,)π΅)(πΉβπ¦) β€ (πΉβπ)) β β’ (π β ((β D πΉ)βπ) β€ 0) | ||
Theorem | dvferm2lem 25905* | Lemma for dvferm 25907. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π΄(,)π΅) β π) & β’ (π β π β dom (β D πΉ)) & β’ (π β βπ¦ β (π΄(,)π)(πΉβπ¦) β€ (πΉβπ)) & β’ (π β ((β D πΉ)βπ) < 0) & β’ (π β π β β+) & β’ (π β βπ§ β (π β {π})((π§ β π β§ (absβ(π§ β π)) < π) β (absβ((((πΉβπ§) β (πΉβπ)) / (π§ β π)) β ((β D πΉ)βπ))) < -((β D πΉ)βπ))) & β’ π = ((if(π΄ β€ (π β π), (π β π), π΄) + π) / 2) β β’ Β¬ π | ||
Theorem | dvferm2 25906* | One-sided version of dvferm 25907. A point π which is the local maximum of its left neighborhood has derivative at least zero. (Contributed by Mario Carneiro, 24-Feb-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π΄(,)π΅) β π) & β’ (π β π β dom (β D πΉ)) & β’ (π β βπ¦ β (π΄(,)π)(πΉβπ¦) β€ (πΉβπ)) β β’ (π β 0 β€ ((β D πΉ)βπ)) | ||
Theorem | dvferm 25907* | Fermat's theorem on stationary points. A point π which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π΄(,)π΅) β π) & β’ (π β π β dom (β D πΉ)) & β’ (π β βπ¦ β (π΄(,)π΅)(πΉβπ¦) β€ (πΉβπ)) β β’ (π β ((β D πΉ)βπ) = 0) | ||
Theorem | rollelem 25908* | Lemma for rolle 25909. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β Β¬ π β {π΄, π΅}) β β’ (π β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) | ||
Theorem | rolle 25909* | Rolle's theorem. If πΉ is a real continuous function on [π΄, π΅] which is differentiable on (π΄, π΅), and πΉ(π΄) = πΉ(π΅), then there is some π₯ β (π΄, π΅) such that (β D πΉ)βπ₯ = 0. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β (πΉβπ΄) = (πΉβπ΅)) β β’ (π β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) | ||
Theorem | cmvth 25910* | Cauchy's Mean Value Theorem. If πΉ, πΊ are real continuous functions on [π΄, π΅] differentiable on (π΄, π΅), then there is some π₯ β (π΄, π΅) such that πΉ' (π₯) / πΊ' (π₯) = (πΉ(π΄) β πΉ(π΅)) / (πΊ(π΄) β πΊ(π΅)). (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016.) Avoid ax-mulf 11210. (Revised by GG, 16-Mar-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β dom (β D πΊ) = (π΄(,)π΅)) β β’ (π β βπ₯ β (π΄(,)π΅)(((πΉβπ΅) β (πΉβπ΄)) Β· ((β D πΊ)βπ₯)) = (((πΊβπ΅) β (πΊβπ΄)) Β· ((β D πΉ)βπ₯))) | ||
Theorem | cmvthOLD 25911* | Obsolete version of cmvth 25910 as of 16-Apr-2025. (Contributed by Mario Carneiro, 29-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β dom (β D πΊ) = (π΄(,)π΅)) β β’ (π β βπ₯ β (π΄(,)π΅)(((πΉβπ΅) β (πΉβπ΄)) Β· ((β D πΊ)βπ₯)) = (((πΊβπ΅) β (πΊβπ΄)) Β· ((β D πΉ)βπ₯))) | ||
Theorem | mvth 25912* | The Mean Value Theorem. If πΉ is a real continuous function on [π΄, π΅] which is differentiable on (π΄, π΅), then there is some π₯ β (π΄, π΅) such that (β D πΉ)βπ₯ is equal to the average slope over [π΄, π΅]. This is Metamath 100 proof #75. (Contributed by Mario Carneiro, 1-Sep-2014.) (Proof shortened by Mario Carneiro, 29-Dec-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) β β’ (π β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = (((πΉβπ΅) β (πΉβπ΄)) / (π΅ β π΄))) | ||
Theorem | dvlip 25913* | A function with derivative bounded by π is π-Lipschitz continuous. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β π β β) & β’ ((π β§ π₯ β (π΄(,)π΅)) β (absβ((β D πΉ)βπ₯)) β€ π) β β’ ((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) | ||
Theorem | dvlipcn 25914* | A complex function with derivative bounded by π on an open ball is π-Lipschitz continuous. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ (π β π β β) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β π β β*) & β’ π΅ = (π΄(ballβ(abs β β ))π ) & β’ (π β π΅ β dom (β D πΉ)) & β’ (π β π β β) & β’ ((π β§ π₯ β π΅) β (absβ((β D πΉ)βπ₯)) β€ π) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) | ||
Theorem | dvlip2 25915* | Combine the results of dvlip 25913 and dvlipcn 25914 into one. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ (π β π β {β, β}) & β’ π½ = ((abs β β ) βΎ (π Γ π)) & β’ (π β π β π) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β π) & β’ (π β π β β*) & β’ π΅ = (π΄(ballβπ½)π ) & β’ (π β π΅ β dom (π D πΉ)) & β’ (π β π β β) & β’ ((π β§ π₯ β π΅) β (absβ((π D πΉ)βπ₯)) β€ π) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) | ||
Theorem | c1liplem1 25916* | Lemma for c1lip1 25917. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β (β βpm β)) & β’ (π β ((β D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) & β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) & β’ πΎ = sup((abs β ((β D πΉ) β (π΄[,]π΅))), β, < ) β β’ (π β (πΎ β β β§ βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(π₯ < π¦ β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ (πΎ Β· (absβ(π¦ β π₯)))))) | ||
Theorem | c1lip1 25917* | C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β (β βpm β)) & β’ (π β ((β D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) & β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) β β’ (π β βπ β β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(absβ((πΉβπ¦) β (πΉβπ₯))) β€ (π Β· (absβ(π¦ β π₯)))) | ||
Theorem | c1lip2 25918* | C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((πCπββ)β1)) & β’ (π β ran πΉ β β) & β’ (π β (π΄[,]π΅) β dom πΉ) β β’ (π β βπ β β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(absβ((πΉβπ¦) β (πΉβπ₯))) β€ (π Β· (absβ(π¦ β π₯)))) | ||
Theorem | c1lip3 25919* | C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (πΉ βΎ β) β ((πCπββ)β1)) & β’ (π β (πΉ β β) β β) & β’ (π β (π΄[,]π΅) β dom πΉ) β β’ (π β βπ β β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(absβ((πΉβπ¦) β (πΉβπ₯))) β€ (π Β· (absβ(π¦ β π₯)))) | ||
Theorem | dveq0 25920 | If a continuous function has zero derivative at all points on the interior of a closed interval, then it must be a constant function. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by Mario Carneiro, 3-Mar-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ) = ((π΄(,)π΅) Γ {0})) β β’ (π β πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) | ||
Theorem | dv11cn 25921 | Two functions defined on a ball whose derivatives are the same and which are equal at any given point πΆ in the ball must be equal everywhere. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ π = (π΄(ballβ(abs β β ))π ) & β’ (π β π΄ β β) & β’ (π β π β β*) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β dom (β D πΉ) = π) & β’ (π β (β D πΉ) = (β D πΊ)) & β’ (π β πΆ β π) & β’ (π β (πΉβπΆ) = (πΊβπΆ)) β β’ (π β πΉ = πΊ) | ||
Theorem | dvgt0lem1 25922 | Lemma for dvgt0 25924 and dvlt0 25925. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ):(π΄(,)π΅)βΆπ) β β’ (((π β§ (π β (π΄[,]π΅) β§ π β (π΄[,]π΅))) β§ π < π) β (((πΉβπ) β (πΉβπ)) / (π β π)) β π) | ||
Theorem | dvgt0lem2 25923* | Lemma for dvgt0 25924 and dvlt0 25925. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ):(π΄(,)π΅)βΆπ) & β’ π Or β & β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉβπ₯)π(πΉβπ¦)) β β’ (π β πΉ Isom < , π ((π΄[,]π΅), ran πΉ)) | ||
Theorem | dvgt0 25924 | A function on a closed interval with positive derivative is increasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ):(π΄(,)π΅)βΆβ+) β β’ (π β πΉ Isom < , < ((π΄[,]π΅), ran πΉ)) | ||
Theorem | dvlt0 25925 | A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ):(π΄(,)π΅)βΆ(-β(,)0)) β β’ (π β πΉ Isom < , β‘ < ((π΄[,]π΅), ran πΉ)) | ||
Theorem | dvge0 25926 | A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β (β D πΉ):(π΄(,)π΅)βΆ(0[,)+β)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π β€ π) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | dvle 25927* | If π΄(π₯), πΆ(π₯) are differentiable functions and π΄β β€ πΆβ, then for π₯ β€ π¦, π΄(π¦) β π΄(π₯) β€ πΆ(π¦) β πΆ(π₯). (Contributed by Mario Carneiro, 16-May-2016.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π β (π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ)) & β’ (π β (β D (π₯ β (π(,)π) β¦ πΆ)) = (π₯ β (π(,)π) β¦ π·)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β€ π·) & β’ (π β π β (π[,]π)) & β’ (π β π β (π[,]π)) & β’ (π β π β€ π) & β’ (π₯ = π β π΄ = π) & β’ (π₯ = π β πΆ = π) & β’ (π₯ = π β π΄ = π ) & β’ (π₯ = π β πΆ = π) β β’ (π β (π β π) β€ (π β π)) | ||
Theorem | dvivthlem1 25928* | Lemma for dvivth 25930. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π β (π΄(,)π΅)) & β’ (π β π β (π΄(,)π΅)) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β π < π) & β’ (π β πΆ β (((β D πΉ)βπ)[,]((β D πΉ)βπ))) & β’ πΊ = (π¦ β (π΄(,)π΅) β¦ ((πΉβπ¦) β (πΆ Β· π¦))) β β’ (π β βπ₯ β (π[,]π)((β D πΉ)βπ₯) = πΆ) | ||
Theorem | dvivthlem2 25929* | Lemma for dvivth 25930. (Contributed by Mario Carneiro, 20-Feb-2015.) |
β’ (π β π β (π΄(,)π΅)) & β’ (π β π β (π΄(,)π΅)) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β π < π) & β’ (π β πΆ β (((β D πΉ)βπ)[,]((β D πΉ)βπ))) & β’ πΊ = (π¦ β (π΄(,)π΅) β¦ ((πΉβπ¦) β (πΆ Β· π¦))) β β’ (π β πΆ β ran (β D πΉ)) | ||
Theorem | dvivth 25930 | Darboux' theorem, or the intermediate value theorem for derivatives. A differentiable function's derivative satisfies the intermediate value property, even though it may not be continuous (so that ivthicc 25374 does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π β (π΄(,)π΅)) & β’ (π β π β (π΄(,)π΅)) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) β β’ (π β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β ran (β D πΉ)) | ||
Theorem | dvne0 25931 | A function on a closed interval with nonzero derivative is either monotone increasing or monotone decreasing. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β Β¬ 0 β ran (β D πΉ)) β β’ (π β (πΉ Isom < , < ((π΄[,]π΅), ran πΉ) β¨ πΉ Isom < , β‘ < ((π΄[,]π΅), ran πΉ))) | ||
Theorem | dvne0f1 25932 | A function on a closed interval with nonzero derivative is one-to-one. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β Β¬ 0 β ran (β D πΉ)) β β’ (π β πΉ:(π΄[,]π΅)β1-1ββ) | ||
Theorem | lhop1lem 25933* | Lemma for lhop1 25934. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β πΊ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β dom (β D πΊ) = (π΄(,)π΅)) & β’ (π β 0 β (πΉ limβ π΄)) & β’ (π β 0 β (πΊ limβ π΄)) & β’ (π β Β¬ 0 β ran πΊ) & β’ (π β Β¬ 0 β ran (β D πΊ)) & β’ (π β πΆ β ((π§ β (π΄(,)π΅) β¦ (((β D πΉ)βπ§) / ((β D πΊ)βπ§))) limβ π΄)) & β’ (π β πΈ β β+) & β’ (π β π· β β) & β’ (π β π· β€ π΅) & β’ (π β π β (π΄(,)π·)) & β’ (π β βπ‘ β (π΄(,)π·)(absβ((((β D πΉ)βπ‘) / ((β D πΊ)βπ‘)) β πΆ)) < πΈ) & β’ π = (π΄ + (π / 2)) β β’ (π β (absβ(((πΉβπ) / (πΊβπ)) β πΆ)) < (2 Β· πΈ)) | ||
Theorem | lhop1 25934* | L'HΓ΄pital's Rule for limits from the right. 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 | lhop2 25935* | 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 25936* | 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 25937 | Lemma for dvcnvre 25939. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β dom (β D πΉ) = π) & β’ (π β Β¬ 0 β ran (β D πΉ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β πΆ β π) & β’ (π β π β β+) & β’ (π β ((πΆ β π )[,](πΆ + π )) β π) β β’ (π β (πΉβπΆ) β ((intβ(topGenβran (,)))β(πΉ β ((πΆ β π )[,](πΆ + π ))))) | ||
Theorem | dvcnvrelem2 25938 | Lemma for dvcnvre 25939. (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 25939* | 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 25940 | 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 25941* | 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.) Avoid ax-mulf 11210. (Revised by GG, 16-Mar-2025.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β€ π΅) β β’ (π β Ξ£π β (π..^π)π β€ (π· β πΆ)) | ||
Theorem | dvfsumleOLD 25942* | Obsolete version of dvfsumle 25941 as of 17-Apr-2025. (Contributed by Mario Carneiro, 14-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β (β€β₯βπ)) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) & β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π₯ = π β π΄ = πΆ) & β’ (π₯ = π β π΄ = π·) & β’ ((π β§ π β (π..^π)) β π β β) & β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β€ π΅) β β’ (π β Ξ£π β (π..^π)π β€ (π· β πΆ)) | ||
Theorem | dvfsumge 25943* | 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 25944* | 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 25945* | Real closure of a derivative. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ ((π β§ π₯ β π) β π΅ β β) | ||
Theorem | dvfsumrlimf 25946* | Lemma for dvfsumrlim 25953. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) β β’ (π β πΊ:πβΆβ) | ||
Theorem | dvfsumlem1 25947* | Lemma for dvfsumrlim 25953. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β (π»βπ) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ)) | ||
Theorem | dvfsumlem2 25948* | Lemma for dvfsumrlim 25953. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11210. (Revised by GG, 16-Mar-2025.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | dvfsumlem2OLD 25949* | Obsolete version of dvfsumlem2 25948 as of 17-Apr-2025. (Contributed by Mario Carneiro, 17-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β π β€ ((ββπ) + 1)) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | dvfsumlem3 25950* | Lemma for dvfsumrlim 25953. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) β β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) | ||
Theorem | dvfsumlem4 25951* | Lemma for dvfsumrlim 25953. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π β π β β*) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ ((π β§ (π₯ β π β§ π· β€ π₯ β§ π₯ β€ π)) β 0 β€ π΅) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π· β€ π) & β’ (π β π β€ π) & β’ (π β π β€ π) β β’ (π β (absβ((πΊβπ) β (πΊβπ))) β€ β¦π / π₯β¦π΅) | ||
Theorem | dvfsumrlimge0 25952* | Lemma for dvfsumrlim 25953. Satisfy the assumption of dvfsumlem4 25951. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ π = (π(,)+β) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β β) & β’ (π β π β€ (π· + 1)) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π₯ = π β π΅ = πΆ) & β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) & β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) & β’ (π β (π₯ β π β¦ π΅) βπ 0) β β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β 0 β€ π΅) | ||
Theorem | dvfsumrlim 25953* | 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 25954* | 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 25955* | Conjoin the statements of dvfsumrlim 25953 and dvfsumrlim2 25954. (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 25956* | The reverse of dvfsumrlim 25953, 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 25957* | Lemma for ftc1a 25959 and ftc1 25964. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π β (π΄[,]π΅)) β β’ ((π β§ π β€ π) β ((πΊβπ) β (πΊβπ)) = β«(π(,)π)(πΉβπ‘) dπ‘) | ||
Theorem | ftc1lem2 25958* | Lemma for ftc1 25964. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ (π β πΊ:(π΄[,]π΅)βΆβ) | ||
Theorem | ftc1a 25959* | 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 25960* | Lemma for ftc1 25964. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) β β’ (π β πΉ:π·βΆβ) | ||
Theorem | ftc1lem4 25961* | Lemma for ftc1 25964. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) & β’ π½ = (πΏ βΎt β) & β’ πΎ = (πΏ βΎt π·) & β’ πΏ = (TopOpenββfld) & β’ π» = (π§ β ((π΄[,]π΅) β {πΆ}) β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) & β’ (π β πΈ β β+) & β’ (π β π β β+) & β’ ((π β§ π¦ β π·) β ((absβ(π¦ β πΆ)) < π β (absβ((πΉβπ¦) β (πΉβπΆ))) < πΈ)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β πΆ)) < π ) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β πΆ)) < π ) β β’ ((π β§ π < π) β (absβ((((πΊβπ) β (πΊβπ)) / (π β π)) β (πΉβπΆ))) < πΈ) | ||
Theorem | ftc1lem5 25962* | Lemma for ftc1 25964. (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 25963* | Lemma for ftc1 25964. (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 25964* | 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 25965* | Strengthen the assumptions of ftc1 25964 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 25966* | 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 25967* | Lemma for ftc2ditg 25968. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β (π[,]π)) & β’ (π β π΅ β (π[,]π)) & β’ (π β (β D πΉ) β ((π(,)π)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π[,]π)βcnββ)) β β’ ((π β§ π΄ β€ π΅) β β¨[π΄ β π΅]((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | ftc2ditg 25968* | Directed integral analogue of ftc2 25966. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β (π[,]π)) & β’ (π β π΅ β (π[,]π)) & β’ (π β (β D πΉ) β ((π(,)π)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π[,]π)βcnββ)) β β’ (π β β¨[π΄ β π΅]((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | itgparts 25969* | 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 25970* | Lemma for itgsubst 25971. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(π(,)π))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (π’ β (π(,)π) β¦ πΆ) β ((π(,)π)βcnββ)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) & β’ (π β π β (π(,)π)) & β’ (π β π β (π(,)π)) & β’ ((π β§ π₯ β (π[,]π)) β π΄ β (π(,)π)) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubst 25971* | 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 25970, 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 25972* | 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 25973 | Multivariate polynomial degree. |
class mDeg | ||
Syntax | cdg1 25974 | Univariate polynomial degree. |
class deg1 | ||
Definition | df-mdeg 25975* | 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 26112. (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 25976 | Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ deg1 = (π β V β¦ (1o mDeg π)) | ||
Theorem | reldmmdeg 25977 | Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ Rel dom mDeg | ||
Theorem | tdeglem1 25978* | 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 25979* | Obsolete version of tdeglem1 25978 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 25980* | 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 25981* | Obsolete version of tdeglem3 25980 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 25982* | 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 25983* | Obsolete version of tdeglem4 25982 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 25984 | 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 25985* | 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 25986* | 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 25987* | 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 25988* | 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 25989* | 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 25990 | 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 25991 | 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 25992 | Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β (β0 βͺ {-β})) | ||
Theorem | mdeg0 25993 | 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 25994 | Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π·βπΉ) β β0) | ||
Theorem | degltlem1 25995 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ ((π β (β0 βͺ {-β}) β§ π β β€) β (π < π β π β€ (π β 1))) | ||
Theorem | degltp1le 25996 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ ((π β (β0 βͺ {-β}) β§ π β β€) β (π < (π + 1) β π β€ π)) | ||
Theorem | mdegaddle 25997 | 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 25998 | 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 25999 | 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 26000 | 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}))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |