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 42359
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 7158 . . . . . 6 (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
43sumeq1d 15053 . . . . 5 (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
54oveq2d 7166 . . . 4 (𝑚 = 𝑁 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
65adantl 482 . . 3 ((𝜑𝑚 = 𝑁) → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
7 fourierdlem83.n . . 3 (𝜑𝑁 ∈ ℕ)
8 id 22 . . . . . 6 (𝜑𝜑)
9 0nn0 11906 . . . . . . 7 0 ∈ ℕ0
109a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
119elexi 3519 . . . . . . 7 0 ∈ V
12 eleq1 2905 . . . . . . . . 9 (𝑛 = 0 → (𝑛 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1312anbi2d 628 . . . . . . . 8 (𝑛 = 0 → ((𝜑𝑛 ∈ ℕ0) ↔ (𝜑 ∧ 0 ∈ ℕ0)))
14 fveq2 6669 . . . . . . . . 9 (𝑛 = 0 → (𝐴𝑛) = (𝐴‘0))
1514eleq1d 2902 . . . . . . . 8 (𝑛 = 0 → ((𝐴𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
1613, 15imbi12d 346 . . . . . . 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 42299 . . . . . . . . 9 (𝜑 → ((𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵𝑛) ∈ ℝ)))
2322simpld 495 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ))
2423imp 407 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℝ)
2511, 16, 24vtocl 3565 . . . . . 6 ((𝜑 ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℝ)
268, 10, 25syl2anc 584 . . . . 5 (𝜑 → (𝐴‘0) ∈ ℝ)
2726rehalfcld 11878 . . . 4 (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28 fzfid 13336 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
29 eleq1 2905 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ0𝑛 ∈ ℕ0))
3029anbi2d 628 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ0) ↔ (𝜑𝑛 ∈ ℕ0)))
31 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑘 = 𝑛𝑥𝐶) → 𝑘 = 𝑛)
3231oveq1d 7165 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑛𝑥𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
3332fveq2d 6673 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑛𝑥𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
3433oveq2d 7166 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
3534itgeq2dv 24316 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
3635eleq1d 2902 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
3730, 36imbi12d 346 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
3817adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝐹:ℝ⟶ℝ)
3919adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝐶) ∈ 𝐿1)
40 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
4138, 18, 39, 20, 40fourierdlem16 42293 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (((𝐴𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
4241simprd 496 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
4337, 42chvarv 2410 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44 pire 24978 . . . . . . . . . . . 12 π ∈ ℝ
4544a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ∈ ℝ)
46 0re 10637 . . . . . . . . . . . . 13 0 ∈ ℝ
47 pipos 24980 . . . . . . . . . . . . 13 0 < π
4846, 47gtneii 10746 . . . . . . . . . . . 12 π ≠ 0
4948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ≠ 0)
5043, 45, 49redivcld 11462 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
5150, 20fmptd 6876 . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℝ)
5251adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴:ℕ0⟶ℝ)
53 elfznn 12931 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
5453nnnn0d 11949 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ0)
5554adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ0)
5652, 55ffvelrnd 6850 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) ∈ ℝ)
5755nn0red 11950 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58 fourierdlem83.x . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
5958adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
6057, 59remulcld 10665 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
6160recoscld 15492 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
6256, 61remulcld 10665 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63 eleq1 2905 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
6463anbi2d 628 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ) ↔ (𝜑𝑛 ∈ ℕ)))
65 oveq1 7157 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
6665fveq2d 6673 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
6766oveq2d 7166 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6867adantr 481 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6968itgeq2dv 24316 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
7069eleq1d 2902 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
7164, 70imbi12d 346 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
7217adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
7319adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹𝐶) ∈ 𝐿1)
74 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
7572, 18, 73, 21, 74fourierdlem21 42298 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((𝐵𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
7675simprd 496 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
7771, 76chvarv 2410 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
7844a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ∈ ℝ)
7948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ≠ 0)
8077, 78, 79redivcld 11462 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
8180, 21fmptd 6876 . . . . . . . . 9 (𝜑𝐵:ℕ⟶ℝ)
8281adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
8353adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
8482, 83ffvelrnd 6850 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) ∈ ℝ)
8560resincld 15491 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
8684, 85remulcld 10665 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
8762, 86readdcld 10664 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8828, 87fsumrecl 15086 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8927, 88readdcld 10664 . . 3 (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
902, 6, 7, 89fvmptd 6773 . 2 (𝜑 → (𝑆𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
9120a1i 11 . . . . . . 7 (𝜑𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92 oveq1 7157 . . . . . . . . . . . . 13 (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
9392fveq2d 6673 . . . . . . . . . . . 12 (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
9493oveq2d 7166 . . . . . . . . . . 11 (𝑛 = 0 → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9594adantr 481 . . . . . . . . . 10 ((𝑛 = 0 ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9695itgeq2dv 24316 . . . . . . . . 9 (𝑛 = 0 → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9796adantl 482 . . . . . . . 8 ((𝜑𝑛 = 0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9897oveq1d 7165 . . . . . . 7 ((𝜑𝑛 = 0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
9917, 18, 19, 20, 10fourierdlem16 42293 . . . . . . . . 9 (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
10099simprd 496 . . . . . . . 8 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
10144a1i 11 . . . . . . . 8 (𝜑 → π ∈ ℝ)
10248a1i 11 . . . . . . . 8 (𝜑 → π ≠ 0)
103100, 101, 102redivcld 11462 . . . . . . 7 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
10491, 98, 10, 103fvmptd 6773 . . . . . 6 (𝜑 → (𝐴‘0) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105 ioosscn 41653 . . . . . . . . . . . . . . 15 (-π(,)π) ⊆ ℂ
106 id 22 . . . . . . . . . . . . . . . 16 (𝑥𝐶𝑥𝐶)
107106, 18syl6eleq 2928 . . . . . . . . . . . . . . 15 (𝑥𝐶𝑥 ∈ (-π(,)π))
108105, 107sseldi 3969 . . . . . . . . . . . . . 14 (𝑥𝐶𝑥 ∈ ℂ)
109108mul02d 10832 . . . . . . . . . . . . 13 (𝑥𝐶 → (0 · 𝑥) = 0)
110109fveq2d 6673 . . . . . . . . . . . 12 (𝑥𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111 cos0 15498 . . . . . . . . . . . 12 (cos‘0) = 1
112110, 111syl6eq 2877 . . . . . . . . . . 11 (𝑥𝐶 → (cos‘(0 · 𝑥)) = 1)
113112oveq2d 7166 . . . . . . . . . 10 (𝑥𝐶 → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
114113adantl 482 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
11517adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝐹:ℝ⟶ℝ)
116 ioossre 12793 . . . . . . . . . . . . . 14 (-π(,)π) ⊆ ℝ
117116, 107sseldi 3969 . . . . . . . . . . . . 13 (𝑥𝐶𝑥 ∈ ℝ)
118117adantl 482 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝑥 ∈ ℝ)
119115, 118ffvelrnd 6850 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
120119recnd 10663 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
121120mulid1d 10652 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · 1) = (𝐹𝑥))
122114, 121eqtrd 2861 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = (𝐹𝑥))
123122itgeq2dv 24316 . . . . . . 7 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹𝑥) d𝑥)
124123oveq1d 7165 . . . . . 6 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹𝑥) d𝑥 / π))
125104, 124eqtrd 2861 . . . . 5 (𝜑 → (𝐴‘0) = (∫𝐶(𝐹𝑥) d𝑥 / π))
126125oveq1d 7165 . . . 4 (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2))
12717feqmptd 6732 . . . . . . . . 9 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
128127reseq1d 5851 . . . . . . . 8 (𝜑 → (𝐹𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶))
12944a1i 11 . . . . . . . . . . . 12 (𝑥𝐶 → π ∈ ℝ)
130129renegcld 11061 . . . . . . . . . . 11 (𝑥𝐶 → -π ∈ ℝ)
131 ioossicc 12817 . . . . . . . . . . . . 13 (-π(,)π) ⊆ (-π[,]π)
13218, 131eqsstri 4005 . . . . . . . . . . . 12 𝐶 ⊆ (-π[,]π)
133132sseli 3967 . . . . . . . . . . 11 (𝑥𝐶𝑥 ∈ (-π[,]π))
134 eliccre 41665 . . . . . . . . . . 11 ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135130, 129, 133, 134syl3anc 1365 . . . . . . . . . 10 (𝑥𝐶𝑥 ∈ ℝ)
136135ssriv 3975 . . . . . . . . 9 𝐶 ⊆ ℝ
137 resmpt 5904 . . . . . . . . 9 (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
138136, 137mp1i 13 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
139128, 138eqtr2d 2862 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝐹𝐶))
140139, 19eqeltrd 2918 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
141119, 140itgcl 24318 . . . . 5 (𝜑 → ∫𝐶(𝐹𝑥) d𝑥 ∈ ℂ)
142101recnd 10663 . . . . 5 (𝜑 → π ∈ ℂ)
143 2cnd 11709 . . . . 5 (𝜑 → 2 ∈ ℂ)
144 2ne0 11735 . . . . . 6 2 ≠ 0
145144a1i 11 . . . . 5 (𝜑 → 2 ≠ 0)
146141, 142, 143, 102, 145divdiv32d 11435 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π))
147141, 143, 145divrecd 11413 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)))
148143, 145reccld 11403 . . . . . . 7 (𝜑 → (1 / 2) ∈ ℂ)
149141, 148mulcomd 10656 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥))
150148, 119, 140itgmulc2 24368 . . . . . 6 (𝜑 → ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
151147, 149, 1503eqtrd 2865 . . . . 5 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
152151oveq1d 7165 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
153126, 146, 1523eqtrd 2865 . . 3 (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
15455, 50syldan 591 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
15520fvmpt2 6777 . . . . . . . . . 10 ((𝑛 ∈ ℕ0 ∧ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
15655, 154, 155syl2anc 584 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157156oveq1d 7165 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158154recnd 10663 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
15961recnd 10663 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160158, 159mulcomd 10656 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16155, 43syldan 591 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162161recnd 10663 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163142adantr 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
16448a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ≠ 0)
165159, 162, 163, 164divassd 11445 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16617ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝐹:ℝ⟶ℝ)
167117adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
168166, 167ffvelrnd 6850 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
169 nn0re 11900 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
170169ad2antlr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
171170, 167remulcld 10665 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172171recoscld 15492 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173168, 172remulcld 10665 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
17454, 173sylanl2 677 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175 ioombl 24100 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) ∈ dom vol
17618, 175eqeltri 2914 . . . . . . . . . . . . . . . . . 18 𝐶 ∈ dom vol
177176elexi 3519 . . . . . . . . . . . . . . . . 17 𝐶 ∈ V
178177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ∈ V)
179 eqidd 2827 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180 eqidd 2827 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
181178, 172, 168, 179, 180offval2 7420 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
182172recnd 10663 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183120adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
184182, 183mulcomd 10656 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
185184mpteq2dva 5158 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
186181, 185eqtr2d 2862 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
187 coscn 24967 . . . . . . . . . . . . . . . . . 18 cos ∈ (ℂ–cn→ℂ)
188187a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → cos ∈ (ℂ–cn→ℂ))
189 ax-resscn 10588 . . . . . . . . . . . . . . . . . . . . 21 ℝ ⊆ ℂ
190136, 189sstri 3980 . . . . . . . . . . . . . . . . . . . 20 𝐶 ⊆ ℂ
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ⊆ ℂ)
192169recnd 10663 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
193192adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
194 ssid 3993 . . . . . . . . . . . . . . . . . . . 20 ℂ ⊆ ℂ
195194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → ℂ ⊆ ℂ)
196191, 193, 195constcncfg 42038 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
197191, 195idcncfg 42039 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
198196, 197mulcncf 23981 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
199188, 198cncfmpt1f 23455 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
200 cnmbf 24194 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201176, 199, 200sylancr 587 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202140adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
203 1re 10635 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
204 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205169adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑛 ∈ ℝ)
206117adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑥 ∈ ℝ)
207205, 206remulcld 10665 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208207recoscld 15492 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209208ralrimiva 3187 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ0 → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210209adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211 dmmptg 6095 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213204, 212eleqtrd 2920 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦𝐶)
214 eqidd 2827 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215 oveq2 7158 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216215fveq2d 6673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217216adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦𝐶)
219169adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑛 ∈ ℝ)
220136, 218sseldi 3969 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦 ∈ ℝ)
221219, 220remulcld 10665 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222221recoscld 15492 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223214, 217, 218, 222fvmptd 6773 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224223fveq2d 6673 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225 abscosbd 41428 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227224, 226eqbrtrd 5085 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228213, 227syldan 591 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229228ralrimiva 3187 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230 breq2 5067 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231230ralbidv 3202 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232231rspcev 3627 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233203, 229, 232sylancr 587 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234233adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235 bddmulibl 24373 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
236201, 202, 234, 235syl3anc 1365 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
237186, 236eqeltrd 2918 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
23855, 237syldan 591 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
239159, 174, 238itgmulc2 24368 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240159adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241120adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
24254, 182sylanl2 677 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243240, 241, 242mul12d 10843 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244240, 242mulcomd 10656 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245244oveq2d 7166 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246243, 245eqtrd 2861 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247246itgeq2dv 24316 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248239, 247eqtrd 2861 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249248oveq1d 7165 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250165, 249eqtr3d 2863 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251157, 160, 2503eqtrd 2865 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
25283, 80syldan 591 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
25321fvmpt2 6777 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
25483, 252, 253syl2anc 584 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255254oveq1d 7165 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256252recnd 10663 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
25785recnd 10663 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258256, 257mulcomd 10656 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
25983, 77syldan 591 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260259recnd 10663 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261257, 260, 163, 164divassd 11445 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262119adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
263 nnre 11639 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264263adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
265117adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
266264, 265remulcld 10665 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267266resincld 15491 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268267adantll 710 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269262, 268remulcld 10665 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
27053, 269sylanl2 677 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ V)
272 eqidd 2827 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273 eqidd 2827 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
274271, 268, 262, 272, 273offval2 7420 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
275268recnd 10663 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276120adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
277275, 276mulcomd 10656 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
278277mpteq2dva 5158 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
279274, 278eqtr2d 2862 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
280 sincn 24966 . . . . . . . . . . . . . . . . . 18 sin ∈ (ℂ–cn→ℂ)
281280a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283263recnd 10663 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285282, 283, 284constcncfg 42038 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
286282, 284idcncfg 42039 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
287285, 286mulcncf 23981 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
288287adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
289281, 288cncfmpt1f 23455 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
290 cnmbf 24194 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291176, 289, 290sylancr 587 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292140adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
293 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294267ralrimiva 3187 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → ∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295 dmmptg 6095 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
296294, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
297296adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
298293, 297eleqtrd 2920 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦𝐶)
299 eqidd 2827 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300215fveq2d 6673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301300adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦𝐶)
303263adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
304136, 302sseldi 3969 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
305303, 304remulcld 10665 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306305resincld 15491 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307299, 301, 302, 306fvmptd 6773 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308307fveq2d 6673 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309 abssinbd 41446 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310305, 309syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311308, 310eqbrtrd 5085 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312298, 311syldan 591 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313312ralrimiva 3187 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314 breq2 5067 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315314ralbidv 3202 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316315rspcev 3627 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317203, 313, 316sylancr 587 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318317adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319 bddmulibl 24373 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
320291, 292, 318, 319syl3anc 1365 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
321279, 320eqeltrd 2918 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
32283, 321syldan 591 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
323257, 270, 322itgmulc2 24368 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥)
324257adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
32553, 275sylanl2 677 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
326324, 241, 325mul12d 10843 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327324, 325mulcomd 10656 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328327oveq2d 7166 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329326, 328eqtrd 2861 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330329itgeq2dv 24316 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331323, 330eqtrd 2861 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332331oveq1d 7165 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333261, 332eqtr3d 2863 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334255, 258, 3333eqtrd 2865 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335251, 334oveq12d 7168 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
33654, 168sylanl2 677 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
33755, 208sylan 580 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
33861adantr 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339337, 338remulcld 10665 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340336, 339remulcld 10665 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341241, 242, 240mul13d 41429 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
342242, 241mulcomd 10656 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
343342oveq2d 7166 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
344341, 343eqtrd 2861 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
345344mpteq2dva 5158 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))))
346159, 174, 238iblmulc2 24365 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿1)
347345, 346eqeltrd 2918 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿1)
348340, 347itgcl 24318 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
34983, 267sylan 580 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
35085adantr 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351349, 350remulcld 10665 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352336, 351remulcld 10665 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353241, 325, 324mul13d 41429 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
354325, 241mulcomd 10656 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
355354oveq2d 7166 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
356353, 355eqtrd 2861 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
357356mpteq2dva 5158 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))))
358257, 270, 322iblmulc2 24365 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿1)
359357, 358eqeltrd 2918 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿1)
360352, 359itgcl 24318 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361348, 360, 163, 164divdird 11448 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
36253nncnd 11648 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363362ad2antlr 723 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℂ)
364108adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℂ)
36558recnd 10663 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℂ)
366365ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℂ)
367363, 364, 366subdid 11090 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368367fveq2d 6673 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369363, 364mulcld 10655 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370363, 366mulcld 10655 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371 cossub 15517 . . . . . . . . . . . . 13 (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372369, 370, 371syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373368, 372eqtrd 2861 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374373oveq2d 7166 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375339recnd 10663 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376351recnd 10663 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377241, 375, 376adddid 10659 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378374, 377eqtrd 2861 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379378itgeq2dv 24316 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380340, 347, 352, 359itgadd 24359 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381379, 380eqtr2d 2862 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
382381oveq1d 7165 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
383335, 361, 3823eqtr2d 2867 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
384383sumeq2dv 15055 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
38557adantr 481 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
386117adantl 482 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
38758ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℝ)
388386, 387resubcld 11062 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
389385, 388remulcld 10665 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) ∈ ℝ)
390389recoscld 15492 . . . . . . 7 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
391336, 390remulcld 10665 . . . . . 6 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
392177a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393 eqidd 2827 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
394 eqidd 2827 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
395392, 390, 336, 393, 394offval2 7420 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))))
396390recnd 10663 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
397396, 241mulcomd 10656 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
398397mpteq2dva 5158 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
399395, 398eqtr2d 2862 . . . . . . 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 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
405194a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ℂ ⊆ ℂ)
406403, 404, 405constcncfg 42038 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶𝑋) ∈ (𝐶cn→ℂ))
407402, 406subcncf 42036 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑥𝑋)) ∈ (𝐶cn→ℂ))
408401, 407mulcncf 23981 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑛 · (𝑥𝑋))) ∈ (𝐶cn→ℂ))
409400, 408cncfmpt1f 23455 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ))
410 cnmbf 24194 . . . . . . . . 9 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
411176, 409, 410sylancr 587 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
412140adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
413 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
414390ralrimiva 3187 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
415 dmmptg 6095 . . . . . . . . . . . . . 14 (∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
416414, 415syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
417416adantr 481 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
418413, 417eleqtrd 2920 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦𝐶)
419 eqidd 2827 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
420 oveq1 7157 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑋) = (𝑦𝑋))
421420oveq2d 7166 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑛 · (𝑥𝑋)) = (𝑛 · (𝑦𝑋)))
422421fveq2d 6673 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
423422adantl 482 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
424 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦𝐶)
42557adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
42655, 220sylan 580 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
42758ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑋 ∈ ℝ)
428426, 427resubcld 11062 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
429425, 428remulcld 10665 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑛 · (𝑦𝑋)) ∈ ℝ)
430429recoscld 15492 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (cos‘(𝑛 · (𝑦𝑋))) ∈ ℝ)
431419, 423, 424, 430fvmptd 6773 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦𝑋))))
432431fveq2d 6673 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦𝑋)))))
433 abscosbd 41428 . . . . . . . . . . . . 13 ((𝑛 · (𝑦𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
434429, 433syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
435432, 434eqbrtrd 5085 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
436418, 435syldan 591 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
437436ralrimiva 3187 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
438 breq2 5067 . . . . . . . . . . 11 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
439438ralbidv 3202 . . . . . . . . . 10 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
440439rspcev 3627 . . . . . . . . 9 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
441203, 437, 440sylancr 587 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
442 bddmulibl 24373 . . . . . . . 8 (((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
443411, 412, 441, 442syl3anc 1365 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
444399, 443eqeltrd 2918 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
445391, 444itgcl 24318 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
44628, 142, 445, 102fsumdivc 15136 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
447176a1i 11 . . . . . . . 8 (𝜑𝐶 ∈ dom vol)
448 anass 469 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)))
449 ancom 461 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶) ↔ (𝑥𝐶𝑛 ∈ (1...𝑁)))
450449anbi2i 622 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
451448, 450bitri 276 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
452451, 391sylbir 236 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
453447, 28, 452, 444itgfsum 24361 . . . . . . 7 (𝜑 → ((𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1 ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
454453simprd 496 . . . . . 6 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
455454eqcomd 2832 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
456455oveq1d 7165 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
457384, 446, 4563eqtr2d 2867 . . 3 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
458153, 457oveq12d 7168 . 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 481 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝑁 ∈ ℕ)
461 eqid 2826 . . . . . . . . . . 11 (𝐷𝑁) = (𝐷𝑁)
462 eqid 2826 . . . . . . . . . . 11 (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463459, 460, 461, 462dirkertrigeq 42271 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐷𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464 oveq2 7158 . . . . . . . . . . . . . . 15 (𝑠 = (𝑥𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥𝑋)))
465464fveq2d 6673 . . . . . . . . . . . . . 14 (𝑠 = (𝑥𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥𝑋))))
466465sumeq2sdv 15056 . . . . . . . . . . . . 13 (𝑠 = (𝑥𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))
467466oveq2d 7166 . . . . . . . . . . . 12 (𝑠 = (𝑥𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
468467oveq1d 7165 . . . . . . . . . . 11 (𝑠 = (𝑥𝑋) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
469468adantl 482 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑠 = (𝑥𝑋)) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
47058adantr 481 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝑋 ∈ ℝ)
471118, 470resubcld 11062 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
472 halfre 11845 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
473472a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℝ)
474 fzfid 13336 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (1...𝑁) ∈ Fin)
475390an32s 648 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
476474, 475fsumrecl 15086 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
477473, 476readdcld 10664 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
47844a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ∈ ℝ)
47948a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ≠ 0)
480477, 478, 479redivcld 11462 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) ∈ ℝ)
481463, 469, 471, 480fvmptd 6773 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
482481, 480eqeltrd 2918 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
483119, 482remulcld 10665 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) ∈ ℝ)
484177a1i 11 . . . . . . . . . 10 (𝜑𝐶 ∈ V)
485 eqidd 2827 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
486 eqidd 2827 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
487484, 482, 119, 485, 486offval2 7420 . . . . . . . . 9 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
488482recnd 10663 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
489488, 120mulcomd 10656 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥)) = ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))))
490489mpteq2dva 5158 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
491487, 490eqtr2d 2862 . . . . . . . 8 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) = ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
492 eqid 2826 . . . . . . . . . . 11 (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))
493 eqid 2826 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋)))
494194a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℂ ⊆ ℂ)
495 cncfss 23441 . . . . . . . . . . . . . 14 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496189, 494, 495sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49858adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499497, 498resubcld 11062 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑥𝑋) ∈ ℝ)
500 eqid 2826 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ ↦ (𝑥𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥𝑋))
501499, 500fmptd 6876 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ)
502189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ℝ ⊆ ℂ)
503502, 494idcncfg 42039 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504502, 365, 494constcncfg 42038 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505503, 504subcncf 42036 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ))
506 cncffvrn 23440 . . . . . . . . . . . . . . . 16 ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
507189, 505, 506sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
508501, 507mpbird 258 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ))
509459dirkercncf 42277 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
5107, 509syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
511508, 510cncfcompt 42050 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℝ))
512496, 511sseldd 3972 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℂ))
51344renegcli 10941 . . . . . . . . . . . . . 14 -π ∈ ℝ
514 iccssre 12813 . . . . . . . . . . . . . 14 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515513, 44, 514mp2an 688 . . . . . . . . . . . . 13 (-π[,]π) ⊆ ℝ
516515a1i 11 . . . . . . . . . . . 12 (𝜑 → (-π[,]π) ⊆ ℝ)
517459dirkerf 42267 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (𝐷𝑁):ℝ⟶ℝ)
5187, 517syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁):ℝ⟶ℝ)
519518adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
520516sselda 3971 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
52158adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522520, 521resubcld 11062 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝑥𝑋) ∈ ℝ)
523519, 522ffvelrnd 6850 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
524523recnd 10663 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
525493, 512, 516, 494, 524cncfmptssg 42037 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526132a1i 11 . . . . . . . . . . 11 (𝜑𝐶 ⊆ (-π[,]π))
527492, 525, 526, 494, 488cncfmptssg 42037 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ))
528 cnmbf 24194 . . . . . . . . . 10 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
529176, 527, 528sylancr 587 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
530513a1i 11 . . . . . . . . . . . . 13 (𝜑 → -π ∈ ℝ)
531 0red 10638 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
532 negpilt0 41430 . . . . . . . . . . . . . . . 16 -π < 0
533532a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → -π < 0)
53447a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 < π)
535530, 531, 101, 533, 534lttrd 10795 . . . . . . . . . . . . . 14 (𝜑 → -π < π)
536530, 101, 535ltled 10782 . . . . . . . . . . . . 13 (𝜑 → -π ≤ π)
537493, 512, 516, 502, 523cncfmptssg 42037 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538530, 101, 536, 537evthiccabs 41655 . . . . . . . . . . . 12 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑤))))
539538simpld 495 . . . . . . . . . . 11 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)))
540 eqidd 2827 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
541420fveq2d 6673 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
542541adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
543 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544518adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
545515, 543sseldi 3969 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
54658adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547545, 546resubcld 11062 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑦𝑋) ∈ ℝ)
548544, 547ffvelrnd 6850 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
549540, 542, 543, 548fvmptd 6773 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
550549fveq2d 6673 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
551550adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
552 eqidd 2827 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
553 oveq1 7157 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → (𝑥𝑋) = (𝑐𝑋))
554553fveq2d 6673 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
555554adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
556 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557518adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
558515, 556sseldi 3969 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
55958adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560558, 559resubcld 11062 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑐𝑋) ∈ ℝ)
561557, 560ffvelrnd 6850 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℝ)
562552, 555, 556, 561fvmptd 6773 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐) = ((𝐷𝑁)‘(𝑐𝑋)))
563562fveq2d 6673 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
564563adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
565551, 564breq12d 5076 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
566565ralbidva 3201 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
567566rexbidva 3301 . . . . . . . . . . 11 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
568539, 567mpbid 233 . . . . . . . . . 10 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
569561recnd 10663 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℂ)
570569abscld 14791 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
5715703adant3 1126 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
572 nfv 1908 . . . . . . . . . . . . . 14 𝑦𝜑
573 nfv 1908 . . . . . . . . . . . . . 14 𝑦 𝑐 ∈ (-π[,]π)
574 nfra1 3224 . . . . . . . . . . . . . 14 𝑦𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))
575572, 573, 574nf3an 1895 . . . . . . . . . . . . 13 𝑦(𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
576 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
577482ralrimiva 3187 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
578 dmmptg 6095 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
579577, 578syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
580579adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
581576, 580eleqtrd 2920 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
5825813ad2antl1 1179 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
583 eqidd 2827 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
584541adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦𝐶) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
585 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → 𝑦𝐶)
586518adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝐷𝑁):ℝ⟶ℝ)
587136, 585sseldi 3969 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑦 ∈ ℝ)
58858adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑋 ∈ ℝ)
589587, 588resubcld 11062 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
590586, 589ffvelrnd 6850 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
591583, 584, 585, 590fvmptd 6773 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝐶) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
592591fveq2d 6673 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
593592adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
594 simplr 765 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
595132sseli 3967 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐶𝑦 ∈ (-π[,]π))
596595adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → 𝑦 ∈ (-π[,]π))
597 rspa 3211 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
598594, 596, 597syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
599593, 598eqbrtrd 5085 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
6005993adantl2 1161 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
601582, 600syldan 591 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
602601ex 413 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
603575, 602ralrimi 3221 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
604 breq2 5067 . . . . . . . . . . . . . 14 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ((abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
605604ralbidv 3202 . . . . . . . . . . . . 13 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → (∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
606605rspcev 3627 . . . . . . . . . . . 12 (((abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
607571, 603, 606syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
608607rexlimdv3a 3291 . . . . . . . . . 10 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏))
609568, 608mpd 15 . . . . . . . . 9 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
610 bddmulibl 24373 . . . . . . . . 9 (((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
611529, 140, 609, 610syl3anc 1365 . . . . . . . 8 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
612491, 611eqeltrd 2918 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) ∈ 𝐿1)
613142, 483, 612itgmulc2 24368 . . . . . 6 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
614142adantr 481 . . . . . . . . 9 ((𝜑𝑥𝐶) → π ∈ ℂ)
615120, 488, 614mul13d 41429 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
616489oveq2d 7166 . . . . . . . 8 ((𝜑𝑥𝐶) → (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
617615, 616eqtrd 2861 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
618617itgeq2dv 24316 . . . . . 6 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
619613, 618eqtr4d 2864 . . . . 5 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥)
620148adantr 481 . . . . . . . . 9 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℂ)
621620, 120mulcomd 10656 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) = ((𝐹𝑥) · (1 / 2)))
622396an32s 648 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
623474, 120, 622fsummulc2 15134 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
624623eqcomd 2832 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
625621, 624oveq12d 7168 . . . . . . 7 ((𝜑𝑥𝐶) → (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
626474, 622fsumcl 15085 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
627120, 620, 626adddid 10659 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
628481oveq1d 7165 . . . . . . . . 9 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π))
629620, 626addcld 10654 . . . . . . . . . 10 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℂ)
630629, 614, 479divcan1d 11411 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
631628, 630eqtr2d 2862 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = (((𝐷𝑁)‘(𝑥𝑋)) · π))
632631oveq2d 7166 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)))
633625, 627, 6323eqtr2rd 2868 . . . . . 6 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
634633itgeq2dv 24316 . . . . 5 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥)
635 remulcl 10616 . . . . . . 7 (((1 / 2) ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
636472, 119, 635sylancr 587 . . . . . 6 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
637148, 119, 140iblmulc2 24365 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ ((1 / 2) · (𝐹𝑥))) ∈ 𝐿1)
638391an32s 648 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
639474, 638fsumrecl 15086 . . . . . 6 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
640453simpld 495 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
641636, 637, 639, 640itgadd 24359 . . . . 5 (𝜑 → ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
642619, 634, 6413eqtrrd 2866 . . . 4 (𝜑 → (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) = (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥))
643642oveq1d 7165 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π))
644636, 637itgcl 24318 . . . 4 (𝜑 → ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 ∈ ℂ)
645639, 640itgcl 24318 . . . 4 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
646644, 645, 142, 102divdird 11448 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)))
647483, 612itgcl 24318 . . . 4 (𝜑 → ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥 ∈ ℂ)
648647, 142, 102divcan3d 11415 . . 3 (𝜑 → ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
649643, 646, 6483eqtr3d 2869 . 2 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
65090, 458, 6493eqtrd 2865 1 (𝜑 → (𝑆𝑁) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3021  wral 3143  wrex 3144  Vcvv 3500  wss 3940  ifcif 4470   class class class wbr 5063  cmpt 5143  dom cdm 5554  cres 5556  wf 6350  cfv 6354  (class class class)co 7150  f cof 7401  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536   < clt 10669  cle 10670  cmin 10864  -cneg 10865   / cdiv 11291  cn 11632  2c2 11686  0cn0 11891  (,)cioo 12733  [,]cicc 12736  ...cfz 12887   mod cmo 13232  abscabs 14588  Σcsu 15037  sincsin 15412  cosccos 15413  πcpi 15415  cnccncf 23418  volcvol 23998  MblFncmbf 24149  𝐿1cibl 24152  citg 24153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cc 9851  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-disj 5029  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-ofr 7404  df-om 7574  df-1st 7685  df-2nd 7686  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8284  df-map 8403  df-pm 8404  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-fi 8869  df-sup 8900  df-inf 8901  df-oi 8968  df-dju 9324  df-card 9362  df-acn 9365  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-q 12343  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ioc 12738  df-ico 12739  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13425  df-fac 13629  df-bc 13658  df-hash 13686  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18170  df-cntz 18392  df-cmn 18844  df-psmet 20472  df-xmet 20473  df-met 20474  df-bl 20475  df-mopn 20476  df-fbas 20477  df-fg 20478  df-cnfld 20481  df-top 21437  df-topon 21454  df-topsp 21476  df-bases 21489  df-cld 21562  df-ntr 21563  df-cls 21564  df-nei 21641  df-lp 21679  df-perf 21680  df-cn 21770  df-cnp 21771  df-t1 21857  df-haus 21858  df-cmp 21930  df-tx 22105  df-hmeo 22298  df-fil 22389  df-fm 22481  df-flim 22482  df-flf 22483  df-xms 22864  df-ms 22865  df-tms 22866  df-cncf 23420  df-ovol 23999  df-vol 24000  df-mbf 24154  df-itg1 24155  df-itg2 24156  df-ibl 24157  df-itg 24158  df-0p 24205  df-limc 24398  df-dv 24399
This theorem is referenced by:  fourierdlem111  42387
  Copyright terms: Public domain W3C validator