| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem115.f | . . . 4
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 2 |  | fourierdlem115.t | . . . 4
⊢ 𝑇 = (2 ·
π) | 
| 3 |  | fourierdlem115.per | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) | 
| 4 |  | fourierdlem115.g | . . . 4
⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) | 
| 5 |  | fourierdlem115.dmdv | . . . 4
⊢ (𝜑 → ((-π(,)π) ∖
dom 𝐺) ∈
Fin) | 
| 6 |  | fourierdlem115.dvcn | . . . 4
⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) | 
| 7 |  | fourierdlem115.rlim | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) | 
| 8 |  | fourierdlem115.llim | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) | 
| 9 |  | fourierdlem115.x | . . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 10 |  | fourierdlem115.l | . . . 4
⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) | 
| 11 |  | fourierdlem115.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) | 
| 12 |  | fourierdlem115.a | . . . . 5
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦
(∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) | 
| 13 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 · 𝑥) = (𝑘 · 𝑥)) | 
| 14 | 13 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑘 · 𝑥))) | 
| 15 | 14 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥)))) | 
| 16 | 15 | adantr 480 | . . . . . . . 8
⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ (-π(,)π)) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥)))) | 
| 17 | 16 | itgeq2dv 25818 | . . . . . . 7
⊢ (𝑛 = 𝑘 → ∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥) | 
| 18 | 17 | oveq1d 7447 | . . . . . 6
⊢ (𝑛 = 𝑘 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 / π)) | 
| 19 | 18 | cbvmptv 5254 | . . . . 5
⊢ (𝑛 ∈ ℕ0
↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (𝑘 ∈ ℕ0 ↦
(∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 / π)) | 
| 20 | 12, 19 | eqtri 2764 | . . . 4
⊢ 𝐴 = (𝑘 ∈ ℕ0 ↦
(∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 / π)) | 
| 21 |  | fourierdlem115.b | . . . . 5
⊢ 𝐵 = (𝑛 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) | 
| 22 | 13 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑘 · 𝑥))) | 
| 23 | 22 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥)))) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ (-π(,)π)) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥)))) | 
| 25 | 24 | itgeq2dv 25818 | . . . . . . 7
⊢ (𝑛 = 𝑘 → ∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 = ∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥) | 
| 26 | 25 | oveq1d 7447 | . . . . . 6
⊢ (𝑛 = 𝑘 → (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) = (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 / π)) | 
| 27 | 26 | cbvmptv 5254 | . . . . 5
⊢ (𝑛 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (𝑘 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 / π)) | 
| 28 | 21, 27 | eqtri 2764 | . . . 4
⊢ 𝐵 = (𝑘 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 / π)) | 
| 29 |  | fourierdlem115.s | . . . 4
⊢ 𝑆 = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) | 
| 30 |  | eqid 2736 | . . . 4
⊢ (𝑘 ∈ ℕ ↦ {𝑤 ∈ (ℝ
↑m (0...𝑘))
∣ (((𝑤‘0) =
-π ∧ (𝑤‘𝑘) = π) ∧ ∀𝑧 ∈ (0..^𝑘)(𝑤‘𝑧) < (𝑤‘(𝑧 + 1)))}) = (𝑘 ∈ ℕ ↦ {𝑤 ∈ (ℝ ↑m
(0...𝑘)) ∣ (((𝑤‘0) = -π ∧ (𝑤‘𝑘) = π) ∧ ∀𝑧 ∈ (0..^𝑘)(𝑤‘𝑧) < (𝑤‘(𝑧 + 1)))}) | 
| 31 |  | id 22 | . . . . . 6
⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥) | 
| 32 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥)) | 
| 33 | 32 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇)) | 
| 34 | 33 | fveq2d 6909 | . . . . . . 7
⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇))) | 
| 35 | 34 | oveq1d 7447 | . . . . . 6
⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)) | 
| 36 | 31, 35 | oveq12d 7450 | . . . . 5
⊢ (𝑦 = 𝑥 → (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) | 
| 37 | 36 | cbvmptv 5254 | . . . 4
⊢ (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π
− 𝑦) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) | 
| 38 |  | eqid 2736 | . . . 4
⊢ ({-π,
π, ((𝑦 ∈ ℝ
↦ (𝑦 +
((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) = ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π
− 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) | 
| 39 |  | eqid 2736 | . . . 4
⊢
((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1) =
((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1) | 
| 40 |  | isoeq1 7338 | . . . . 5
⊢ (𝑔 = 𝑓 → (𝑔 Isom < , <
((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π,
((𝑦 ∈ ℝ ↦
(𝑦 + ((⌊‘((π
− 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) ↔ 𝑓 Isom < , <
((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π,
((𝑦 ∈ ℝ ↦
(𝑦 + ((⌊‘((π
− 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))))) | 
| 41 | 40 | cbviotavw 6521 | . . . 4
⊢
(℩𝑔𝑔 Isom < , <
((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π,
((𝑦 ∈ ℝ ↦
(𝑦 + ((⌊‘((π
− 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))) = (℩𝑓𝑓 Isom < , <
((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π,
((𝑦 ∈ ℝ ↦
(𝑦 + ((⌊‘((π
− 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))) | 
| 42 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 20, 28, 29, 30, 37, 38, 39, 41 | fourierdlem114 46240 | . . 3
⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | 
| 43 | 42 | simpld 494 | . 2
⊢ (𝜑 → seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2))) | 
| 44 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) | 
| 45 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋)) | 
| 46 | 45 | fveq2d 6909 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋))) | 
| 47 | 44, 46 | oveq12d 7450 | . . . . . 6
⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋)))) | 
| 48 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘)) | 
| 49 | 45 | fveq2d 6909 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋))) | 
| 50 | 48, 49 | oveq12d 7450 | . . . . . 6
⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) | 
| 51 | 47, 50 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) | 
| 52 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑘(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) | 
| 53 |  | nfmpt1 5249 | . . . . . . . . 9
⊢
Ⅎ𝑛(𝑛 ∈ ℕ0 ↦
(∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) | 
| 54 | 12, 53 | nfcxfr 2902 | . . . . . . . 8
⊢
Ⅎ𝑛𝐴 | 
| 55 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑛𝑘 | 
| 56 | 54, 55 | nffv 6915 | . . . . . . 7
⊢
Ⅎ𝑛(𝐴‘𝑘) | 
| 57 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑛
· | 
| 58 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑛(cos‘(𝑘 · 𝑋)) | 
| 59 | 56, 57, 58 | nfov 7462 | . . . . . 6
⊢
Ⅎ𝑛((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) | 
| 60 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑛
+ | 
| 61 |  | nfmpt1 5249 | . . . . . . . . 9
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) | 
| 62 | 21, 61 | nfcxfr 2902 | . . . . . . . 8
⊢
Ⅎ𝑛𝐵 | 
| 63 | 62, 55 | nffv 6915 | . . . . . . 7
⊢
Ⅎ𝑛(𝐵‘𝑘) | 
| 64 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑛(sin‘(𝑘 · 𝑋)) | 
| 65 | 63, 57, 64 | nfov 7462 | . . . . . 6
⊢
Ⅎ𝑛((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))) | 
| 66 | 59, 60, 65 | nfov 7462 | . . . . 5
⊢
Ⅎ𝑛(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) | 
| 67 | 51, 52, 66 | cbvsum 15732 | . . . 4
⊢
Σ𝑛 ∈
ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) | 
| 68 | 67 | oveq2i 7443 | . . 3
⊢ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) | 
| 69 | 42 | simprd 495 | . . 3
⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = ((𝐿 + 𝑅) / 2)) | 
| 70 | 68, 69 | eqtrid 2788 | . 2
⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)) | 
| 71 | 43, 70 | jca 511 | 1
⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) |