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 38865
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 6534 . . . . . 6 (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
43sumeq1d 14227 . . . . 5 (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
54oveq2d 6542 . . . 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 11156 . . . . . . 7 0 ∈ ℕ0
109a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
119elexi 3185 . . . . . . 7 0 ∈ V
12 eleq1 2675 . . . . . . . . 9 (𝑛 = 0 → (𝑛 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1312anbi2d 735 . . . . . . . 8 (𝑛 = 0 → ((𝜑𝑛 ∈ ℕ0) ↔ (𝜑 ∧ 0 ∈ ℕ0)))
14 fveq2 6087 . . . . . . . . 9 (𝑛 = 0 → (𝐴𝑛) = (𝐴‘0))
1514eleq1d 2671 . . . . . . . 8 (𝑛 = 0 → ((𝐴𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
1613, 15imbi12d 332 . . . . . . 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 38805 . . . . . . . . 9 (𝜑 → ((𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵𝑛) ∈ ℝ)))
2322simpld 473 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ))
2423imp 443 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℝ)
2511, 16, 24vtocl 3231 . . . . . 6 ((𝜑 ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℝ)
268, 10, 25syl2anc 690 . . . . 5 (𝜑 → (𝐴‘0) ∈ ℝ)
2726rehalfcld 11128 . . . 4 (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28 fzfid 12591 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
29 eleq1 2675 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ0𝑛 ∈ ℕ0))
3029anbi2d 735 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ0) ↔ (𝜑𝑛 ∈ ℕ0)))
31 simpl 471 . . . . . . . . . . . . . . . . . 18 ((𝑘 = 𝑛𝑥𝐶) → 𝑘 = 𝑛)
3231oveq1d 6541 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑛𝑥𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
3332fveq2d 6091 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑛𝑥𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
3433oveq2d 6542 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
3534itgeq2dv 23298 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
3635eleq1d 2671 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
3730, 36imbi12d 332 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
3817adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝐹:ℝ⟶ℝ)
3919adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝐶) ∈ 𝐿1)
40 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
4138, 18, 39, 20, 40fourierdlem16 38799 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (((𝐴𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
4241simprd 477 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
4337, 42chvarv 2250 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44 pire 23958 . . . . . . . . . . . 12 π ∈ ℝ
4544a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ∈ ℝ)
46 0re 9896 . . . . . . . . . . . . 13 0 ∈ ℝ
47 pipos 23960 . . . . . . . . . . . . 13 0 < π
4846, 47gtneii 10000 . . . . . . . . . . . 12 π ≠ 0
4948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ≠ 0)
5043, 45, 49redivcld 10704 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
5150, 20fmptd 6276 . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℝ)
5251adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴:ℕ0⟶ℝ)
53 elfznn 12198 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
5453nnnn0d 11200 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ0)
5554adantl 480 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ0)
5652, 55ffvelrnd 6252 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) ∈ ℝ)
5755nn0red 11201 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58 fourierdlem83.x . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
5958adantr 479 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
6057, 59remulcld 9926 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
6160recoscld 14661 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
6256, 61remulcld 9926 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63 eleq1 2675 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
6463anbi2d 735 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ) ↔ (𝜑𝑛 ∈ ℕ)))
65 oveq1 6533 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
6665fveq2d 6091 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
6766oveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6867adantr 479 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6968itgeq2dv 23298 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
7069eleq1d 2671 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
7164, 70imbi12d 332 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
7217adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
7319adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹𝐶) ∈ 𝐿1)
74 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
7572, 18, 73, 21, 74fourierdlem21 38804 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((𝐵𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
7675simprd 477 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
7771, 76chvarv 2250 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
7844a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ∈ ℝ)
7948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ≠ 0)
8077, 78, 79redivcld 10704 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
8180, 21fmptd 6276 . . . . . . . . 9 (𝜑𝐵:ℕ⟶ℝ)
8281adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
8353adantl 480 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
8482, 83ffvelrnd 6252 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) ∈ ℝ)
8560resincld 14660 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
8684, 85remulcld 9926 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
8762, 86readdcld 9925 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8828, 87fsumrecl 14260 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8927, 88readdcld 9925 . . 3 (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
902, 6, 7, 89fvmptd 6181 . 2 (𝜑 → (𝑆𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
9120a1i 11 . . . . . . 7 (𝜑𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92 oveq1 6533 . . . . . . . . . . . . 13 (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
9392fveq2d 6091 . . . . . . . . . . . 12 (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
9493oveq2d 6542 . . . . . . . . . . 11 (𝑛 = 0 → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9594adantr 479 . . . . . . . . . 10 ((𝑛 = 0 ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9695itgeq2dv 23298 . . . . . . . . 9 (𝑛 = 0 → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9796adantl 480 . . . . . . . 8 ((𝜑𝑛 = 0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9897oveq1d 6541 . . . . . . 7 ((𝜑𝑛 = 0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
9917, 18, 19, 20, 10fourierdlem16 38799 . . . . . . . . 9 (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
10099simprd 477 . . . . . . . 8 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
10144a1i 11 . . . . . . . 8 (𝜑 → π ∈ ℝ)
10248a1i 11 . . . . . . . 8 (𝜑 → π ≠ 0)
103100, 101, 102redivcld 10704 . . . . . . 7 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
10491, 98, 10, 103fvmptd 6181 . . . . . 6 (𝜑 → (𝐴‘0) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105 ioosscn 38346 . . . . . . . . . . . . . . 15 (-π(,)π) ⊆ ℂ
106 id 22 . . . . . . . . . . . . . . . 16 (𝑥𝐶𝑥𝐶)
107106, 18syl6eleq 2697 . . . . . . . . . . . . . . 15 (𝑥𝐶𝑥 ∈ (-π(,)π))
108105, 107sseldi 3565 . . . . . . . . . . . . . 14 (𝑥𝐶𝑥 ∈ ℂ)
109108mul02d 10085 . . . . . . . . . . . . 13 (𝑥𝐶 → (0 · 𝑥) = 0)
110109fveq2d 6091 . . . . . . . . . . . 12 (𝑥𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111 cos0 14667 . . . . . . . . . . . 12 (cos‘0) = 1
112110, 111syl6eq 2659 . . . . . . . . . . 11 (𝑥𝐶 → (cos‘(0 · 𝑥)) = 1)
113112oveq2d 6542 . . . . . . . . . 10 (𝑥𝐶 → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
114113adantl 480 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
11517adantr 479 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝐹:ℝ⟶ℝ)
116 ioossre 12064 . . . . . . . . . . . . . 14 (-π(,)π) ⊆ ℝ
117116, 107sseldi 3565 . . . . . . . . . . . . 13 (𝑥𝐶𝑥 ∈ ℝ)
118117adantl 480 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝑥 ∈ ℝ)
119115, 118ffvelrnd 6252 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
120119recnd 9924 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
121120mulid1d 9913 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · 1) = (𝐹𝑥))
122114, 121eqtrd 2643 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = (𝐹𝑥))
123122itgeq2dv 23298 . . . . . . 7 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹𝑥) d𝑥)
124123oveq1d 6541 . . . . . 6 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹𝑥) d𝑥 / π))
125104, 124eqtrd 2643 . . . . 5 (𝜑 → (𝐴‘0) = (∫𝐶(𝐹𝑥) d𝑥 / π))
126125oveq1d 6541 . . . 4 (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2))
12717feqmptd 6143 . . . . . . . . 9 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
128127reseq1d 5302 . . . . . . . 8 (𝜑 → (𝐹𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶))
12944a1i 11 . . . . . . . . . . . 12 (𝑥𝐶 → π ∈ ℝ)
130129renegcld 10308 . . . . . . . . . . 11 (𝑥𝐶 → -π ∈ ℝ)
131 ioossicc 12088 . . . . . . . . . . . . 13 (-π(,)π) ⊆ (-π[,]π)
13218, 131eqsstri 3597 . . . . . . . . . . . 12 𝐶 ⊆ (-π[,]π)
133132sseli 3563 . . . . . . . . . . 11 (𝑥𝐶𝑥 ∈ (-π[,]π))
134 eliccre 38358 . . . . . . . . . . 11 ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135130, 129, 133, 134syl3anc 1317 . . . . . . . . . 10 (𝑥𝐶𝑥 ∈ ℝ)
136135ssriv 3571 . . . . . . . . 9 𝐶 ⊆ ℝ
137 resmpt 5355 . . . . . . . . 9 (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
138136, 137mp1i 13 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
139128, 138eqtr2d 2644 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝐹𝐶))
140139, 19eqeltrd 2687 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
141119, 140itgcl 23300 . . . . 5 (𝜑 → ∫𝐶(𝐹𝑥) d𝑥 ∈ ℂ)
142101recnd 9924 . . . . 5 (𝜑 → π ∈ ℂ)
143 2cnd 10942 . . . . 5 (𝜑 → 2 ∈ ℂ)
144 2ne0 10962 . . . . . 6 2 ≠ 0
145144a1i 11 . . . . 5 (𝜑 → 2 ≠ 0)
146141, 142, 143, 102, 145divdiv32d 10677 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π))
147141, 143, 145divrecd 10655 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)))
148143, 145reccld 10645 . . . . . . 7 (𝜑 → (1 / 2) ∈ ℂ)
149141, 148mulcomd 9917 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥))
150148, 119, 140itgmulc2 23350 . . . . . 6 (𝜑 → ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
151147, 149, 1503eqtrd 2647 . . . . 5 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
152151oveq1d 6541 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
153126, 146, 1523eqtrd 2647 . . 3 (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
15455, 50syldan 485 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
15520fvmpt2 6184 . . . . . . . . . 10 ((𝑛 ∈ ℕ0 ∧ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
15655, 154, 155syl2anc 690 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157156oveq1d 6541 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158154recnd 9924 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
15961recnd 9924 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160158, 159mulcomd 9917 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16155, 43syldan 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162161recnd 9924 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163142adantr 479 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
16448a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ≠ 0)
165159, 162, 163, 164divassd 10687 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16617ad2antrr 757 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝐹:ℝ⟶ℝ)
167117adantl 480 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
168166, 167ffvelrnd 6252 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
169 nn0re 11150 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
170169ad2antlr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
171170, 167remulcld 9926 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172171recoscld 14661 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173168, 172remulcld 9926 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
17454, 173sylanl2 680 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175 ioombl 23084 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) ∈ dom vol
17618, 175eqeltri 2683 . . . . . . . . . . . . . . . . . 18 𝐶 ∈ dom vol
177176elexi 3185 . . . . . . . . . . . . . . . . 17 𝐶 ∈ V
178177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ∈ V)
179 eqidd 2610 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180 eqidd 2610 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
181178, 172, 168, 179, 180offval2 6789 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
182172recnd 9924 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183120adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
184182, 183mulcomd 9917 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
185184mpteq2dva 4666 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
186181, 185eqtr2d 2644 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
187 coscn 23947 . . . . . . . . . . . . . . . . . 18 cos ∈ (ℂ–cn→ℂ)
188187a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → cos ∈ (ℂ–cn→ℂ))
189 ax-resscn 9849 . . . . . . . . . . . . . . . . . . . . 21 ℝ ⊆ ℂ
190136, 189sstri 3576 . . . . . . . . . . . . . . . . . . . 20 𝐶 ⊆ ℂ
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ⊆ ℂ)
192169recnd 9924 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
193192adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
194 ssid 3586 . . . . . . . . . . . . . . . . . . . 20 ℂ ⊆ ℂ
195194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → ℂ ⊆ ℂ)
196191, 193, 195constcncfg 38539 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
197191, 195idcncfg 38540 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
198196, 197mulcncf 22967 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
199188, 198cncfmpt1f 22471 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
200 cnmbf 23176 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201176, 199, 200sylancr 693 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202140adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
203 1re 9895 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
204 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205169adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑛 ∈ ℝ)
206117adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑥 ∈ ℝ)
207205, 206remulcld 9926 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208207recoscld 14661 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209208ralrimiva 2948 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ0 → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210209adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211 dmmptg 5534 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213204, 212eleqtrd 2689 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦𝐶)
214 eqidd 2610 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215 oveq2 6534 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216215fveq2d 6091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217216adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦𝐶)
219169adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑛 ∈ ℝ)
220136, 218sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦 ∈ ℝ)
221219, 220remulcld 9926 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222221recoscld 14661 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223214, 217, 218, 222fvmptd 6181 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224223fveq2d 6091 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225 abscosbd 38214 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227224, 226eqbrtrd 4599 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228213, 227syldan 485 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229228ralrimiva 2948 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230 breq2 4581 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231230ralbidv 2968 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232231rspcev 3281 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233203, 229, 232sylancr 693 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234233adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235 bddmulibl 23355 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
236201, 202, 234, 235syl3anc 1317 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
237186, 236eqeltrd 2687 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
23855, 237syldan 485 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
239159, 174, 238itgmulc2 23350 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240159adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241120adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
24254, 182sylanl2 680 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243240, 241, 242mul12d 10096 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244240, 242mulcomd 9917 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245244oveq2d 6542 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246243, 245eqtrd 2643 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247246itgeq2dv 23298 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248239, 247eqtrd 2643 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249248oveq1d 6541 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250165, 249eqtr3d 2645 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251157, 160, 2503eqtrd 2647 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
25283, 80syldan 485 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
25321fvmpt2 6184 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
25483, 252, 253syl2anc 690 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255254oveq1d 6541 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256252recnd 9924 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
25785recnd 9924 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258256, 257mulcomd 9917 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
25983, 77syldan 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260259recnd 9924 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261257, 260, 163, 164divassd 10687 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262119adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
263 nnre 10876 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264263adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
265117adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
266264, 265remulcld 9926 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267266resincld 14660 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268267adantll 745 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269262, 268remulcld 9926 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
27053, 269sylanl2 680 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ V)
272 eqidd 2610 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273 eqidd 2610 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
274271, 268, 262, 272, 273offval2 6789 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
275268recnd 9924 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276120adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
277275, 276mulcomd 9917 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
278277mpteq2dva 4666 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
279274, 278eqtr2d 2644 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
280 sincn 23946 . . . . . . . . . . . . . . . . . 18 sin ∈ (ℂ–cn→ℂ)
281280a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283263recnd 9924 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285282, 283, 284constcncfg 38539 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
286282, 284idcncfg 38540 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
287285, 286mulcncf 22967 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
288287adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
289281, 288cncfmpt1f 22471 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
290 cnmbf 23176 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291176, 289, 290sylancr 693 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292140adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
293 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294267ralrimiva 2948 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → ∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295 dmmptg 5534 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
296294, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
297296adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
298293, 297eleqtrd 2689 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦𝐶)
299 eqidd 2610 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300215fveq2d 6091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301300adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦𝐶)
303263adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
304136, 302sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
305303, 304remulcld 9926 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306305resincld 14660 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307299, 301, 302, 306fvmptd 6181 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308307fveq2d 6091 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309 abssinbd 38233 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310305, 309syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311308, 310eqbrtrd 4599 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312298, 311syldan 485 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313312ralrimiva 2948 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314 breq2 4581 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315314ralbidv 2968 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316315rspcev 3281 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317203, 313, 316sylancr 693 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318317adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319 bddmulibl 23355 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
320291, 292, 318, 319syl3anc 1317 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
321279, 320eqeltrd 2687 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
32283, 321syldan 485 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
323257, 270, 322itgmulc2 23350 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥)
324257adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
32553, 275sylanl2 680 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
326324, 241, 325mul12d 10096 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327324, 325mulcomd 9917 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328327oveq2d 6542 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329326, 328eqtrd 2643 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330329itgeq2dv 23298 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331323, 330eqtrd 2643 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332331oveq1d 6541 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333261, 332eqtr3d 2645 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334255, 258, 3333eqtrd 2647 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335251, 334oveq12d 6544 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
33654, 168sylanl2 680 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
33755, 208sylan 486 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
33861adantr 479 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339337, 338remulcld 9926 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340336, 339remulcld 9926 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341241, 242, 240mul13d 38215 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
342242, 241mulcomd 9917 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
343342oveq2d 6542 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
344341, 343eqtrd 2643 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
345344mpteq2dva 4666 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))))
346159, 174, 238iblmulc2 23347 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿1)
347345, 346eqeltrd 2687 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿1)
348340, 347itgcl 23300 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
34983, 267sylan 486 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
35085adantr 479 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351349, 350remulcld 9926 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352336, 351remulcld 9926 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353241, 325, 324mul13d 38215 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
354325, 241mulcomd 9917 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
355354oveq2d 6542 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
356353, 355eqtrd 2643 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
357356mpteq2dva 4666 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))))
358257, 270, 322iblmulc2 23347 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿1)
359357, 358eqeltrd 2687 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿1)
360352, 359itgcl 23300 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361348, 360, 163, 164divdird 10690 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
36253nncnd 10885 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363362ad2antlr 758 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℂ)
364108adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℂ)
36558recnd 9924 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℂ)
366365ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℂ)
367363, 364, 366subdid 10337 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368367fveq2d 6091 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369363, 364mulcld 9916 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370363, 366mulcld 9916 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371 cossub 14686 . . . . . . . . . . . . 13 (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372369, 370, 371syl2anc 690 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373368, 372eqtrd 2643 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374373oveq2d 6542 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375339recnd 9924 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376351recnd 9924 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377241, 375, 376adddid 9920 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378374, 377eqtrd 2643 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379378itgeq2dv 23298 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380340, 347, 352, 359itgadd 23341 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381379, 380eqtr2d 2644 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
382381oveq1d 6541 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
383335, 361, 3823eqtr2d 2649 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
384383sumeq2dv 14229 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
38557adantr 479 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
386117adantl 480 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
38758ad2antrr 757 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℝ)
388386, 387resubcld 10309 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
389385, 388remulcld 9926 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) ∈ ℝ)
390389recoscld 14661 . . . . . . 7 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
391336, 390remulcld 9926 . . . . . 6 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
392177a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393 eqidd 2610 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
394 eqidd 2610 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
395392, 390, 336, 393, 394offval2 6789 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))))
396390recnd 9924 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
397396, 241mulcomd 9917 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
398397mpteq2dva 4666 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
399395, 398eqtr2d 2644 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) = ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
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 38539 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶𝑋) ∈ (𝐶cn→ℂ))
407402, 406subcncf 38537 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑥𝑋)) ∈ (𝐶cn→ℂ))
408401, 407mulcncf 22967 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑛 · (𝑥𝑋))) ∈ (𝐶cn→ℂ))
409400, 408cncfmpt1f 22471 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ))
410 cnmbf 23176 . . . . . . . . 9 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
411176, 409, 410sylancr 693 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
412140adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
413 simpr 475 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
414390ralrimiva 2948 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
415 dmmptg 5534 . . . . . . . . . . . . . 14 (∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
416414, 415syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
417416adantr 479 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
418413, 417eleqtrd 2689 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦𝐶)
419 eqidd 2610 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
420 oveq1 6533 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑋) = (𝑦𝑋))
421420oveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑛 · (𝑥𝑋)) = (𝑛 · (𝑦𝑋)))
422421fveq2d 6091 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
423422adantl 480 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
424 simpr 475 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦𝐶)
42557adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
42655, 220sylan 486 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
42758ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑋 ∈ ℝ)
428426, 427resubcld 10309 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
429425, 428remulcld 9926 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑛 · (𝑦𝑋)) ∈ ℝ)
430429recoscld 14661 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (cos‘(𝑛 · (𝑦𝑋))) ∈ ℝ)
431419, 423, 424, 430fvmptd 6181 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦𝑋))))
432431fveq2d 6091 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦𝑋)))))
433 abscosbd 38214 . . . . . . . . . . . . 13 ((𝑛 · (𝑦𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
434429, 433syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
435432, 434eqbrtrd 4599 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
436418, 435syldan 485 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
437436ralrimiva 2948 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
438 breq2 4581 . . . . . . . . . . 11 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
439438ralbidv 2968 . . . . . . . . . 10 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
440439rspcev 3281 . . . . . . . . 9 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
441203, 437, 440sylancr 693 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
442 bddmulibl 23355 . . . . . . . 8 (((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
443411, 412, 441, 442syl3anc 1317 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
444399, 443eqeltrd 2687 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
445391, 444itgcl 23300 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
44628, 142, 445, 102fsumdivc 14308 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
447176a1i 11 . . . . . . . 8 (𝜑𝐶 ∈ dom vol)
448 anass 678 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)))
449 ancom 464 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶) ↔ (𝑥𝐶𝑛 ∈ (1...𝑁)))
450449anbi2i 725 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
451448, 450bitri 262 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
452451, 391sylbir 223 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
453447, 28, 452, 444itgfsum 23343 . . . . . . 7 (𝜑 → ((𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1 ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
454453simprd 477 . . . . . 6 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
455454eqcomd 2615 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
456455oveq1d 6541 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
457384, 446, 4563eqtr2d 2649 . . 3 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
458153, 457oveq12d 6544 . 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 2609 . . . . . . . . . . 11 (𝐷𝑁) = (𝐷𝑁)
462 eqid 2609 . . . . . . . . . . 11 (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463459, 460, 461, 462dirkertrigeq 38777 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐷𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464 oveq2 6534 . . . . . . . . . . . . . . 15 (𝑠 = (𝑥𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥𝑋)))
465464fveq2d 6091 . . . . . . . . . . . . . 14 (𝑠 = (𝑥𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥𝑋))))
466465sumeq2sdv 14230 . . . . . . . . . . . . 13 (𝑠 = (𝑥𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))
467466oveq2d 6542 . . . . . . . . . . . 12 (𝑠 = (𝑥𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
468467oveq1d 6541 . . . . . . . . . . 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 10309 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
472 halfre 11095 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
473472a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℝ)
474 fzfid 12591 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (1...𝑁) ∈ Fin)
475390an32s 841 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
476474, 475fsumrecl 14260 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
477473, 476readdcld 9925 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
47844a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ∈ ℝ)
47948a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ≠ 0)
480477, 478, 479redivcld 10704 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) ∈ ℝ)
481463, 469, 471, 480fvmptd 6181 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
482481, 480eqeltrd 2687 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
483119, 482remulcld 9926 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) ∈ ℝ)
484177a1i 11 . . . . . . . . . 10 (𝜑𝐶 ∈ V)
485 eqidd 2610 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
486 eqidd 2610 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
487484, 482, 119, 485, 486offval2 6789 . . . . . . . . 9 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
488482recnd 9924 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
489488, 120mulcomd 9917 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥)) = ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))))
490489mpteq2dva 4666 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
491487, 490eqtr2d 2644 . . . . . . . 8 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) = ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
492 eqid 2609 . . . . . . . . . . 11 (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))
493 eqid 2609 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋)))
494194a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℂ ⊆ ℂ)
495 cncfss 22457 . . . . . . . . . . . . . 14 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496189, 494, 495sylancr 693 . . . . . . . . . . . . 13 (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497 simpr 475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49858adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499497, 498resubcld 10309 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑥𝑋) ∈ ℝ)
500 eqid 2609 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ ↦ (𝑥𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥𝑋))
501499, 500fmptd 6276 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ)
502189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ℝ ⊆ ℂ)
503502, 494idcncfg 38540 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504502, 365, 494constcncfg 38539 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505503, 504subcncf 38537 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ))
506 cncffvrn 22456 . . . . . . . . . . . . . . . 16 ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
507189, 505, 506sylancr 693 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
508501, 507mpbird 245 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ))
509459dirkercncf 38783 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
5107, 509syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
511508, 510cncfcompt 38551 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℝ))
512496, 511sseldd 3568 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℂ))
51344renegcli 10193 . . . . . . . . . . . . . 14 -π ∈ ℝ
514 iccssre 12084 . . . . . . . . . . . . . 14 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515513, 44, 514mp2an 703 . . . . . . . . . . . . 13 (-π[,]π) ⊆ ℝ
516515a1i 11 . . . . . . . . . . . 12 (𝜑 → (-π[,]π) ⊆ ℝ)
517459dirkerf 38773 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (𝐷𝑁):ℝ⟶ℝ)
5187, 517syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁):ℝ⟶ℝ)
519518adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
520516sselda 3567 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
52158adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522520, 521resubcld 10309 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝑥𝑋) ∈ ℝ)
523519, 522ffvelrnd 6252 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
524523recnd 9924 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
525493, 512, 516, 494, 524cncfmptssg 38538 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526132a1i 11 . . . . . . . . . . 11 (𝜑𝐶 ⊆ (-π[,]π))
527492, 525, 526, 494, 488cncfmptssg 38538 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ))
528 cnmbf 23176 . . . . . . . . . 10 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
529176, 527, 528sylancr 693 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
530513a1i 11 . . . . . . . . . . . . 13 (𝜑 → -π ∈ ℝ)
531 0red 9897 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
532 negpilt0 38216 . . . . . . . . . . . . . . . 16 -π < 0
533532a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → -π < 0)
53447a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 < π)
535530, 531, 101, 533, 534lttrd 10049 . . . . . . . . . . . . . 14 (𝜑 → -π < π)
536530, 101, 535ltled 10036 . . . . . . . . . . . . 13 (𝜑 → -π ≤ π)
537493, 512, 516, 502, 523cncfmptssg 38538 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538530, 101, 536, 537evthiccabs 38348 . . . . . . . . . . . 12 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑤))))
539538simpld 473 . . . . . . . . . . 11 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)))
540 eqidd 2610 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
541420fveq2d 6091 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
542541adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
543 simpr 475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544518adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
545515, 543sseldi 3565 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
54658adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547545, 546resubcld 10309 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑦𝑋) ∈ ℝ)
548544, 547ffvelrnd 6252 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
549540, 542, 543, 548fvmptd 6181 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
550549fveq2d 6091 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
551550adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
552 eqidd 2610 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
553 oveq1 6533 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → (𝑥𝑋) = (𝑐𝑋))
554553fveq2d 6091 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
555554adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
556 simpr 475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557518adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
558515, 556sseldi 3565 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
55958adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560558, 559resubcld 10309 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑐𝑋) ∈ ℝ)
561557, 560ffvelrnd 6252 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℝ)
562552, 555, 556, 561fvmptd 6181 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐) = ((𝐷𝑁)‘(𝑐𝑋)))
563562fveq2d 6091 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
564563adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
565551, 564breq12d 4590 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
566565ralbidva 2967 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
567566rexbidva 3030 . . . . . . . . . . 11 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
568539, 567mpbid 220 . . . . . . . . . 10 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
569561recnd 9924 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℂ)
570569abscld 13971 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
5715703adant3 1073 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
572 nfv 1829 . . . . . . . . . . . . . 14 𝑦𝜑
573 nfv 1829 . . . . . . . . . . . . . 14 𝑦 𝑐 ∈ (-π[,]π)
574 nfra1 2924 . . . . . . . . . . . . . 14 𝑦𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))
575572, 573, 574nf3an 1818 . . . . . . . . . . . . 13 𝑦(𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
576 simpr 475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
577482ralrimiva 2948 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
578 dmmptg 5534 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
579577, 578syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
580579adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
581576, 580eleqtrd 2689 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
5825813ad2antl1 1215 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
583 eqidd 2610 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
584541adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦𝐶) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
585 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → 𝑦𝐶)
586518adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝐷𝑁):ℝ⟶ℝ)
587136, 585sseldi 3565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑦 ∈ ℝ)
58858adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑋 ∈ ℝ)
589587, 588resubcld 10309 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
590586, 589ffvelrnd 6252 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
591583, 584, 585, 590fvmptd 6181 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝐶) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
592591fveq2d 6091 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
593592adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
594 simplr 787 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
595132sseli 3563 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐶𝑦 ∈ (-π[,]π))
596595adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → 𝑦 ∈ (-π[,]π))
597 rspa 2913 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
598594, 596, 597syl2anc 690 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
599593, 598eqbrtrd 4599 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
6005993adantl2 1210 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
601582, 600syldan 485 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
602601ex 448 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
603575, 602ralrimi 2939 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
604 breq2 4581 . . . . . . . . . . . . . 14 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ((abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
605604ralbidv 2968 . . . . . . . . . . . . 13 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → (∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
606605rspcev 3281 . . . . . . . . . . . 12 (((abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
607571, 603, 606syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
608607rexlimdv3a 3014 . . . . . . . . . 10 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏))
609568, 608mpd 15 . . . . . . . . 9 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
610 bddmulibl 23355 . . . . . . . . 9 (((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
611529, 140, 609, 610syl3anc 1317 . . . . . . . 8 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
612491, 611eqeltrd 2687 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) ∈ 𝐿1)
613142, 483, 612itgmulc2 23350 . . . . . 6 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
614142adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐶) → π ∈ ℂ)
615120, 488, 614mul13d 38215 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
616489oveq2d 6542 . . . . . . . 8 ((𝜑𝑥𝐶) → (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
617615, 616eqtrd 2643 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
618617itgeq2dv 23298 . . . . . 6 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
619613, 618eqtr4d 2646 . . . . 5 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥)
620148adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℂ)
621620, 120mulcomd 9917 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) = ((𝐹𝑥) · (1 / 2)))
622396an32s 841 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
623474, 120, 622fsummulc2 14306 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
624623eqcomd 2615 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
625621, 624oveq12d 6544 . . . . . . 7 ((𝜑𝑥𝐶) → (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
626474, 622fsumcl 14259 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
627120, 620, 626adddid 9920 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
628481oveq1d 6541 . . . . . . . . 9 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π))
629620, 626addcld 9915 . . . . . . . . . 10 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℂ)
630629, 614, 479divcan1d 10653 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
631628, 630eqtr2d 2644 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = (((𝐷𝑁)‘(𝑥𝑋)) · π))
632631oveq2d 6542 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)))
633625, 627, 6323eqtr2rd 2650 . . . . . 6 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
634633itgeq2dv 23298 . . . . 5 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥)
635 remulcl 9877 . . . . . . 7 (((1 / 2) ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
636472, 119, 635sylancr 693 . . . . . 6 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
637148, 119, 140iblmulc2 23347 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ ((1 / 2) · (𝐹𝑥))) ∈ 𝐿1)
638391an32s 841 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
639474, 638fsumrecl 14260 . . . . . 6 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
640453simpld 473 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
641636, 637, 639, 640itgadd 23341 . . . . 5 (𝜑 → ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
642619, 634, 6413eqtrrd 2648 . . . 4 (𝜑 → (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) = (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥))
643642oveq1d 6541 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π))
644636, 637itgcl 23300 . . . 4 (𝜑 → ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 ∈ ℂ)
645639, 640itgcl 23300 . . . 4 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
646644, 645, 142, 102divdird 10690 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)))
647483, 612itgcl 23300 . . . 4 (𝜑 → ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥 ∈ ℂ)
648647, 142, 102divcan3d 10657 . . 3 (𝜑 → ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
649643, 646, 6483eqtr3d 2651 . 2 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
65090, 458, 6493eqtrd 2647 1 (𝜑 → (𝑆𝑁) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  Vcvv 3172  wss 3539  ifcif 4035   class class class wbr 4577  cmpt 4637  dom cdm 5027  cres 5029  wf 5785  cfv 5789  (class class class)co 6526  𝑓 cof 6770  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10535  cn 10869  2c2 10919  0cn0 11141  (,)cioo 12004  [,]cicc 12007  ...cfz 12154   mod cmo 12487  abscabs 13770  Σcsu 14212  sincsin 14581  cosccos 14582  πcpi 14584  cnccncf 22434  volcvol 22983  MblFncmbf 23133  𝐿1cibl 23136  citg 23137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cc 9117  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-of 6772  df-ofr 6773  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-omul 7429  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-acn 8628  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-5 10931  df-6 10932  df-7 10933  df-8 10934  df-9 10935  df-n0 11142  df-z 11213  df-dec 11328  df-uz 11522  df-q 11623  df-rp 11667  df-xneg 11780  df-xadd 11781  df-xmul 11782  df-ioo 12008  df-ioc 12009  df-ico 12010  df-icc 12011  df-fz 12155  df-fzo 12292  df-fl 12412  df-mod 12488  df-seq 12621  df-exp 12680  df-fac 12880  df-bc 12909  df-hash 12937  df-shft 13603  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-limsup 13998  df-clim 14015  df-rlim 14016  df-sum 14213  df-ef 14585  df-sin 14587  df-cos 14588  df-pi 14590  df-struct 15645  df-ndx 15646  df-slot 15647  df-base 15648  df-sets 15649  df-ress 15650  df-plusg 15729  df-mulr 15730  df-starv 15731  df-sca 15732  df-vsca 15733  df-ip 15734  df-tset 15735  df-ple 15736  df-ds 15739  df-unif 15740  df-hom 15741  df-cco 15742  df-rest 15854  df-topn 15855  df-0g 15873  df-gsum 15874  df-topgen 15875  df-pt 15876  df-prds 15879  df-xrs 15933  df-qtop 15938  df-imas 15939  df-xps 15941  df-mre 16017  df-mrc 16018  df-acs 16020  df-mgm 17013  df-sgrp 17055  df-mnd 17066  df-submnd 17107  df-mulg 17312  df-cntz 17521  df-cmn 17966  df-psmet 19507  df-xmet 19508  df-met 19509  df-bl 19510  df-mopn 19511  df-fbas 19512  df-fg 19513  df-cnfld 19516  df-top 20468  df-bases 20469  df-topon 20470  df-topsp 20471  df-cld 20580  df-ntr 20581  df-cls 20582  df-nei 20659  df-lp 20697  df-perf 20698  df-cn 20788  df-cnp 20789  df-t1 20875  df-haus 20876  df-cmp 20947  df-tx 21122  df-hmeo 21315  df-fil 21407  df-fm 21499  df-flim 21500  df-flf 21501  df-xms 21882  df-ms 21883  df-tms 21884  df-cncf 22436  df-ovol 22984  df-vol 22985  df-mbf 23138  df-itg1 23139  df-itg2 23140  df-ibl 23141  df-itg 23142  df-0p 23187  df-limc 23380  df-dv 23381
This theorem is referenced by:  fourierdlem111  38893
  Copyright terms: Public domain W3C validator