Home | Metamath
Proof Explorer Theorem List (p. 392 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fourierdlem102 39101* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) & ⊢ 𝑀 = ((#‘𝐻) − 1) & ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻)) ⇒ ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅)) | ||
Theorem | fourierdlem103 39102* | The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ 𝑍 = (𝑚 ∈ ℕ ↦ ∫(-π(,)0)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑚)‘𝑠)) d𝑠) & ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ (∫(-π(,)0)(𝐺‘𝑠) d𝑠 / π)) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐵 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ 𝑂 = (𝑈 ↾ (-π[,]𝑑)) & ⊢ 𝑇 = ({-π, 𝑑} ∪ (ran 𝑄 ∩ (-π(,)𝑑))) & ⊢ 𝑁 = ((#‘𝑇) − 1) & ⊢ 𝐽 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝐶 = (℩𝑙 ∈ (0..^𝑀)((𝐽‘𝑘)(,)(𝐽‘(𝑘 + 1))) ⊆ ((𝑄‘𝑙)(,)(𝑄‘(𝑙 + 1)))) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ (-π(,)0)) ∧ 𝑘 ∈ ℕ) ∧ (abs‘∫(𝑑(,)0)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)) ∧ (abs‘∫(-π(,)𝑑)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))) ⇒ ⊢ (𝜑 → 𝑍 ⇝ (𝑊 / 2)) | ||
Theorem | fourierdlem104 39103* | The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ 𝑍 = (𝑚 ∈ ℕ ↦ ∫(0(,)π)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑚)‘𝑠)) d𝑠) & ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ (∫(0(,)π)(𝐺‘𝑠) d𝑠 / π)) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐵 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ 𝑂 = (𝑈 ↾ (𝑑[,]π)) & ⊢ 𝑇 = ({𝑑, π} ∪ (ran 𝑄 ∩ (𝑑(,)π))) & ⊢ 𝑁 = ((#‘𝑇) − 1) & ⊢ 𝐽 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝐶 = (℩𝑙 ∈ (0..^𝑀)((𝐽‘𝑘)(,)(𝐽‘(𝑘 + 1))) ⊆ ((𝑄‘𝑙)(,)(𝑄‘(𝑙 + 1)))) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ (0(,)π)) ∧ 𝑘 ∈ ℕ) ∧ (abs‘∫(0(,)𝑑)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)) ∧ (abs‘∫(𝑑(,)π)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))) ⇒ ⊢ (𝜑 → 𝑍 ⇝ (𝑌 / 2)) | ||
Theorem | fourierdlem105 39104* | A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹‘𝑥)) ∈ 𝐿1) | ||
Theorem | fourierdlem106 39105* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅)) | ||
Theorem | fourierdlem107 39106* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 39091 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({(𝐴 − 𝑋), 𝐴} ∪ {𝑦 ∈ ((𝐴 − 𝑋)[,]𝐴) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((#‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem108 39107* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 39091 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem109 39108* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any value 𝑋. This lemma generalizes fourierdlem92 39091 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = (𝐵 − 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({(𝐴 − 𝑋), (𝐵 − 𝑋)} ∪ {𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((#‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐽 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ (𝐽‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem110 39109* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any value 𝑋. This lemma generalizes fourierdlem92 39091 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem111 39110* | The fourier partial sum for 𝐹 is the sum of two integrals, with the same integrand involving 𝐹 and the Dirichlet Kernel 𝐷, but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑡) · (cos‘(𝑛 · 𝑡))) d𝑡 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑡) · (sin‘(𝑛 · 𝑡))) d𝑡 / π)) & ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ ((𝐹‘(𝑋 + 𝑥)) · ((𝐷‘𝑛)‘𝑥))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝑇 = (2 · π) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π − 𝑋) ∧ (𝑝‘𝑚) = (π − 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑊 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) ⇒ ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = (∫(-π(,)0)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠 + ∫(0(,)π)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠)) | ||
Theorem | fourierdlem112 39111* | Here abbreviations (local definitions) are introduced to prove the fourier 39118 theorem. (𝑍‘𝑚) is the mth partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝐷 = (𝑚 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑚) + 1) / (2 · π)), ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ 𝑁 = ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) & ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐶 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑈 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ (𝜑 → 𝐸 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐼 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑍 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) & ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierdlem113 39112* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) & ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierdlem114 39113* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) & ⊢ 𝑀 = ((#‘𝐻) − 1) & ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻)) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierdlem115 39114* | Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierd 39115* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 39119. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 39120 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 39125. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)) | ||
Theorem | fourierclimd 39116* | Fourier series convergence, for piecewise smooth functions. See fourierd 39115 for the analogous Σ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ⇒ ⊢ (𝜑 → seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2))) | ||
Theorem | fourierclim 39117* | Fourier series convergence, for piecewise smooth functions. See fourier 39118 for the analogous Σ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹:ℝ⟶ℝ & ⊢ 𝑇 = (2 · π) & ⊢ (𝑥 ∈ ℝ → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ ((-π(,)π) ∖ dom 𝐺) ∈ Fin & ⊢ 𝐺 ∈ (dom 𝐺–cn→ℂ) & ⊢ (𝑥 ∈ ((-π[,)π) ∖ dom 𝐺) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ (𝑥 ∈ ((-π(,]π) ∖ dom 𝐺) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) & ⊢ 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ⇒ ⊢ seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) | ||
Theorem | fourier 39118* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 39119. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 39120 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 39125. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹:ℝ⟶ℝ & ⊢ 𝑇 = (2 · π) & ⊢ (𝑥 ∈ ℝ → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ ((-π(,)π) ∖ dom 𝐺) ∈ Fin & ⊢ 𝐺 ∈ (dom 𝐺–cn→ℂ) & ⊢ (𝑥 ∈ ((-π[,)π) ∖ dom 𝐺) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ (𝑥 ∈ ((-π(,]π) ∖ dom 𝐺) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) & ⊢ 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2) | ||
Theorem | fouriercnp 39119* | If 𝐹 is continuous at the point 𝑋, then its Fourier series at 𝑋, converges to (𝐹‘𝑋). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐽)‘𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝐹‘𝑋)) | ||
Theorem | fourier2 39120* | Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of 𝐹 at any given point 𝑋. See fourierd 39115 for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → ∃𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)) | ||
Theorem | sqwvfoura 39121* | Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the 𝐴 coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0) | ||
Theorem | sqwvfourb 39122* | Fourier series 𝐵 coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π)))) | ||
Theorem | fourierswlem 39123* | The Fourier series for the square wave 𝐹 converges to 𝑌, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) ⇒ ⊢ 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) | ||
Theorem | fouriersw 39124* | Fourier series convergence, for the square wave function. Where 𝐹 is discontinuous, the series converges to 0, the average value of the left and the right limits. Notice that 𝐹 is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((sin‘(((2 · 𝑛) − 1) · 𝑋)) / ((2 · 𝑛) − 1))) & ⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) ⇒ ⊢ (((4 / π) · Σ𝑘 ∈ ℕ ((sin‘(((2 · 𝑘) − 1) · 𝑋)) / ((2 · 𝑘) − 1))) = 𝑌 ∧ seq1( + , 𝑆) ⇝ ((π / 4) · 𝑌)) | ||
Theorem | fouriercn 39125* | If the derivative of 𝐹 is continuous, then the Fourier series for 𝐹 converges to 𝐹 everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function ( see fourierd 39115 for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (ℝ–cn→ℂ)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝐹‘𝑋)) | ||
Theorem | elaa2lem 39126* | Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 39127. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝔸) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝐺 ≠ 0𝑝) & ⊢ (𝜑 → (𝐺‘𝐴) = 0) & ⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) & ⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))) & ⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) | ||
Theorem | elaa2 39127* | Elementhood in the set of nonzero algebraic numbers: when 𝐴 is nonzero, the polynomial 𝑓 can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 1-Oct-2020.) |
⊢ (𝐴 ∈ (𝔸 ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))) | ||
Theorem | etransclem1 39128* | 𝐻 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → (𝐻‘𝐽):𝑋⟶ℂ) | ||
Theorem | etransclem2 39129* | Derivative of 𝐺. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) | ||
Theorem | etransclem3 39130 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) | ||
Theorem | etransclem4 39131* | 𝐹 expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐸 = (𝑥 ∈ 𝐴 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐸) | ||
Theorem | etransclem5 39132* | A change of bound variable, often used in proofs for etransc 39176. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) | ||
Theorem | etransclem6 39133* | A change of bound variable, often used in proofs for etransc 39176. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) | ||
Theorem | etransclem7 39134* | The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) | ||
Theorem | etransclem8 39135* | 𝐹 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) | ||
Theorem | etransclem9 39136 | If 𝐾 divides 𝑁 but 𝐾 does not divide 𝑀 then 𝑀 + 𝑁 cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≠ 0) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → ¬ 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 + 𝑁) ≠ 0) | ||
Theorem | etransclem10 39137 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈ ℤ) | ||
Theorem | etransclem11 39138* | A change of bound variable, often used in proofs for etransc 39176. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑𝑚 (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) | ||
Theorem | etransclem12 39139* | 𝐶 applied to 𝑁. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) = {𝑐 ∈ ((0...𝑁) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) | ||
Theorem | etransclem13 39140* | 𝐹 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘𝑌) = ∏𝑗 ∈ (0...𝑀)((𝑌 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) | ||
Theorem | etransclem14 39141* | Value of the term 𝑇, when 𝐽 = 0 and (𝐶‘0) = 𝑃 − 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) & ⊢ (𝜑 → 𝐽 = 0) & ⊢ (𝜑 → (𝐶‘0) = (𝑃 − 1)) ⇒ ⊢ (𝜑 → 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · (-𝑗↑(𝑃 − (𝐶‘𝑗)))))))) | ||
Theorem | etransclem15 39142* | Value of the term 𝑇, when 𝐽 = 0 and (𝐶‘0) = 𝑃 − 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) & ⊢ (𝜑 → 𝐽 = 0) & ⊢ (𝜑 → (𝐶‘0) ≠ (𝑃 − 1)) ⇒ ⊢ (𝜑 → 𝑇 = 0) | ||
Theorem | etransclem16 39143* | Every element in the range of 𝐶 is a finite set . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin) | ||
Theorem | etransclem17 39144* | The 𝑁-th derivative of 𝐻. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) | ||
Theorem | etransclem18 39145* | The given function is integrable . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → ℝ ∈ {ℝ, ℂ}) & ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿1) | ||
Theorem | etransclem19 39146* | The 𝑁-th derivative of 𝐻 is 0 if 𝑁 is large enough. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)) | ||
Theorem | etransclem20 39147* | 𝐻 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁):𝑋⟶ℂ) | ||
Theorem | etransclem21 39148* | The 𝑁-th derivative of 𝐻 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁)‘𝑌) = if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) | ||
Theorem | etransclem22 39149* | The 𝑁-th derivative of 𝐻 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem23 39150* | This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) & ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) & ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1))) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1) ⇒ ⊢ (𝜑 → (abs‘𝐾) < 1) | ||
Theorem | etransclem24 39151* | 𝑃 divides the I -th derivative of 𝐹 applied to 𝐽. when 𝐽 = 0 and 𝐼 is not equal to 𝑃 − 1. This is the second part of case 2 proven in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ≠ (𝑃 − 1)) & ⊢ (𝜑 → 𝐽 = 0) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝐼)) ⇒ ⊢ (𝜑 → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem25 39152* | 𝑃 factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗) = 𝑁) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (!‘𝑃) ∥ 𝑇) | ||
Theorem | etransclem26 39153* | Every term in the sum of the 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝑁)) ⇒ ⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) ∈ ℤ) | ||
Theorem | etransclem27 39154* | The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐶:dom 𝐶⟶(ℕ0 ↑𝑚 (0...𝑀))) & ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑙 ∈ dom 𝐶∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘((𝐶‘𝑙)‘𝑗))‘𝑥)) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐺‘𝐽) ∈ ℤ) | ||
Theorem | etransclem28 39155* | (𝑃 − 1) factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) ⇒ ⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ 𝑇) | ||
Theorem | etransclem29 39156* | The 𝑁-th derivative of 𝐹. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ 𝐸 = (𝑥 ∈ 𝑋 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)))) | ||
Theorem | etransclem30 39157* | The 𝑁-th derivative of 𝐹. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)))) | ||
Theorem | etransclem31 39158* | The 𝑁-th derivative of 𝐻 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑌) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝑌↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝑌 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) | ||
Theorem | etransclem32 39159* | This is the proof for the last equation in the proof of the derivative calculated in [Juillerat] p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < 𝑁) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)) | ||
Theorem | etransclem33 39160* | 𝐹 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝑋⟶ℂ) | ||
Theorem | etransclem34 39161* | The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑘 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = 𝑛}) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem35 39162* | 𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)) ⇒ ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))) | ||
Theorem | etransclem36 39163* | The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽) ∈ ℤ) | ||
Theorem | etransclem37 39164* | (𝑃 − 1) factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽)) | ||
Theorem | etransclem38 39165* | 𝑃 divides the I -th derivative of 𝐹 applied to 𝐽. if it is not the case that 𝐼 = 𝑃 − 1 and 𝐽 = 0. This is case 1 and the second part of case 2 proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → ¬ (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0)) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) ⇒ ⊢ (𝜑 → 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘𝐼)‘𝐽) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem39 39166* | 𝐺 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐺:ℝ⟶ℂ) | ||
Theorem | etransclem40 39167* | The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem41 39168* | 𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is the first part of case 2: proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (!‘𝑀) < 𝑃) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) ⇒ ⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem42 39169* | The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽) ∈ ℤ) | ||
Theorem | etransclem43 39170* | 𝐺 is a continuous function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (0...𝑅)(((𝑆 D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem44 39171* | The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) & ⊢ (𝜑 → (𝐴‘0) ≠ 0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃) & ⊢ (𝜑 → (!‘𝑀) < 𝑃) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1))) ⇒ ⊢ (𝜑 → 𝐾 ≠ 0) | ||
Theorem | etransclem45 39172* | 𝐾 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) & ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1))) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
Theorem | etransclem46 39173* | This is the proof for equation *(7) in [Juillerat] p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large 𝑃, but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝑄‘e) = 0) & ⊢ 𝐴 = (coeff‘𝑄) & ⊢ 𝑀 = (deg‘𝑄) & ⊢ (𝜑 → ℝ ⊆ ℝ) & ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ}) & ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) & ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1)) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) & ⊢ 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem47 39174* | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝑄‘e) = 0) & ⊢ 𝐴 = (coeff‘𝑄) & ⊢ (𝜑 → (𝐴‘0) ≠ 0) & ⊢ 𝑀 = (deg‘𝑄) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃) & ⊢ (𝜑 → (!‘𝑀) < 𝑃) & ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) & ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1))) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)) | ||
Theorem | etransclem48 39175* | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. In this lemma, a large enough prime 𝑝 is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.) |
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝑄‘e) = 0) & ⊢ 𝐴 = (coeff‘𝑄) & ⊢ (𝜑 → (𝐴‘0) ≠ 0) & ⊢ 𝑀 = (deg‘𝑄) & ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) & ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) & ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) & ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)) | ||
Theorem | etransc 39176 | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ e ∈ (ℂ ∖ 𝔸) | ||
Theorem | rrxtopn 39177* | The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) ⇒ ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))) | ||
Theorem | rrxngp 39178 | Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ NrmGrp) | ||
Theorem | rrxbasefi 39179 | The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of (ℝ ↑𝑚 𝑋) for the development of the Lebeasgue measure theory for n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐻 = (ℝ^‘𝑋) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝜑 → 𝐵 = (ℝ ↑𝑚 𝑋)) | ||
Theorem | rrxtps 39180 | Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ TopSp) | ||
Theorem | rrxdsfi 39181* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (ℝ ↑𝑚 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (dist‘𝐻) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxtopnfi 39182* | The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) ⇒ ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑𝑚 𝐼), 𝑔 ∈ (ℝ ↑𝑚 𝐼) ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) | ||
Theorem | rrxmetfi 39183 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑𝑚 𝐼))) | ||
Theorem | rrxtopon 39184 | The topology on Generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ (TopOn‘(Base‘(ℝ^‘𝐼)))) | ||
Theorem | rrxtop 39185 | The topology on Generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ Top) | ||
Theorem | rrndistlt 39186* | Given two points in the space of n-dimensional real numbers, if every component is closer than 𝐸 then the distance between the two points is less then ((√‘𝑛) · 𝐸) (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐼 ≠ ∅) & ⊢ 𝑁 = (#‘𝐼) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑𝑚 𝐼)) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑𝑚 𝐼)) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑌‘𝑖))) < 𝐸) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → (𝑋𝐷𝑌) < ((√‘𝑁) · 𝐸)) | ||
Theorem | rrxtoponfi 39187 | The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐽 ∈ (TopOn‘(ℝ ↑𝑚 𝐼))) | ||
Theorem | rrxunitopnfi 39188 | The base set of the standard topology on the space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝑋 ∈ Fin → ∪ (TopOpen‘(ℝ^‘𝑋)) = (ℝ ↑𝑚 𝑋)) | ||
Theorem | rrxtopn0 39189 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (TopOpen‘(ℝ^‘∅)) = 𝒫 {∅} | ||
Theorem | qndenserrnbllem 39190* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐼 ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑𝑚 𝐼)) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) | ||
Theorem | qndenserrnbl 39191* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑𝑚 𝐼)) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) | ||
Theorem | rrxtopn0b 39192 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}} | ||
Theorem | qndenserrnopnlem 39193* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ 𝑉) | ||
Theorem | qndenserrnopn 39194* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚 𝐼)𝑦 ∈ 𝑉) | ||
Theorem | qndenserrn 39195 | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘(ℚ ↑𝑚 𝐼)) = (ℝ ↑𝑚 𝐼)) | ||
Theorem | rrxsnicc 39196* | A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑𝑚 𝑋)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴}) | ||
Theorem | rrnprjdstle 39197 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ 𝐷 = (dist‘(ℝ^‘𝑋)) ⇒ ⊢ (𝜑 → (abs‘((𝐹‘𝐼) − (𝐺‘𝐼))) ≤ (𝐹𝐷𝐺)) | ||
Theorem | rrndsmet 39198* | 𝐷 is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ ↑𝑚 𝑋))) | ||
Theorem | rrndsxmet 39199* | 𝐷 is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ ↑𝑚 𝑋))) | ||
Theorem | ioorrnopnlem 39200* | The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) & ⊢ 𝐻 = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) & ⊢ 𝐸 = inf(𝐻, ℝ, < ) & ⊢ 𝑉 = (𝐹(ball‘𝐷)𝐸) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑𝑚 𝑋), 𝑔 ∈ (ℝ ↑𝑚 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |