Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
2 | | fourierdlem95.ass |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ((-π[,]π) ∖
{0})) |
3 | 2 | difss2d 4025 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ (-π[,]π)) |
4 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ (-π[,]π)) |
5 | 4 | sselda 3877 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (-π[,]π)) |
6 | | fourierdlem95.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
7 | 6 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℝ⟶ℝ) |
8 | | fourierdlem95.xre |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
9 | 8 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ ℝ) |
10 | | ioossre 12882 |
. . . . . . . . . . . . 13
⊢ (𝑋(,)+∞) ⊆
ℝ |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋(,)+∞) ⊆
ℝ) |
12 | 6, 11 | fssresd 6545 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ (𝑋(,)+∞)):(𝑋(,)+∞)⟶ℝ) |
13 | | ioosscn 12883 |
. . . . . . . . . . . 12
⊢ (𝑋(,)+∞) ⊆
ℂ |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋(,)+∞) ⊆
ℂ) |
15 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
16 | | pnfxr 10773 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → +∞ ∈
ℝ*) |
18 | 8 | ltpnfd 12599 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 < +∞) |
19 | 15, 17, 8, 18 | lptioo1cn 42729 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)+∞))) |
20 | | fourierdlem95.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
21 | 12, 14, 19, 20 | limcrecl 42712 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
22 | 21 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑌 ∈ ℝ) |
23 | | ioossre 12882 |
. . . . . . . . . . . . 13
⊢
(-∞(,)𝑋)
⊆ ℝ |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-∞(,)𝑋) ⊆
ℝ) |
25 | 6, 24 | fssresd 6545 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ) |
26 | | ioosscn 12883 |
. . . . . . . . . . . 12
⊢
(-∞(,)𝑋)
⊆ ℂ |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (-∞(,)𝑋) ⊆
ℂ) |
28 | | mnfxr 10776 |
. . . . . . . . . . . . 13
⊢ -∞
∈ ℝ* |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → -∞ ∈
ℝ*) |
30 | 8 | mnfltd 12602 |
. . . . . . . . . . . 12
⊢ (𝜑 → -∞ < 𝑋) |
31 | 15, 29, 8, 30 | lptioo2cn 42728 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
((limPt‘(TopOpen‘ℂfld))‘(-∞(,)𝑋))) |
32 | | fourierdlem95.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
33 | 25, 27, 31, 32 | limcrecl 42712 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℝ) |
34 | 33 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ) |
35 | | fourierdlem95.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) |
36 | | fourierdlem95.k |
. . . . . . . . 9
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) |
37 | | fourierdlem95.u |
. . . . . . . . 9
⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) |
38 | 1 | nnred 11731 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
39 | | fourierdlem95.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑛 + (1 / 2))
· 𝑠))) |
40 | | fourierdlem95.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) |
41 | 7, 9, 22, 34, 35, 36, 37, 38, 39, 40 | fourierdlem67 43256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:(-π[,]π)⟶ℝ) |
42 | 41 | ffvelrnda 6861 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → (𝐺‘𝑠) ∈ ℝ) |
43 | 5, 42 | syldan 594 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝐺‘𝑠) ∈ ℝ) |
44 | | fourierdlem95.admvol |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ dom vol) |
45 | 44 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ dom vol) |
46 | 41 | feqmptd 6737 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 = (𝑠 ∈ (-π[,]π) ↦ (𝐺‘𝑠))) |
47 | | fourierdlem95.p |
. . . . . . . . 9
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
48 | | fourierdlem95.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ran 𝑉) |
49 | 48 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ ran 𝑉) |
50 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
51 | 32 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
52 | | fourierdlem95.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
53 | 52 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ) |
54 | | fourierdlem95.v |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) |
55 | 54 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑉 ∈ (𝑃‘𝑀)) |
56 | | fourierdlem95.fcn |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) |
57 | 56 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) |
58 | | fourierdlem95.r |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) |
59 | 58 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) |
60 | | fourierdlem95.l |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) |
61 | 60 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) |
62 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → (𝑉‘𝑗) = (𝑉‘𝑖)) |
63 | 62 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘𝑖) − 𝑋)) |
64 | 63 | cbvmptv 5133 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) |
65 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ
↑m (0...𝑚))
∣ (((𝑝‘0) =
-π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
66 | | fourierdlem95.i |
. . . . . . . . 9
⊢ 𝐼 = (ℝ D 𝐹) |
67 | | fourierdlem95.ifn |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐼 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ) |
68 | 67 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐼 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ) |
69 | | fourierdlem95.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ((𝐼 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
70 | 69 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ((𝐼 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
71 | | fourierdlem95.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((𝐼 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
72 | 71 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ((𝐼 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
73 | 47, 7, 49, 50, 51, 35, 36, 37, 38, 39, 40, 53, 55, 57, 59, 61, 64, 65, 66, 68, 70, 72 | fourierdlem88 43277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 ∈
𝐿1) |
74 | 46, 73 | eqeltrrd 2834 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ (-π[,]π) ↦ (𝐺‘𝑠)) ∈
𝐿1) |
75 | 4, 45, 42, 74 | iblss 24557 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ 𝐴 ↦ (𝐺‘𝑠)) ∈
𝐿1) |
76 | 43, 75 | itgrecl 24550 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴(𝐺‘𝑠) d𝑠 ∈ ℝ) |
77 | | pire 25203 |
. . . . . 6
⊢ π
∈ ℝ |
78 | 77 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈
ℝ) |
79 | | pipos 25205 |
. . . . . . 7
⊢ 0 <
π |
80 | 77, 79 | gt0ne0ii 11254 |
. . . . . 6
⊢ π ≠
0 |
81 | 80 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ≠
0) |
82 | 76, 78, 81 | redivcld 11546 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐴(𝐺‘𝑠) d𝑠 / π) ∈ ℝ) |
83 | | fourierlemenplusacver2eqitgdirker.e |
. . . . 5
⊢ 𝐸 = (𝑛 ∈ ℕ ↦ (∫𝐴(𝐺‘𝑠) d𝑠 / π)) |
84 | 83 | fvmpt2 6786 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧
(∫𝐴(𝐺‘𝑠) d𝑠 / π) ∈ ℝ) → (𝐸‘𝑛) = (∫𝐴(𝐺‘𝑠) d𝑠 / π)) |
85 | 1, 82, 84 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) = (∫𝐴(𝐺‘𝑠) d𝑠 / π)) |
86 | | fourierdlem95.o |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ ℝ) |
87 | 86 | recnd 10747 |
. . . . . 6
⊢ (𝜑 → 𝑂 ∈ ℂ) |
88 | | 2cnd 11794 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℂ) |
89 | | 2ne0 11820 |
. . . . . . 7
⊢ 2 ≠
0 |
90 | 89 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ≠ 0) |
91 | 87, 88, 90 | divrecd 11497 |
. . . . 5
⊢ (𝜑 → (𝑂 / 2) = (𝑂 · (1 / 2))) |
92 | 91 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂 / 2) = (𝑂 · (1 / 2))) |
93 | | fourierdlem95.itgdirker |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠 = (1 / 2)) |
94 | 93 | eqcomd 2744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 2) = ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠) |
95 | 94 | oveq2d 7186 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂 · (1 / 2)) = (𝑂 · ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠)) |
96 | 92, 95 | eqtrd 2773 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂 / 2) = (𝑂 · ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠)) |
97 | 85, 96 | oveq12d 7188 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑛) + (𝑂 / 2)) = ((∫𝐴(𝐺‘𝑠) d𝑠 / π) + (𝑂 · ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠))) |
98 | 2 | sselda 3877 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ((-π[,]π) ∖
{0})) |
99 | 98 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ((-π[,]π) ∖
{0})) |
100 | | fourierdlem95.d |
. . . . . . . 8
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) ·
(sin‘(𝑠 /
2))))))) |
101 | | eqid 2738 |
. . . . . . . 8
⊢
((-π[,]π) ∖ {0}) = ((-π[,]π) ∖
{0}) |
102 | 6, 8, 21, 33, 100, 35, 36, 37, 39, 40, 101 | fourierdlem66 43255 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) →
(𝐺‘𝑠) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)))) |
103 | 99, 102 | syldan 594 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝐺‘𝑠) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)))) |
104 | 103 | itgeq2dv 24534 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴(𝐺‘𝑠) d𝑠 = ∫𝐴(π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) d𝑠) |
105 | 104 | oveq1d 7185 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐴(𝐺‘𝑠) d𝑠 / π) = (∫𝐴(π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) d𝑠 / π)) |
106 | 78 | recnd 10747 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈
ℂ) |
107 | 6 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐹:ℝ⟶ℝ) |
108 | 8 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℝ) |
109 | | difss 4022 |
. . . . . . . . . . . . . 14
⊢
((-π[,]π) ∖ {0}) ⊆ (-π[,]π) |
110 | 77 | renegcli 11025 |
. . . . . . . . . . . . . . 15
⊢ -π
∈ ℝ |
111 | | iccssre 12903 |
. . . . . . . . . . . . . . 15
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
112 | 110, 77, 111 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
(-π[,]π) ⊆ ℝ |
113 | 109, 112 | sstri 3886 |
. . . . . . . . . . . . 13
⊢
((-π[,]π) ∖ {0}) ⊆ ℝ |
114 | 113, 98 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
115 | 108, 114 | readdcld 10748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ ℝ) |
116 | 107, 115 | ffvelrnd 6862 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) |
117 | 21, 33 | ifcld 4460 |
. . . . . . . . . . 11
⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ) |
118 | 117 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ) |
119 | 116, 118 | resubcld 11146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ) |
120 | 119 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ) |
121 | 1 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → 𝑛 ∈ ℕ) |
122 | 114 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
123 | 100 | dirkerre 43178 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ) → ((𝐷‘𝑛)‘𝑠) ∈ ℝ) |
124 | 121, 122,
123 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((𝐷‘𝑛)‘𝑠) ∈ ℝ) |
125 | 120, 124 | remulcld 10749 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) ∈ ℝ) |
126 | 103 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) = (𝐺‘𝑠)) |
127 | 126 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) / π) = ((𝐺‘𝑠) / π)) |
128 | | picn 25204 |
. . . . . . . . . . . . 13
⊢ π
∈ ℂ |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → π ∈
ℂ) |
130 | 125 | recnd 10747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) ∈ ℂ) |
131 | 80 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → π ≠ 0) |
132 | 129, 130,
129, 131 | div23d 11531 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) / π) = ((π / π) ·
(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)))) |
133 | 43 | recnd 10747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝐺‘𝑠) ∈ ℂ) |
134 | 133, 129,
131 | divrec2d 11498 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((𝐺‘𝑠) / π) = ((1 / π) · (𝐺‘𝑠))) |
135 | 127, 132,
134 | 3eqtr3rd 2782 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((1 / π) · (𝐺‘𝑠)) = ((π / π) · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)))) |
136 | 128, 80 | dividi 11451 |
. . . . . . . . . . . 12
⊢ (π /
π) = 1 |
137 | 136 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (π / π) = 1) |
138 | 137 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((π / π) · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) = (1 · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)))) |
139 | 130 | mulid2d 10737 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (1 · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) |
140 | 135, 138,
139 | 3eqtrrd 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) = ((1 / π) · (𝐺‘𝑠))) |
141 | 140 | mpteq2dva 5125 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ 𝐴 ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) = (𝑠 ∈ 𝐴 ↦ ((1 / π) · (𝐺‘𝑠)))) |
142 | 106, 81 | reccld 11487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / π) ∈
ℂ) |
143 | 142, 43, 75 | iblmulc2 24583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ 𝐴 ↦ ((1 / π) · (𝐺‘𝑠))) ∈
𝐿1) |
144 | 141, 143 | eqeltrd 2833 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ 𝐴 ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) ∈
𝐿1) |
145 | 106, 125,
144 | itgmulc2 24586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (π ·
∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) = ∫𝐴(π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) d𝑠) |
146 | 145 | eqcomd 2744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴(π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) d𝑠 = (π · ∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠)) |
147 | 146 | oveq1d 7185 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐴(π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))) d𝑠 / π) = ((π · ∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) / π)) |
148 | 125, 144 | itgcl 24536 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠 ∈ ℂ) |
149 | 148, 106,
81 | divcan3d 11499 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((π ·
∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) / π) = ∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) |
150 | 105, 147,
149 | 3eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐴(𝐺‘𝑠) d𝑠 / π) = ∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) |
151 | 87 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂 ∈ ℂ) |
152 | 112 | sseli 3873 |
. . . . . . 7
⊢ (𝑠 ∈ (-π[,]π) →
𝑠 ∈
ℝ) |
153 | 152, 123 | sylan2 596 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ 𝑠 ∈ (-π[,]π)) →
((𝐷‘𝑛)‘𝑠) ∈ ℝ) |
154 | 153 | adantll 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ (-π[,]π)) → ((𝐷‘𝑛)‘𝑠) ∈ ℝ) |
155 | 110 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -π ∈
ℝ) |
156 | | ax-resscn 10672 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
157 | 156 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ℝ
⊆ ℂ) |
158 | | ssid 3899 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
159 | | cncfss 23651 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
((-π[,]π)–cn→ℝ)
⊆ ((-π[,]π)–cn→ℂ)) |
160 | 157, 158,
159 | sylancl 589 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((-π[,]π)–cn→ℝ)
⊆ ((-π[,]π)–cn→ℂ)) |
161 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑠 ∈ ℝ ↦ ((𝐷‘𝑛)‘𝑠)) = (𝑠 ∈ ℝ ↦ ((𝐷‘𝑛)‘𝑠)) |
162 | 100 | dirkerf 43180 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛):ℝ⟶ℝ) |
163 | 162 | feqmptd 6737 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) = (𝑠 ∈ ℝ ↦ ((𝐷‘𝑛)‘𝑠))) |
164 | 100 | dirkercncf 43190 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) ∈ (ℝ–cn→ℝ)) |
165 | 163, 164 | eqeltrrd 2834 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑠 ∈ ℝ ↦ ((𝐷‘𝑛)‘𝑠)) ∈ (ℝ–cn→ℝ)) |
166 | 112 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(-π[,]π) ⊆ ℝ) |
167 | | ssid 3899 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ |
168 | 167 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ℝ
⊆ ℝ) |
169 | 161, 165,
166, 168, 153 | cncfmptssg 42954 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑠 ∈ (-π[,]π) ↦
((𝐷‘𝑛)‘𝑠)) ∈ ((-π[,]π)–cn→ℝ)) |
170 | 160, 169 | sseldd 3878 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (𝑠 ∈ (-π[,]π) ↦
((𝐷‘𝑛)‘𝑠)) ∈ ((-π[,]π)–cn→ℂ)) |
171 | 170 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ (-π[,]π) ↦ ((𝐷‘𝑛)‘𝑠)) ∈ ((-π[,]π)–cn→ℂ)) |
172 | | cniccibl 24593 |
. . . . . 6
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ (𝑠 ∈ (-π[,]π) ↦ ((𝐷‘𝑛)‘𝑠)) ∈ ((-π[,]π)–cn→ℂ)) → (𝑠 ∈ (-π[,]π) ↦ ((𝐷‘𝑛)‘𝑠)) ∈
𝐿1) |
173 | 155, 78, 171, 172 | syl3anc 1372 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ (-π[,]π) ↦ ((𝐷‘𝑛)‘𝑠)) ∈
𝐿1) |
174 | 4, 45, 154, 173 | iblss 24557 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ 𝐴 ↦ ((𝐷‘𝑛)‘𝑠)) ∈
𝐿1) |
175 | 151, 124,
174 | itgmulc2 24586 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂 · ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠) = ∫𝐴(𝑂 · ((𝐷‘𝑛)‘𝑠)) d𝑠) |
176 | 150, 175 | oveq12d 7188 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((∫𝐴(𝐺‘𝑠) d𝑠 / π) + (𝑂 · ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠)) = (∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠 + ∫𝐴(𝑂 · ((𝐷‘𝑛)‘𝑠)) d𝑠)) |
177 | 86 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → 𝑂 ∈ ℝ) |
178 | 177, 124 | remulcld 10749 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝑂 · ((𝐷‘𝑛)‘𝑠)) ∈ ℝ) |
179 | 151, 124,
174 | iblmulc2 24583 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑠 ∈ 𝐴 ↦ (𝑂 · ((𝐷‘𝑛)‘𝑠))) ∈
𝐿1) |
180 | 125, 144,
178, 179 | itgadd 24577 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) + (𝑂 · ((𝐷‘𝑛)‘𝑠))) d𝑠 = (∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠 + ∫𝐴(𝑂 · ((𝐷‘𝑛)‘𝑠)) d𝑠)) |
181 | | fourierdlem95.ifeqo |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑂) |
182 | 181 | eqcomd 2744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑂 = if(0 < 𝑠, 𝑌, 𝑊)) |
183 | 182 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → 𝑂 = if(0 < 𝑠, 𝑌, 𝑊)) |
184 | 183 | oveq1d 7185 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝑂 · ((𝐷‘𝑛)‘𝑠)) = (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠))) |
185 | 184 | oveq2d 7186 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) + (𝑂 · ((𝐷‘𝑛)‘𝑠))) = ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) + (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠)))) |
186 | 116 | recnd 10747 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
187 | 186 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
188 | 118 | recnd 10747 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) |
189 | 188 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) |
190 | 124 | recnd 10747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((𝐷‘𝑛)‘𝑠) ∈ ℂ) |
191 | 187, 189,
190 | subdird 11175 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) = (((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) − (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠)))) |
192 | 191 | oveq1d 7185 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) + (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠))) = ((((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) − (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠))) + (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠)))) |
193 | 187, 190 | mulcld 10739 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) ∈ ℂ) |
194 | 189, 190 | mulcld 10739 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠)) ∈ ℂ) |
195 | 193, 194 | npcand 11079 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) − (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠))) + (if(0 < 𝑠, 𝑌, 𝑊) · ((𝐷‘𝑛)‘𝑠))) = ((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠))) |
196 | 185, 192,
195 | 3eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) + (𝑂 · ((𝐷‘𝑛)‘𝑠))) = ((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠))) |
197 | 196 | itgeq2dv 24534 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) + (𝑂 · ((𝐷‘𝑛)‘𝑠))) d𝑠 = ∫𝐴((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) |
198 | 180, 197 | eqtr3d 2775 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐴(((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)) d𝑠 + ∫𝐴(𝑂 · ((𝐷‘𝑛)‘𝑠)) d𝑠) = ∫𝐴((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) |
199 | 97, 176, 198 | 3eqtrd 2777 |
1
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑛) + (𝑂 / 2)) = ∫𝐴((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) |