![]() |
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 > |