Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem83 Structured version   Visualization version   GIF version

Theorem fourierdlem83 45846
Description: The fourier partial sum for 𝐹 rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem83.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem83.c 𝐶 = (-π(,)π)
fourierdlem83.fl1 (𝜑 → (𝐹𝐶) ∈ 𝐿1)
fourierdlem83.a 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem83.b 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem83.x (𝜑𝑋 ∈ ℝ)
fourierdlem83.s 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
fourierdlem83.d 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
fourierdlem83.n (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
fourierdlem83 (𝜑 → (𝑆𝑁) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
Distinct variable groups:   𝐴,𝑚,𝑛   𝐵,𝑚   𝑥,𝐶,𝑛,𝑠   𝑥,𝐷,𝑠   𝑛,𝐹,𝑥   𝑥,𝑁   𝑚,𝑁,𝑛   𝑁,𝑠   𝑥,𝑋   𝑚,𝑋,𝑛   𝑋,𝑠   𝜑,𝑥,𝑛   𝜑,𝑚   𝜑,𝑠
Allowed substitution hints:   𝐴(𝑥,𝑠)   𝐵(𝑥,𝑛,𝑠)   𝐶(𝑚)   𝐷(𝑚,𝑛)   𝑆(𝑥,𝑚,𝑛,𝑠)   𝐹(𝑚,𝑠)

Proof of Theorem fourierdlem83
Dummy variables 𝑏 𝑐 𝑦 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem83.s . . . 4 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
21a1i 11 . . 3 (𝜑𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))))
3 oveq2 7424 . . . . . 6 (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
43sumeq1d 15700 . . . . 5 (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
54oveq2d 7432 . . . 4 (𝑚 = 𝑁 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
65adantl 480 . . 3 ((𝜑𝑚 = 𝑁) → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
7 fourierdlem83.n . . 3 (𝜑𝑁 ∈ ℕ)
8 id 22 . . . . . 6 (𝜑𝜑)
9 0nn0 12533 . . . . . . 7 0 ∈ ℕ0
109a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
119elexi 3484 . . . . . . 7 0 ∈ V
12 eleq1 2814 . . . . . . . . 9 (𝑛 = 0 → (𝑛 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1312anbi2d 628 . . . . . . . 8 (𝑛 = 0 → ((𝜑𝑛 ∈ ℕ0) ↔ (𝜑 ∧ 0 ∈ ℕ0)))
14 fveq2 6893 . . . . . . . . 9 (𝑛 = 0 → (𝐴𝑛) = (𝐴‘0))
1514eleq1d 2811 . . . . . . . 8 (𝑛 = 0 → ((𝐴𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
1613, 15imbi12d 343 . . . . . . 7 (𝑛 = 0 → (((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℝ) ↔ ((𝜑 ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℝ)))
17 fourierdlem83.f . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
18 fourierdlem83.c . . . . . . . . . 10 𝐶 = (-π(,)π)
19 fourierdlem83.fl1 . . . . . . . . . 10 (𝜑 → (𝐹𝐶) ∈ 𝐿1)
20 fourierdlem83.a . . . . . . . . . 10 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
21 fourierdlem83.b . . . . . . . . . 10 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
2217, 18, 19, 20, 21fourierdlem22 45786 . . . . . . . . 9 (𝜑 → ((𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵𝑛) ∈ ℝ)))
2322simpld 493 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ))
2423imp 405 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℝ)
2511, 16, 24vtocl 3537 . . . . . 6 ((𝜑 ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℝ)
268, 10, 25syl2anc 582 . . . . 5 (𝜑 → (𝐴‘0) ∈ ℝ)
2726rehalfcld 12505 . . . 4 (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28 fzfid 13987 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
29 eleq1 2814 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ0𝑛 ∈ ℕ0))
3029anbi2d 628 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ0) ↔ (𝜑𝑛 ∈ ℕ0)))
31 simpl 481 . . . . . . . . . . . . . . . . . 18 ((𝑘 = 𝑛𝑥𝐶) → 𝑘 = 𝑛)
3231oveq1d 7431 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑛𝑥𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
3332fveq2d 6897 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑛𝑥𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
3433oveq2d 7432 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
3534itgeq2dv 25799 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
3635eleq1d 2811 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
3730, 36imbi12d 343 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
3817adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝐹:ℝ⟶ℝ)
3919adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝐶) ∈ 𝐿1)
40 simpr 483 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
4138, 18, 39, 20, 40fourierdlem16 45780 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (((𝐴𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
4241simprd 494 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
4337, 42chvarvv 1995 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44 pire 26483 . . . . . . . . . . . 12 π ∈ ℝ
4544a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ∈ ℝ)
46 0re 11257 . . . . . . . . . . . . 13 0 ∈ ℝ
47 pipos 26485 . . . . . . . . . . . . 13 0 < π
4846, 47gtneii 11367 . . . . . . . . . . . 12 π ≠ 0
4948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ≠ 0)
5043, 45, 49redivcld 12087 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
5150, 20fmptd 7120 . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℝ)
5251adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴:ℕ0⟶ℝ)
53 elfznn 13578 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
5453nnnn0d 12578 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ0)
5554adantl 480 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ0)
5652, 55ffvelcdmd 7091 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) ∈ ℝ)
5755nn0red 12579 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58 fourierdlem83.x . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
5958adantr 479 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
6057, 59remulcld 11285 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
6160recoscld 16141 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
6256, 61remulcld 11285 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63 eleq1 2814 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
6463anbi2d 628 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ) ↔ (𝜑𝑛 ∈ ℕ)))
65 oveq1 7423 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
6665fveq2d 6897 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
6766oveq2d 7432 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6867adantr 479 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6968itgeq2dv 25799 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
7069eleq1d 2811 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
7164, 70imbi12d 343 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
7217adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
7319adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹𝐶) ∈ 𝐿1)
74 simpr 483 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
7572, 18, 73, 21, 74fourierdlem21 45785 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((𝐵𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
7675simprd 494 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
7771, 76chvarvv 1995 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
7844a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ∈ ℝ)
7948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ≠ 0)
8077, 78, 79redivcld 12087 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
8180, 21fmptd 7120 . . . . . . . . 9 (𝜑𝐵:ℕ⟶ℝ)
8281adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
8353adantl 480 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
8482, 83ffvelcdmd 7091 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) ∈ ℝ)
8560resincld 16140 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
8684, 85remulcld 11285 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
8762, 86readdcld 11284 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8828, 87fsumrecl 15733 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8927, 88readdcld 11284 . . 3 (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
902, 6, 7, 89fvmptd 7008 . 2 (𝜑 → (𝑆𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
9120a1i 11 . . . . . . 7 (𝜑𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92 oveq1 7423 . . . . . . . . . . . . 13 (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
9392fveq2d 6897 . . . . . . . . . . . 12 (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
9493oveq2d 7432 . . . . . . . . . . 11 (𝑛 = 0 → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9594adantr 479 . . . . . . . . . 10 ((𝑛 = 0 ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9695itgeq2dv 25799 . . . . . . . . 9 (𝑛 = 0 → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9796adantl 480 . . . . . . . 8 ((𝜑𝑛 = 0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9897oveq1d 7431 . . . . . . 7 ((𝜑𝑛 = 0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
9917, 18, 19, 20, 10fourierdlem16 45780 . . . . . . . . 9 (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
10099simprd 494 . . . . . . . 8 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
10144a1i 11 . . . . . . . 8 (𝜑 → π ∈ ℝ)
10248a1i 11 . . . . . . . 8 (𝜑 → π ≠ 0)
103100, 101, 102redivcld 12087 . . . . . . 7 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
10491, 98, 10, 103fvmptd 7008 . . . . . 6 (𝜑 → (𝐴‘0) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105 ioosscn 13434 . . . . . . . . . . . . . . 15 (-π(,)π) ⊆ ℂ
106 id 22 . . . . . . . . . . . . . . . 16 (𝑥𝐶𝑥𝐶)
107106, 18eleqtrdi 2836 . . . . . . . . . . . . . . 15 (𝑥𝐶𝑥 ∈ (-π(,)π))
108105, 107sselid 3976 . . . . . . . . . . . . . 14 (𝑥𝐶𝑥 ∈ ℂ)
109108mul02d 11453 . . . . . . . . . . . . 13 (𝑥𝐶 → (0 · 𝑥) = 0)
110109fveq2d 6897 . . . . . . . . . . . 12 (𝑥𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111 cos0 16147 . . . . . . . . . . . 12 (cos‘0) = 1
112110, 111eqtrdi 2782 . . . . . . . . . . 11 (𝑥𝐶 → (cos‘(0 · 𝑥)) = 1)
113112oveq2d 7432 . . . . . . . . . 10 (𝑥𝐶 → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
114113adantl 480 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
11517adantr 479 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝐹:ℝ⟶ℝ)
116 ioossre 13433 . . . . . . . . . . . . . 14 (-π(,)π) ⊆ ℝ
117116, 107sselid 3976 . . . . . . . . . . . . 13 (𝑥𝐶𝑥 ∈ ℝ)
118117adantl 480 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝑥 ∈ ℝ)
119115, 118ffvelcdmd 7091 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
120119recnd 11283 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
121120mulridd 11272 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · 1) = (𝐹𝑥))
122114, 121eqtrd 2766 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = (𝐹𝑥))
123122itgeq2dv 25799 . . . . . . 7 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹𝑥) d𝑥)
124123oveq1d 7431 . . . . . 6 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹𝑥) d𝑥 / π))
125104, 124eqtrd 2766 . . . . 5 (𝜑 → (𝐴‘0) = (∫𝐶(𝐹𝑥) d𝑥 / π))
126125oveq1d 7431 . . . 4 (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2))
12717feqmptd 6963 . . . . . . . . 9 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
128127reseq1d 5980 . . . . . . . 8 (𝜑 → (𝐹𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶))
12944a1i 11 . . . . . . . . . . . 12 (𝑥𝐶 → π ∈ ℝ)
130129renegcld 11682 . . . . . . . . . . 11 (𝑥𝐶 → -π ∈ ℝ)
131 ioossicc 13458 . . . . . . . . . . . . 13 (-π(,)π) ⊆ (-π[,]π)
13218, 131eqsstri 4013 . . . . . . . . . . . 12 𝐶 ⊆ (-π[,]π)
133132sseli 3974 . . . . . . . . . . 11 (𝑥𝐶𝑥 ∈ (-π[,]π))
134 eliccre 45159 . . . . . . . . . . 11 ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135130, 129, 133, 134syl3anc 1368 . . . . . . . . . 10 (𝑥𝐶𝑥 ∈ ℝ)
136135ssriv 3982 . . . . . . . . 9 𝐶 ⊆ ℝ
137 resmpt 6038 . . . . . . . . 9 (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
138136, 137mp1i 13 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
139128, 138eqtr2d 2767 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝐹𝐶))
140139, 19eqeltrd 2826 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
141119, 140itgcl 25801 . . . . 5 (𝜑 → ∫𝐶(𝐹𝑥) d𝑥 ∈ ℂ)
142101recnd 11283 . . . . 5 (𝜑 → π ∈ ℂ)
143 2cnd 12336 . . . . 5 (𝜑 → 2 ∈ ℂ)
144 2ne0 12362 . . . . . 6 2 ≠ 0
145144a1i 11 . . . . 5 (𝜑 → 2 ≠ 0)
146141, 142, 143, 102, 145divdiv32d 12060 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π))
147141, 143, 145divrecd 12038 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)))
148143, 145reccld 12028 . . . . . . 7 (𝜑 → (1 / 2) ∈ ℂ)
149141, 148mulcomd 11276 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥))
150148, 119, 140itgmulc2 25851 . . . . . 6 (𝜑 → ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
151147, 149, 1503eqtrd 2770 . . . . 5 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
152151oveq1d 7431 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
153126, 146, 1523eqtrd 2770 . . 3 (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
15455, 50syldan 589 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
15520fvmpt2 7012 . . . . . . . . . 10 ((𝑛 ∈ ℕ0 ∧ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
15655, 154, 155syl2anc 582 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157156oveq1d 7431 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158154recnd 11283 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
15961recnd 11283 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160158, 159mulcomd 11276 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16155, 43syldan 589 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162161recnd 11283 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163142adantr 479 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
16448a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ≠ 0)
165159, 162, 163, 164divassd 12070 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16617ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝐹:ℝ⟶ℝ)
167117adantl 480 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
168166, 167ffvelcdmd 7091 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
169 nn0re 12527 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
170169ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
171170, 167remulcld 11285 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172171recoscld 16141 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173168, 172remulcld 11285 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
17454, 173sylanl2 679 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175 ioombl 25582 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) ∈ dom vol
17618, 175eqeltri 2822 . . . . . . . . . . . . . . . . . 18 𝐶 ∈ dom vol
177176elexi 3484 . . . . . . . . . . . . . . . . 17 𝐶 ∈ V
178177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ∈ V)
179 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
181178, 172, 168, 179, 180offval2 7702 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
182172recnd 11283 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183120adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
184182, 183mulcomd 11276 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
185184mpteq2dva 5245 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
186181, 185eqtr2d 2767 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
187 coscn 26472 . . . . . . . . . . . . . . . . . 18 cos ∈ (ℂ–cn→ℂ)
188187a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → cos ∈ (ℂ–cn→ℂ))
189 ax-resscn 11206 . . . . . . . . . . . . . . . . . . . . 21 ℝ ⊆ ℂ
190136, 189sstri 3988 . . . . . . . . . . . . . . . . . . . 20 𝐶 ⊆ ℂ
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ⊆ ℂ)
192169recnd 11283 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
193192adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
194 ssid 4001 . . . . . . . . . . . . . . . . . . . 20 ℂ ⊆ ℂ
195194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → ℂ ⊆ ℂ)
196191, 193, 195constcncfg 45529 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
197191, 195idcncfg 45530 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
198196, 197mulcncf 25462 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
199188, 198cncfmpt1f 24922 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
200 cnmbf 25676 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201176, 199, 200sylancr 585 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202140adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
203 1re 11255 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
204 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205169adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑛 ∈ ℝ)
206117adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑥 ∈ ℝ)
207205, 206remulcld 11285 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208207recoscld 16141 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209208ralrimiva 3136 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ0 → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210209adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211 dmmptg 6245 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213204, 212eleqtrd 2828 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦𝐶)
214 eqidd 2727 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215 oveq2 7424 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216215fveq2d 6897 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217216adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦𝐶)
219169adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑛 ∈ ℝ)
220136, 218sselid 3976 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦 ∈ ℝ)
221219, 220remulcld 11285 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222221recoscld 16141 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223214, 217, 218, 222fvmptd 7008 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224223fveq2d 6897 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225 abscosbd 44929 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227224, 226eqbrtrd 5167 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228213, 227syldan 589 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229228ralrimiva 3136 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230 breq2 5149 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231230ralbidv 3168 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232231rspcev 3607 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233203, 229, 232sylancr 585 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234233adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235 bddmulibl 25856 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
236201, 202, 234, 235syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
237186, 236eqeltrd 2826 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
23855, 237syldan 589 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
239159, 174, 238itgmulc2 25851 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240159adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241120adantlr 713 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
24254, 182sylanl2 679 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243240, 241, 242mul12d 11464 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244240, 242mulcomd 11276 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245244oveq2d 7432 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246243, 245eqtrd 2766 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247246itgeq2dv 25799 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248239, 247eqtrd 2766 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249248oveq1d 7431 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250165, 249eqtr3d 2768 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251157, 160, 2503eqtrd 2770 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
25283, 80syldan 589 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
25321fvmpt2 7012 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
25483, 252, 253syl2anc 582 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255254oveq1d 7431 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256252recnd 11283 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
25785recnd 11283 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258256, 257mulcomd 11276 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
25983, 77syldan 589 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260259recnd 11283 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261257, 260, 163, 164divassd 12070 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262119adantlr 713 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
263 nnre 12265 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264263adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
265117adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
266264, 265remulcld 11285 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267266resincld 16140 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268267adantll 712 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269262, 268remulcld 11285 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
27053, 269sylanl2 679 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ V)
272 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
274271, 268, 262, 272, 273offval2 7702 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
275268recnd 11283 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276120adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
277275, 276mulcomd 11276 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
278277mpteq2dva 5245 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
279274, 278eqtr2d 2767 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
280 sincn 26471 . . . . . . . . . . . . . . . . . 18 sin ∈ (ℂ–cn→ℂ)
281280a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283263recnd 11283 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285282, 283, 284constcncfg 45529 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
286282, 284idcncfg 45530 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
287285, 286mulcncf 25462 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
288287adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
289281, 288cncfmpt1f 24922 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
290 cnmbf 25676 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291176, 289, 290sylancr 585 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292140adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
293 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294267ralrimiva 3136 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → ∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295 dmmptg 6245 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
296294, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
297296adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
298293, 297eleqtrd 2828 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦𝐶)
299 eqidd 2727 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300215fveq2d 6897 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301300adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦𝐶)
303263adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
304136, 302sselid 3976 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
305303, 304remulcld 11285 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306305resincld 16140 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307299, 301, 302, 306fvmptd 7008 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308307fveq2d 6897 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309 abssinbd 44946 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310305, 309syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311308, 310eqbrtrd 5167 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312298, 311syldan 589 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313312ralrimiva 3136 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314 breq2 5149 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315314ralbidv 3168 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316315rspcev 3607 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317203, 313, 316sylancr 585 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318317adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319 bddmulibl 25856 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
320291, 292, 318, 319syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
321279, 320eqeltrd 2826 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
32283, 321syldan 589 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
323257, 270, 322itgmulc2 25851 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥)
324257adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
32553, 275sylanl2 679 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
326324, 241, 325mul12d 11464 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327324, 325mulcomd 11276 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328327oveq2d 7432 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329326, 328eqtrd 2766 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330329itgeq2dv 25799 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331323, 330eqtrd 2766 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332331oveq1d 7431 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333261, 332eqtr3d 2768 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334255, 258, 3333eqtrd 2770 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335251, 334oveq12d 7434 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
33654, 168sylanl2 679 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
33755, 208sylan 578 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
33861adantr 479 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339337, 338remulcld 11285 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340336, 339remulcld 11285 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341241, 242, 240mul13d 44930 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
342242, 241mulcomd 11276 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
343342oveq2d 7432 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
344341, 343eqtrd 2766 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
345344mpteq2dva 5245 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))))
346159, 174, 238iblmulc2 25848 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿1)
347345, 346eqeltrd 2826 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿1)
348340, 347itgcl 25801 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
34983, 267sylan 578 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
35085adantr 479 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351349, 350remulcld 11285 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352336, 351remulcld 11285 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353241, 325, 324mul13d 44930 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
354325, 241mulcomd 11276 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
355354oveq2d 7432 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
356353, 355eqtrd 2766 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
357356mpteq2dva 5245 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))))
358257, 270, 322iblmulc2 25848 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿1)
359357, 358eqeltrd 2826 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿1)
360352, 359itgcl 25801 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361348, 360, 163, 164divdird 12073 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
36253nncnd 12274 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363362ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℂ)
364108adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℂ)
36558recnd 11283 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℂ)
366365ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℂ)
367363, 364, 366subdid 11711 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368367fveq2d 6897 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369363, 364mulcld 11275 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370363, 366mulcld 11275 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371 cossub 16166 . . . . . . . . . . . . 13 (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372369, 370, 371syl2anc 582 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373368, 372eqtrd 2766 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374373oveq2d 7432 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375339recnd 11283 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376351recnd 11283 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377241, 375, 376adddid 11279 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378374, 377eqtrd 2766 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379378itgeq2dv 25799 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380340, 347, 352, 359itgadd 25842 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381379, 380eqtr2d 2767 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
382381oveq1d 7431 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
383335, 361, 3823eqtr2d 2772 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
384383sumeq2dv 15702 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
38557adantr 479 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
386117adantl 480 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
38758ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℝ)
388386, 387resubcld 11683 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
389385, 388remulcld 11285 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) ∈ ℝ)
390389recoscld 16141 . . . . . . 7 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
391336, 390remulcld 11285 . . . . . 6 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
392177a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393 eqidd 2727 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
394 eqidd 2727 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
395392, 390, 336, 393, 394offval2 7702 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))))
396390recnd 11283 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
397396, 241mulcomd 11276 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
398397mpteq2dva 5245 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
399395, 398eqtr2d 2767 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) = ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
400187a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → cos ∈ (ℂ–cn→ℂ))
40183, 285syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
40283, 286syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
403190a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐶 ⊆ ℂ)
404365adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
405194a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ℂ ⊆ ℂ)
406403, 404, 405constcncfg 45529 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶𝑋) ∈ (𝐶cn→ℂ))
407402, 406subcncf 25461 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑥𝑋)) ∈ (𝐶cn→ℂ))
408401, 407mulcncf 25462 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑛 · (𝑥𝑋))) ∈ (𝐶cn→ℂ))
409400, 408cncfmpt1f 24922 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ))
410 cnmbf 25676 . . . . . . . . 9 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
411176, 409, 410sylancr 585 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
412140adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
413 simpr 483 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
414390ralrimiva 3136 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
415 dmmptg 6245 . . . . . . . . . . . . . 14 (∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
416414, 415syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
417416adantr 479 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
418413, 417eleqtrd 2828 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦𝐶)
419 eqidd 2727 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
420 oveq1 7423 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑋) = (𝑦𝑋))
421420oveq2d 7432 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑛 · (𝑥𝑋)) = (𝑛 · (𝑦𝑋)))
422421fveq2d 6897 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
423422adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
424 simpr 483 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦𝐶)
42557adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
42655, 220sylan 578 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
42758ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑋 ∈ ℝ)
428426, 427resubcld 11683 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
429425, 428remulcld 11285 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑛 · (𝑦𝑋)) ∈ ℝ)
430429recoscld 16141 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (cos‘(𝑛 · (𝑦𝑋))) ∈ ℝ)
431419, 423, 424, 430fvmptd 7008 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦𝑋))))
432431fveq2d 6897 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦𝑋)))))
433 abscosbd 44929 . . . . . . . . . . . . 13 ((𝑛 · (𝑦𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
434429, 433syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
435432, 434eqbrtrd 5167 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
436418, 435syldan 589 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
437436ralrimiva 3136 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
438 breq2 5149 . . . . . . . . . . 11 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
439438ralbidv 3168 . . . . . . . . . 10 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
440439rspcev 3607 . . . . . . . . 9 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
441203, 437, 440sylancr 585 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
442 bddmulibl 25856 . . . . . . . 8 (((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
443411, 412, 441, 442syl3anc 1368 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
444399, 443eqeltrd 2826 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
445391, 444itgcl 25801 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
44628, 142, 445, 102fsumdivc 15785 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
447176a1i 11 . . . . . . . 8 (𝜑𝐶 ∈ dom vol)
448 anass 467 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)))
449 ancom 459 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶) ↔ (𝑥𝐶𝑛 ∈ (1...𝑁)))
450449anbi2i 621 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
451448, 450bitri 274 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
452451, 391sylbir 234 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
453447, 28, 452, 444itgfsum 25844 . . . . . . 7 (𝜑 → ((𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1 ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
454453simprd 494 . . . . . 6 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
455454eqcomd 2732 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
456455oveq1d 7431 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
457384, 446, 4563eqtr2d 2772 . . 3 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
458153, 457oveq12d 7434 . 2 (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)))
459 fourierdlem83.d . . . . . . . . . . 11 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
4607adantr 479 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝑁 ∈ ℕ)
461 eqid 2726 . . . . . . . . . . 11 (𝐷𝑁) = (𝐷𝑁)
462 eqid 2726 . . . . . . . . . . 11 (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463459, 460, 461, 462dirkertrigeq 45758 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐷𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464 oveq2 7424 . . . . . . . . . . . . . . 15 (𝑠 = (𝑥𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥𝑋)))
465464fveq2d 6897 . . . . . . . . . . . . . 14 (𝑠 = (𝑥𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥𝑋))))
466465sumeq2sdv 15703 . . . . . . . . . . . . 13 (𝑠 = (𝑥𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))
467466oveq2d 7432 . . . . . . . . . . . 12 (𝑠 = (𝑥𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
468467oveq1d 7431 . . . . . . . . . . 11 (𝑠 = (𝑥𝑋) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
469468adantl 480 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑠 = (𝑥𝑋)) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
47058adantr 479 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝑋 ∈ ℝ)
471118, 470resubcld 11683 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
472 halfre 12472 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
473472a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℝ)
474 fzfid 13987 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (1...𝑁) ∈ Fin)
475390an32s 650 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
476474, 475fsumrecl 15733 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
477473, 476readdcld 11284 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
47844a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ∈ ℝ)
47948a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ≠ 0)
480477, 478, 479redivcld 12087 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) ∈ ℝ)
481463, 469, 471, 480fvmptd 7008 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
482481, 480eqeltrd 2826 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
483119, 482remulcld 11285 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) ∈ ℝ)
484177a1i 11 . . . . . . . . . 10 (𝜑𝐶 ∈ V)
485 eqidd 2727 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
486 eqidd 2727 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
487484, 482, 119, 485, 486offval2 7702 . . . . . . . . 9 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
488482recnd 11283 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
489488, 120mulcomd 11276 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥)) = ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))))
490489mpteq2dva 5245 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
491487, 490eqtr2d 2767 . . . . . . . 8 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) = ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
492 eqid 2726 . . . . . . . . . . 11 (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))
493 eqid 2726 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋)))
494194a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℂ ⊆ ℂ)
495 cncfss 24907 . . . . . . . . . . . . . 14 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496189, 494, 495sylancr 585 . . . . . . . . . . . . 13 (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49858adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499497, 498resubcld 11683 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑥𝑋) ∈ ℝ)
500 eqid 2726 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ ↦ (𝑥𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥𝑋))
501499, 500fmptd 7120 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ)
502189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ℝ ⊆ ℂ)
503502, 494idcncfg 45530 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504502, 365, 494constcncfg 45529 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505503, 504subcncf 25461 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ))
506 cncfcdm 24906 . . . . . . . . . . . . . . . 16 ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
507189, 505, 506sylancr 585 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
508501, 507mpbird 256 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ))
509459dirkercncf 45764 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
5107, 509syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
511508, 510cncfcompt 45540 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℝ))
512496, 511sseldd 3979 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℂ))
51344renegcli 11562 . . . . . . . . . . . . . 14 -π ∈ ℝ
514 iccssre 13454 . . . . . . . . . . . . . 14 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515513, 44, 514mp2an 690 . . . . . . . . . . . . 13 (-π[,]π) ⊆ ℝ
516515a1i 11 . . . . . . . . . . . 12 (𝜑 → (-π[,]π) ⊆ ℝ)
517459dirkerf 45754 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (𝐷𝑁):ℝ⟶ℝ)
5187, 517syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁):ℝ⟶ℝ)
519518adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
520516sselda 3978 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
52158adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522520, 521resubcld 11683 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝑥𝑋) ∈ ℝ)
523519, 522ffvelcdmd 7091 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
524523recnd 11283 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
525493, 512, 516, 494, 524cncfmptssg 45528 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526132a1i 11 . . . . . . . . . . 11 (𝜑𝐶 ⊆ (-π[,]π))
527492, 525, 526, 494, 488cncfmptssg 45528 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ))
528 cnmbf 25676 . . . . . . . . . 10 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
529176, 527, 528sylancr 585 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
530513a1i 11 . . . . . . . . . . . . 13 (𝜑 → -π ∈ ℝ)
531 0red 11258 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
532 negpilt0 44931 . . . . . . . . . . . . . . . 16 -π < 0
533532a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → -π < 0)
53447a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 < π)
535530, 531, 101, 533, 534lttrd 11416 . . . . . . . . . . . . . 14 (𝜑 → -π < π)
536530, 101, 535ltled 11403 . . . . . . . . . . . . 13 (𝜑 → -π ≤ π)
537493, 512, 516, 502, 523cncfmptssg 45528 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538530, 101, 536, 537evthiccabs 45150 . . . . . . . . . . . 12 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑤))))
539538simpld 493 . . . . . . . . . . 11 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)))
540 eqidd 2727 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
541420fveq2d 6897 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
542541adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
543 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544518adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
545515, 543sselid 3976 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
54658adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547545, 546resubcld 11683 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑦𝑋) ∈ ℝ)
548544, 547ffvelcdmd 7091 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
549540, 542, 543, 548fvmptd 7008 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
550549fveq2d 6897 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
551550adantlr 713 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
552 eqidd 2727 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
553 oveq1 7423 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → (𝑥𝑋) = (𝑐𝑋))
554553fveq2d 6897 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
555554adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
556 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557518adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
558515, 556sselid 3976 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
55958adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560558, 559resubcld 11683 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑐𝑋) ∈ ℝ)
561557, 560ffvelcdmd 7091 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℝ)
562552, 555, 556, 561fvmptd 7008 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐) = ((𝐷𝑁)‘(𝑐𝑋)))
563562fveq2d 6897 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
564563adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
565551, 564breq12d 5158 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
566565ralbidva 3166 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
567566rexbidva 3167 . . . . . . . . . . 11 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
568539, 567mpbid 231 . . . . . . . . . 10 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
569561recnd 11283 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℂ)
570569abscld 15436 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
5715703adant3 1129 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
572 nfv 1910 . . . . . . . . . . . . . 14 𝑦𝜑
573 nfv 1910 . . . . . . . . . . . . . 14 𝑦 𝑐 ∈ (-π[,]π)
574 nfra1 3272 . . . . . . . . . . . . . 14 𝑦𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))
575572, 573, 574nf3an 1897 . . . . . . . . . . . . 13 𝑦(𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
576 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
577482ralrimiva 3136 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
578 dmmptg 6245 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
579577, 578syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
580579adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
581576, 580eleqtrd 2828 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
5825813ad2antl1 1182 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
583 eqidd 2727 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
584541adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦𝐶) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
585 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → 𝑦𝐶)
586518adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝐷𝑁):ℝ⟶ℝ)
587136, 585sselid 3976 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑦 ∈ ℝ)
58858adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑋 ∈ ℝ)
589587, 588resubcld 11683 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
590586, 589ffvelcdmd 7091 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
591583, 584, 585, 590fvmptd 7008 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝐶) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
592591fveq2d 6897 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
593592adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
594 simplr 767 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
595132sseli 3974 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐶𝑦 ∈ (-π[,]π))
596595adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → 𝑦 ∈ (-π[,]π))
597 rspa 3236 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
598594, 596, 597syl2anc 582 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
599593, 598eqbrtrd 5167 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
6005993adantl2 1164 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
601582, 600syldan 589 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
602601ex 411 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
603575, 602ralrimi 3245 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
604 breq2 5149 . . . . . . . . . . . . . 14 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ((abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
605604ralbidv 3168 . . . . . . . . . . . . 13 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → (∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
606605rspcev 3607 . . . . . . . . . . . 12 (((abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
607571, 603, 606syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
608607rexlimdv3a 3149 . . . . . . . . . 10 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏))
609568, 608mpd 15 . . . . . . . . 9 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
610 bddmulibl 25856 . . . . . . . . 9 (((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
611529, 140, 609, 610syl3anc 1368 . . . . . . . 8 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
612491, 611eqeltrd 2826 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) ∈ 𝐿1)
613142, 483, 612itgmulc2 25851 . . . . . 6 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
614142adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐶) → π ∈ ℂ)
615120, 488, 614mul13d 44930 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
616489oveq2d 7432 . . . . . . . 8 ((𝜑𝑥𝐶) → (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
617615, 616eqtrd 2766 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
618617itgeq2dv 25799 . . . . . 6 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
619613, 618eqtr4d 2769 . . . . 5 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥)
620148adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℂ)
621620, 120mulcomd 11276 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) = ((𝐹𝑥) · (1 / 2)))
622396an32s 650 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
623474, 120, 622fsummulc2 15783 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
624623eqcomd 2732 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
625621, 624oveq12d 7434 . . . . . . 7 ((𝜑𝑥𝐶) → (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
626474, 622fsumcl 15732 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
627120, 620, 626adddid 11279 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
628481oveq1d 7431 . . . . . . . . 9 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π))
629620, 626addcld 11274 . . . . . . . . . 10 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℂ)
630629, 614, 479divcan1d 12036 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
631628, 630eqtr2d 2767 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = (((𝐷𝑁)‘(𝑥𝑋)) · π))
632631oveq2d 7432 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)))
633625, 627, 6323eqtr2rd 2773 . . . . . 6 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
634633itgeq2dv 25799 . . . . 5 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥)
635 remulcl 11234 . . . . . . 7 (((1 / 2) ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
636472, 119, 635sylancr 585 . . . . . 6 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
637148, 119, 140iblmulc2 25848 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ ((1 / 2) · (𝐹𝑥))) ∈ 𝐿1)
638391an32s 650 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
639474, 638fsumrecl 15733 . . . . . 6 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
640453simpld 493 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
641636, 637, 639, 640itgadd 25842 . . . . 5 (𝜑 → ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
642619, 634, 6413eqtrrd 2771 . . . 4 (𝜑 → (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) = (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥))
643642oveq1d 7431 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π))
644636, 637itgcl 25801 . . . 4 (𝜑 → ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 ∈ ℂ)
645639, 640itgcl 25801 . . . 4 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
646644, 645, 142, 102divdird 12073 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)))
647483, 612itgcl 25801 . . . 4 (𝜑 → ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥 ∈ ℂ)
648647, 142, 102divcan3d 12040 . . 3 (𝜑 → ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
649643, 646, 6483eqtr3d 2774 . 2 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
65090, 458, 6493eqtrd 2770 1 (𝜑 → (𝑆𝑁) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wral 3051  wrex 3060  Vcvv 3462  wss 3946  ifcif 4523   class class class wbr 5145  cmpt 5228  dom cdm 5674  cres 5676  wf 6542  cfv 6546  (class class class)co 7416  f cof 7680  cc 11147  cr 11148  0cc0 11149  1c1 11150   + caddc 11152   · cmul 11154   < clt 11289  cle 11290  cmin 11485  -cneg 11486   / cdiv 11912  cn 12258  2c2 12313  0cn0 12518  (,)cioo 13372  [,]cicc 13375  ...cfz 13532   mod cmo 13883  abscabs 15234  Σcsu 15685  sincsin 16060  cosccos 16061  πcpi 16063  cnccncf 24884  volcvol 25480  MblFncmbf 25631  𝐿1cibl 25634  citg 25635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cc 10469  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-disj 5111  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-ofr 7683  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-oadd 8492  df-omul 8493  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-dju 9937  df-card 9975  df-acn 9978  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-z 12605  df-dec 12724  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13140  df-xadd 13141  df-xmul 13142  df-ioo 13376  df-ioc 13377  df-ico 13378  df-icc 13379  df-fz 13533  df-fzo 13676  df-fl 13806  df-mod 13884  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-sum 15686  df-ef 16064  df-sin 16066  df-cos 16067  df-pi 16069  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19058  df-cntz 19307  df-cmn 19776  df-psmet 21331  df-xmet 21332  df-met 21333  df-bl 21334  df-mopn 21335  df-fbas 21336  df-fg 21337  df-cnfld 21340  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22937  df-cld 23011  df-ntr 23012  df-cls 23013  df-nei 23090  df-lp 23128  df-perf 23129  df-cn 23219  df-cnp 23220  df-t1 23306  df-haus 23307  df-cmp 23379  df-tx 23554  df-hmeo 23747  df-fil 23838  df-fm 23930  df-flim 23931  df-flf 23932  df-xms 24314  df-ms 24315  df-tms 24316  df-cncf 24886  df-ovol 25481  df-vol 25482  df-mbf 25636  df-itg1 25637  df-itg2 25638  df-ibl 25639  df-itg 25640  df-0p 25687  df-limc 25883  df-dv 25884
This theorem is referenced by:  fourierdlem111  45874
  Copyright terms: Public domain W3C validator