Proof of Theorem fourier2
Step | Hyp | Ref
| Expression |
1 | | fourier2.f |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | | fourier2.t |
. . . . . 6
⊢ 𝑇 = (2 ·
π) |
3 | | fourier2.per |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
4 | | fourier2.g |
. . . . . 6
⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) |
5 | | fourier2.dmdv |
. . . . . 6
⊢ (𝜑 → ((-π(,)π) ∖
dom 𝐺) ∈
Fin) |
6 | | fourier2.dvcn |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) |
7 | | fourier2.rlim |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) |
8 | | fourier2.llim |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) |
9 | | fourier2.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℝ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | fourierdlem106 43428 |
. . . . 5
⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠
∅)) |
11 | 10 | simpld 498 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅) |
12 | | n0 4261 |
. . . 4
⊢ (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ↔
∃𝑙 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
13 | 11, 12 | sylib 221 |
. . 3
⊢ (𝜑 → ∃𝑙 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
14 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
15 | 10 | simprd 499 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅) |
16 | | n0 4261 |
. . . . . . . . . 10
⊢ (((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅ ↔
∃𝑟 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
17 | 15, 16 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑟 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
18 | 17 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → ∃𝑟 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
19 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
20 | 1 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → 𝐹:ℝ⟶ℝ) |
21 | 3 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
22 | 5 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → ((-π(,)π)
∖ dom 𝐺) ∈
Fin) |
23 | 6 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → 𝐺 ∈ (dom 𝐺–cn→ℂ)) |
24 | 7 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) |
25 | 8 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) |
26 | 9 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → 𝑋 ∈ ℝ) |
27 | 14 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
28 | | fourier2.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦
(∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) |
29 | | fourier2.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (𝑛 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) |
30 | 20, 2, 21, 4, 22, 23, 24, 25, 26, 27, 19, 28, 29 | fourierd 43438 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)) |
31 | 19, 30 | jca 515 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) ∧ 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) → (𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))) |
32 | 31 | ex 416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → (𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) → (𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)))) |
33 | 32 | eximdv 1925 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → (∃𝑟 𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) → ∃𝑟(𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)))) |
34 | 18, 33 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → ∃𝑟(𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))) |
35 | | df-rex 3067 |
. . . . . . 7
⊢
(∃𝑟 ∈
((𝐹 ↾ (𝑋(,)+∞))
limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2) ↔ ∃𝑟(𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))) |
36 | 34, 35 | sylibr 237 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → ∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)) |
37 | 14, 36 | jca 515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) → (𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ∧ ∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))) |
38 | 37 | ex 416 |
. . . 4
⊢ (𝜑 → (𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) → (𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ∧ ∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)))) |
39 | 38 | eximdv 1925 |
. . 3
⊢ (𝜑 → (∃𝑙 𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) → ∃𝑙(𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ∧ ∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)))) |
40 | 13, 39 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑙(𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ∧ ∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))) |
41 | | df-rex 3067 |
. 2
⊢
(∃𝑙 ∈
((𝐹 ↾
(-∞(,)𝑋))
limℂ 𝑋)∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2) ↔ ∃𝑙(𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ∧ ∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2))) |
42 | 40, 41 | sylibr 237 |
1
⊢ (𝜑 → ∃𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)) |