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 41043
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 6850 . . . . . 6 (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
43sumeq1d 14716 . . . . 5 (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
54oveq2d 6858 . . . 4 (𝑚 = 𝑁 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
65adantl 473 . . 3 ((𝜑𝑚 = 𝑁) → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
7 fourierdlem83.n . . 3 (𝜑𝑁 ∈ ℕ)
8 id 22 . . . . . 6 (𝜑𝜑)
9 0nn0 11555 . . . . . . 7 0 ∈ ℕ0
109a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
119elexi 3366 . . . . . . 7 0 ∈ V
12 eleq1 2832 . . . . . . . . 9 (𝑛 = 0 → (𝑛 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1312anbi2d 622 . . . . . . . 8 (𝑛 = 0 → ((𝜑𝑛 ∈ ℕ0) ↔ (𝜑 ∧ 0 ∈ ℕ0)))
14 fveq2 6375 . . . . . . . . 9 (𝑛 = 0 → (𝐴𝑛) = (𝐴‘0))
1514eleq1d 2829 . . . . . . . 8 (𝑛 = 0 → ((𝐴𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
1613, 15imbi12d 335 . . . . . . 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 40983 . . . . . . . . 9 (𝜑 → ((𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵𝑛) ∈ ℝ)))
2322simpld 488 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ))
2423imp 395 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℝ)
2511, 16, 24vtocl 3411 . . . . . 6 ((𝜑 ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℝ)
268, 10, 25syl2anc 579 . . . . 5 (𝜑 → (𝐴‘0) ∈ ℝ)
2726rehalfcld 11525 . . . 4 (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28 fzfid 12980 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
29 eleq1 2832 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ0𝑛 ∈ ℕ0))
3029anbi2d 622 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ0) ↔ (𝜑𝑛 ∈ ℕ0)))
31 simpl 474 . . . . . . . . . . . . . . . . . 18 ((𝑘 = 𝑛𝑥𝐶) → 𝑘 = 𝑛)
3231oveq1d 6857 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑛𝑥𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
3332fveq2d 6379 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑛𝑥𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
3433oveq2d 6858 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
3534itgeq2dv 23839 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
3635eleq1d 2829 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
3730, 36imbi12d 335 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
3817adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝐹:ℝ⟶ℝ)
3919adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝐶) ∈ 𝐿1)
40 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
4138, 18, 39, 20, 40fourierdlem16 40977 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (((𝐴𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
4241simprd 489 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
4337, 42chvarv 2369 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44 pire 24502 . . . . . . . . . . . 12 π ∈ ℝ
4544a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ∈ ℝ)
46 0re 10295 . . . . . . . . . . . . 13 0 ∈ ℝ
47 pipos 24504 . . . . . . . . . . . . 13 0 < π
4846, 47gtneii 10403 . . . . . . . . . . . 12 π ≠ 0
4948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → π ≠ 0)
5043, 45, 49redivcld 11107 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
5150, 20fmptd 6574 . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℝ)
5251adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴:ℕ0⟶ℝ)
53 elfznn 12577 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
5453nnnn0d 11598 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ0)
5554adantl 473 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ0)
5652, 55ffvelrnd 6550 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) ∈ ℝ)
5755nn0red 11599 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58 fourierdlem83.x . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
5958adantr 472 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
6057, 59remulcld 10324 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
6160recoscld 15156 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
6256, 61remulcld 10324 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63 eleq1 2832 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
6463anbi2d 622 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((𝜑𝑘 ∈ ℕ) ↔ (𝜑𝑛 ∈ ℕ)))
65 oveq1 6849 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
6665fveq2d 6379 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
6766oveq2d 6858 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6867adantr 472 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑛𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
6968itgeq2dv 23839 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
7069eleq1d 2829 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
7164, 70imbi12d 335 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
7217adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
7319adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝐹𝐶) ∈ 𝐿1)
74 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
7572, 18, 73, 21, 74fourierdlem21 40982 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((𝐵𝑘) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
7675simprd 489 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
7771, 76chvarv 2369 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
7844a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ∈ ℝ)
7948a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → π ≠ 0)
8077, 78, 79redivcld 11107 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
8180, 21fmptd 6574 . . . . . . . . 9 (𝜑𝐵:ℕ⟶ℝ)
8281adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
8353adantl 473 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
8482, 83ffvelrnd 6550 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) ∈ ℝ)
8560resincld 15155 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
8684, 85remulcld 10324 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
8762, 86readdcld 10323 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8828, 87fsumrecl 14750 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
8927, 88readdcld 10323 . . 3 (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
902, 6, 7, 89fvmptd 6477 . 2 (𝜑 → (𝑆𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
9120a1i 11 . . . . . . 7 (𝜑𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92 oveq1 6849 . . . . . . . . . . . . 13 (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
9392fveq2d 6379 . . . . . . . . . . . 12 (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
9493oveq2d 6858 . . . . . . . . . . 11 (𝑛 = 0 → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9594adantr 472 . . . . . . . . . 10 ((𝑛 = 0 ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (cos‘(0 · 𝑥))))
9695itgeq2dv 23839 . . . . . . . . 9 (𝑛 = 0 → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9796adantl 473 . . . . . . . 8 ((𝜑𝑛 = 0) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥)
9897oveq1d 6857 . . . . . . 7 ((𝜑𝑛 = 0) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
9917, 18, 19, 20, 10fourierdlem16 40977 . . . . . . . . 9 (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
10099simprd 489 . . . . . . . 8 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
10144a1i 11 . . . . . . . 8 (𝜑 → π ∈ ℝ)
10248a1i 11 . . . . . . . 8 (𝜑 → π ≠ 0)
103100, 101, 102redivcld 11107 . . . . . . 7 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
10491, 98, 10, 103fvmptd 6477 . . . . . 6 (𝜑 → (𝐴‘0) = (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105 ioosscn 40358 . . . . . . . . . . . . . . 15 (-π(,)π) ⊆ ℂ
106 id 22 . . . . . . . . . . . . . . . 16 (𝑥𝐶𝑥𝐶)
107106, 18syl6eleq 2854 . . . . . . . . . . . . . . 15 (𝑥𝐶𝑥 ∈ (-π(,)π))
108105, 107sseldi 3759 . . . . . . . . . . . . . 14 (𝑥𝐶𝑥 ∈ ℂ)
109108mul02d 10488 . . . . . . . . . . . . 13 (𝑥𝐶 → (0 · 𝑥) = 0)
110109fveq2d 6379 . . . . . . . . . . . 12 (𝑥𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111 cos0 15162 . . . . . . . . . . . 12 (cos‘0) = 1
112110, 111syl6eq 2815 . . . . . . . . . . 11 (𝑥𝐶 → (cos‘(0 · 𝑥)) = 1)
113112oveq2d 6858 . . . . . . . . . 10 (𝑥𝐶 → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
114113adantl 473 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = ((𝐹𝑥) · 1))
11517adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝐹:ℝ⟶ℝ)
116 ioossre 12437 . . . . . . . . . . . . . 14 (-π(,)π) ⊆ ℝ
117116, 107sseldi 3759 . . . . . . . . . . . . 13 (𝑥𝐶𝑥 ∈ ℝ)
118117adantl 473 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → 𝑥 ∈ ℝ)
119115, 118ffvelrnd 6550 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
120119recnd 10322 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
121120mulid1d 10311 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · 1) = (𝐹𝑥))
122114, 121eqtrd 2799 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (cos‘(0 · 𝑥))) = (𝐹𝑥))
123122itgeq2dv 23839 . . . . . . 7 (𝜑 → ∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹𝑥) d𝑥)
124123oveq1d 6857 . . . . . 6 (𝜑 → (∫𝐶((𝐹𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹𝑥) d𝑥 / π))
125104, 124eqtrd 2799 . . . . 5 (𝜑 → (𝐴‘0) = (∫𝐶(𝐹𝑥) d𝑥 / π))
126125oveq1d 6857 . . . 4 (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2))
12717feqmptd 6438 . . . . . . . . 9 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
128127reseq1d 5564 . . . . . . . 8 (𝜑 → (𝐹𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶))
12944a1i 11 . . . . . . . . . . . 12 (𝑥𝐶 → π ∈ ℝ)
130129renegcld 10711 . . . . . . . . . . 11 (𝑥𝐶 → -π ∈ ℝ)
131 ioossicc 12461 . . . . . . . . . . . . 13 (-π(,)π) ⊆ (-π[,]π)
13218, 131eqsstri 3795 . . . . . . . . . . . 12 𝐶 ⊆ (-π[,]π)
133132sseli 3757 . . . . . . . . . . 11 (𝑥𝐶𝑥 ∈ (-π[,]π))
134 eliccre 40370 . . . . . . . . . . 11 ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135130, 129, 133, 134syl3anc 1490 . . . . . . . . . 10 (𝑥𝐶𝑥 ∈ ℝ)
136135ssriv 3765 . . . . . . . . 9 𝐶 ⊆ ℝ
137 resmpt 5626 . . . . . . . . 9 (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
138136, 137mp1i 13 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
139128, 138eqtr2d 2800 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝐹𝐶))
140139, 19eqeltrd 2844 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
141119, 140itgcl 23841 . . . . 5 (𝜑 → ∫𝐶(𝐹𝑥) d𝑥 ∈ ℂ)
142101recnd 10322 . . . . 5 (𝜑 → π ∈ ℂ)
143 2cnd 11350 . . . . 5 (𝜑 → 2 ∈ ℂ)
144 2ne0 11383 . . . . . 6 2 ≠ 0
145144a1i 11 . . . . 5 (𝜑 → 2 ≠ 0)
146141, 142, 143, 102, 145divdiv32d 11080 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π))
147141, 143, 145divrecd 11058 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)))
148143, 145reccld 11048 . . . . . . 7 (𝜑 → (1 / 2) ∈ ℂ)
149141, 148mulcomd 10315 . . . . . 6 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥))
150148, 119, 140itgmulc2 23891 . . . . . 6 (𝜑 → ((1 / 2) · ∫𝐶(𝐹𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
151147, 149, 1503eqtrd 2803 . . . . 5 (𝜑 → (∫𝐶(𝐹𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥)
152151oveq1d 6857 . . . 4 (𝜑 → ((∫𝐶(𝐹𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
153126, 146, 1523eqtrd 2803 . . 3 (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π))
15455, 50syldan 585 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
15520fvmpt2 6480 . . . . . . . . . 10 ((𝑛 ∈ ℕ0 ∧ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
15655, 154, 155syl2anc 579 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴𝑛) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157156oveq1d 6857 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158154recnd 10322 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
15961recnd 10322 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160158, 159mulcomd 10315 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16155, 43syldan 585 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162161recnd 10322 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163142adantr 472 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
16448a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → π ≠ 0)
165159, 162, 163, 164divassd 11090 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
16617ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝐹:ℝ⟶ℝ)
167117adantl 473 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
168166, 167ffvelrnd 6550 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
169 nn0re 11548 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
170169ad2antlr 718 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
171170, 167remulcld 10324 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172171recoscld 15156 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173168, 172remulcld 10324 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
17454, 173sylanl2 671 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175 ioombl 23623 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) ∈ dom vol
17618, 175eqeltri 2840 . . . . . . . . . . . . . . . . . 18 𝐶 ∈ dom vol
177176elexi 3366 . . . . . . . . . . . . . . . . 17 𝐶 ∈ V
178177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ∈ V)
179 eqidd 2766 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180 eqidd 2766 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
181178, 172, 168, 179, 180offval2 7112 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
182172recnd 10322 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183120adantlr 706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
184182, 183mulcomd 10315 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
185184mpteq2dva 4903 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
186181, 185eqtr2d 2800 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
187 coscn 24490 . . . . . . . . . . . . . . . . . 18 cos ∈ (ℂ–cn→ℂ)
188187a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → cos ∈ (ℂ–cn→ℂ))
189 ax-resscn 10246 . . . . . . . . . . . . . . . . . . . . 21 ℝ ⊆ ℂ
190136, 189sstri 3770 . . . . . . . . . . . . . . . . . . . 20 𝐶 ⊆ ℂ
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ⊆ ℂ)
192169recnd 10322 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
193192adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
194 ssid 3783 . . . . . . . . . . . . . . . . . . . 20 ℂ ⊆ ℂ
195194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ0) → ℂ ⊆ ℂ)
196191, 193, 195constcncfg 40722 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
197191, 195idcncfg 40723 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
198196, 197mulcncf 23504 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
199188, 198cncfmpt1f 22995 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
200 cnmbf 23717 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201176, 199, 200sylancr 581 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202140adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
203 1re 10293 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
204 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205169adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑛 ∈ ℝ)
206117adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑥 ∈ ℝ)
207205, 206remulcld 10324 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208207recoscld 15156 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209208ralrimiva 3113 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ0 → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210209adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211 dmmptg 5818 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213204, 212eleqtrd 2846 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦𝐶)
214 eqidd 2766 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215 oveq2 6850 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216215fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217216adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦𝐶)
219169adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑛 ∈ ℝ)
220136, 218sseldi 3759 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦 ∈ ℝ)
221219, 220remulcld 10324 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222221recoscld 15156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ0𝑦𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223214, 217, 218, 222fvmptd 6477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ0𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224223fveq2d 6379 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225 abscosbd 40130 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227224, 226eqbrtrd 4831 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228213, 227syldan 585 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229228ralrimiva 3113 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230 breq2 4813 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231230ralbidv 3133 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232231rspcev 3461 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233203, 229, 232sylancr 581 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234233adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235 bddmulibl 23896 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
236201, 202, 234, 235syl3anc 1490 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
237186, 236eqeltrd 2844 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
23855, 237syldan 585 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿1)
239159, 174, 238itgmulc2 23891 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240159adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241120adantlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
24254, 182sylanl2 671 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243240, 241, 242mul12d 10499 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244240, 242mulcomd 10315 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245244oveq2d 6858 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246243, 245eqtrd 2799 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247246itgeq2dv 23839 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248239, 247eqtrd 2799 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249248oveq1d 6857 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250165, 249eqtr3d 2801 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251157, 160, 2503eqtrd 2803 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
25283, 80syldan 585 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
25321fvmpt2 6480 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
25483, 252, 253syl2anc 579 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐵𝑛) = (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255254oveq1d 6857 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256252recnd 10322 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
25785recnd 10322 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258256, 257mulcomd 10315 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
25983, 77syldan 585 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260259recnd 10322 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261257, 260, 163, 164divassd 11090 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262119adantlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
263 nnre 11282 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264263adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
265117adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
266264, 265remulcld 10324 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267266resincld 15155 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268267adantll 705 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269262, 268remulcld 10324 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
27053, 269sylanl2 671 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271177a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ V)
272 eqidd 2766 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273 eqidd 2766 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
274271, 268, 262, 272, 273offval2 7112 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
275268recnd 10322 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276120adantlr 706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
277275, 276mulcomd 10315 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
278277mpteq2dva 4903 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
279274, 278eqtr2d 2800 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
280 sincn 24489 . . . . . . . . . . . . . . . . . 18 sin ∈ (ℂ–cn→ℂ)
281280a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283263recnd 10322 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285282, 283, 284constcncfg 40722 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
286282, 284idcncfg 40723 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
287285, 286mulcncf 23504 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
288287adantl 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
289281, 288cncfmpt1f 22995 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
290 cnmbf 23717 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291176, 289, 290sylancr 581 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292140adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
293 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294267ralrimiva 3113 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → ∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295 dmmptg 5818 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
296294, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
297296adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
298293, 297eleqtrd 2846 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦𝐶)
299 eqidd 2766 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300215fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301300adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦𝐶)
303263adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
304136, 302sseldi 3759 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
305303, 304remulcld 10324 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306305resincld 15155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307299, 301, 302, 306fvmptd 6477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308307fveq2d 6379 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309 abssinbd 40148 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310305, 309syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311308, 310eqbrtrd 4831 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312298, 311syldan 585 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313312ralrimiva 3113 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314 breq2 4813 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315314ralbidv 3133 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316315rspcev 3461 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317203, 313, 316sylancr 581 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318317adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319 bddmulibl 23896 . . . . . . . . . . . . . . 15 (((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
320291, 292, 318, 319syl3anc 1490 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
321279, 320eqeltrd 2844 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
32283, 321syldan 585 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
323257, 270, 322itgmulc2 23891 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥)
324257adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
32553, 275sylanl2 671 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
326324, 241, 325mul12d 10499 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327324, 325mulcomd 10315 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328327oveq2d 6858 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329326, 328eqtrd 2799 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330329itgeq2dv 23839 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331323, 330eqtrd 2799 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332331oveq1d 6857 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333261, 332eqtr3d 2801 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334255, 258, 3333eqtrd 2803 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335251, 334oveq12d 6860 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
33654, 168sylanl2 671 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
33755, 208sylan 575 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
33861adantr 472 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339337, 338remulcld 10324 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340336, 339remulcld 10324 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341241, 242, 240mul13d 40131 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))))
342242, 241mulcomd 10315 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))
343342oveq2d 6858 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
344341, 343eqtrd 2799 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥)))))
345344mpteq2dva 4903 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))))
346159, 174, 238iblmulc2 23888 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿1)
347345, 346eqeltrd 2844 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿1)
348340, 347itgcl 23841 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
34983, 267sylan 575 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
35085adantr 472 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351349, 350remulcld 10324 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352336, 351remulcld 10324 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353241, 325, 324mul13d 40131 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
354325, 241mulcomd 10315 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
355354oveq2d 6858 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
356353, 355eqtrd 2799 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
357356mpteq2dva 4903 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))))
358257, 270, 322iblmulc2 23888 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿1)
359357, 358eqeltrd 2844 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿1)
360352, 359itgcl 23841 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361348, 360, 163, 164divdird 11093 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
36253nncnd 11292 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363362ad2antlr 718 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℂ)
364108adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℂ)
36558recnd 10322 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ℂ)
366365ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℂ)
367363, 364, 366subdid 10740 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368367fveq2d 6379 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369363, 364mulcld 10314 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370363, 366mulcld 10314 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371 cossub 15181 . . . . . . . . . . . . 13 (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372369, 370, 371syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373368, 372eqtrd 2799 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374373oveq2d 6858 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375339recnd 10322 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376351recnd 10322 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377241, 375, 376adddid 10318 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378374, 377eqtrd 2799 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = (((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379378itgeq2dv 23839 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380340, 347, 352, 359itgadd 23882 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381379, 380eqtr2d 2800 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
382381oveq1d 6857 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
383335, 361, 3823eqtr2d 2805 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
384383sumeq2dv 14718 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
38557adantr 472 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑛 ∈ ℝ)
386117adantl 473 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑥 ∈ ℝ)
38758ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → 𝑋 ∈ ℝ)
388386, 387resubcld 10712 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
389385, 388remulcld 10324 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (𝑛 · (𝑥𝑋)) ∈ ℝ)
390389recoscld 15156 . . . . . . 7 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
391336, 390remulcld 10324 . . . . . 6 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
392177a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393 eqidd 2766 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
394 eqidd 2766 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
395392, 390, 336, 393, 394offval2 7112 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))))
396390recnd 10322 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
397396, 241mulcomd 10315 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) → ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥)) = ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
398397mpteq2dva 4903 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((cos‘(𝑛 · (𝑥𝑋))) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
399395, 398eqtr2d 2800 . . . . . . 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 472 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
405194a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ℂ ⊆ ℂ)
406403, 404, 405constcncfg 40722 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶𝑋) ∈ (𝐶cn→ℂ))
407402, 406subcncf 40720 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑥𝑋)) ∈ (𝐶cn→ℂ))
408401, 407mulcncf 23504 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝑛 · (𝑥𝑋))) ∈ (𝐶cn→ℂ))
409400, 408cncfmpt1f 22995 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ))
410 cnmbf 23717 . . . . . . . . 9 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
411176, 409, 410sylancr 581 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn)
412140adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
413 simpr 477 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
414390ralrimiva 3113 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
415 dmmptg 5818 . . . . . . . . . . . . . 14 (∀𝑥𝐶 (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
416414, 415syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
417416adantr 472 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = 𝐶)
418413, 417eleqtrd 2846 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → 𝑦𝐶)
419 eqidd 2766 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) = (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))))
420 oveq1 6849 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑋) = (𝑦𝑋))
421420oveq2d 6858 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑛 · (𝑥𝑋)) = (𝑛 · (𝑦𝑋)))
422421fveq2d 6379 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
423422adantl 473 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥𝑋))) = (cos‘(𝑛 · (𝑦𝑋))))
424 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦𝐶)
42557adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑛 ∈ ℝ)
42655, 220sylan 575 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑦 ∈ ℝ)
42758ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → 𝑋 ∈ ℝ)
428426, 427resubcld 10712 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
429425, 428remulcld 10324 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (𝑛 · (𝑦𝑋)) ∈ ℝ)
430429recoscld 15156 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (cos‘(𝑛 · (𝑦𝑋))) ∈ ℝ)
431419, 423, 424, 430fvmptd 6477 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦𝑋))))
432431fveq2d 6379 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦𝑋)))))
433 abscosbd 40130 . . . . . . . . . . . . 13 ((𝑛 · (𝑦𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
434429, 433syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘(cos‘(𝑛 · (𝑦𝑋)))) ≤ 1)
435432, 434eqbrtrd 4831 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
436418, 435syldan 585 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))) → (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
437436ralrimiva 3113 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1)
438 breq2 4813 . . . . . . . . . . 11 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
439438ralbidv 3133 . . . . . . . . . 10 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1))
440439rspcev 3461 . . . . . . . . 9 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
441203, 437, 440sylancr 581 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏)
442 bddmulibl 23896 . . . . . . . 8 (((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))(abs‘((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
443411, 412, 441, 442syl3anc 1490 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑥𝐶 ↦ (cos‘(𝑛 · (𝑥𝑋)))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
444399, 443eqeltrd 2844 . . . . . 6 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑥𝐶 ↦ ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
445391, 444itgcl 23841 . . . . 5 ((𝜑𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
44628, 142, 445, 102fsumdivc 14802 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
447176a1i 11 . . . . . . . 8 (𝜑𝐶 ∈ dom vol)
448 anass 460 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)))
449 ancom 452 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶) ↔ (𝑥𝐶𝑛 ∈ (1...𝑁)))
450449anbi2i 616 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥𝐶)) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
451448, 450bitri 266 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑥𝐶) ↔ (𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))))
452451, 391sylbir 226 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐶𝑛 ∈ (1...𝑁))) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
453447, 28, 452, 444itgfsum 23884 . . . . . . 7 (𝜑 → ((𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1 ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
454453simprd 489 . . . . . 6 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
455454eqcomd 2771 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥)
456455oveq1d 6857 . . . 4 (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
457384, 446, 4563eqtr2d 2805 . . 3 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π))
458153, 457oveq12d 6860 . 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 472 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝑁 ∈ ℕ)
461 eqid 2765 . . . . . . . . . . 11 (𝐷𝑁) = (𝐷𝑁)
462 eqid 2765 . . . . . . . . . . 11 (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463459, 460, 461, 462dirkertrigeq 40955 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐷𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464 oveq2 6850 . . . . . . . . . . . . . . 15 (𝑠 = (𝑥𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥𝑋)))
465464fveq2d 6379 . . . . . . . . . . . . . 14 (𝑠 = (𝑥𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥𝑋))))
466465sumeq2sdv 14720 . . . . . . . . . . . . 13 (𝑠 = (𝑥𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))
467466oveq2d 6858 . . . . . . . . . . . 12 (𝑠 = (𝑥𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
468467oveq1d 6857 . . . . . . . . . . 11 (𝑠 = (𝑥𝑋) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
469468adantl 473 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑠 = (𝑥𝑋)) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
47058adantr 472 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → 𝑋 ∈ ℝ)
471118, 470resubcld 10712 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝑥𝑋) ∈ ℝ)
472 halfre 11492 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
473472a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℝ)
474 fzfid 12980 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (1...𝑁) ∈ Fin)
475390an32s 642 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
476474, 475fsumrecl 14750 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℝ)
477473, 476readdcld 10323 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
47844a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ∈ ℝ)
47948a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → π ≠ 0)
480477, 478, 479redivcld 11107 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) ∈ ℝ)
481463, 469, 471, 480fvmptd 6477 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π))
482481, 480eqeltrd 2844 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
483119, 482remulcld 10324 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) ∈ ℝ)
484177a1i 11 . . . . . . . . . 10 (𝜑𝐶 ∈ V)
485 eqidd 2766 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
486 eqidd 2766 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
487484, 482, 119, 485, 486offval2 7112 . . . . . . . . 9 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
488482recnd 10322 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
489488, 120mulcomd 10315 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥)) = ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))))
490489mpteq2dva 4903 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
491487, 490eqtr2d 2800 . . . . . . . 8 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) = ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))))
492 eqid 2765 . . . . . . . . . . 11 (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))
493 eqid 2765 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋)))
494194a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℂ ⊆ ℂ)
495 cncfss 22981 . . . . . . . . . . . . . 14 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496189, 494, 495sylancr 581 . . . . . . . . . . . . 13 (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49858adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499497, 498resubcld 10712 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑥𝑋) ∈ ℝ)
500 eqid 2765 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ ↦ (𝑥𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥𝑋))
501499, 500fmptd 6574 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ)
502189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ℝ ⊆ ℂ)
503502, 494idcncfg 40723 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504502, 365, 494constcncfg 40722 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505503, 504subcncf 40720 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ))
506 cncffvrn 22980 . . . . . . . . . . . . . . . 16 ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
507189, 505, 506sylancr 581 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥𝑋)):ℝ⟶ℝ))
508501, 507mpbird 248 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥𝑋)) ∈ (ℝ–cn→ℝ))
509459dirkercncf 40961 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
5107, 509syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝑁) ∈ (ℝ–cn→ℝ))
511508, 510cncfcompt 40734 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℝ))
512496, 511sseldd 3762 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (ℝ–cn→ℂ))
51344renegcli 10596 . . . . . . . . . . . . . 14 -π ∈ ℝ
514 iccssre 12457 . . . . . . . . . . . . . 14 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515513, 44, 514mp2an 683 . . . . . . . . . . . . 13 (-π[,]π) ⊆ ℝ
516515a1i 11 . . . . . . . . . . . 12 (𝜑 → (-π[,]π) ⊆ ℝ)
517459dirkerf 40951 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (𝐷𝑁):ℝ⟶ℝ)
5187, 517syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁):ℝ⟶ℝ)
519518adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
520516sselda 3761 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
52158adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522520, 521resubcld 10712 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (-π[,]π)) → (𝑥𝑋) ∈ ℝ)
523519, 522ffvelrnd 6550 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
524523recnd 10322 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℂ)
525493, 512, 516, 494, 524cncfmptssg 40721 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526132a1i 11 . . . . . . . . . . 11 (𝜑𝐶 ⊆ (-π[,]π))
527492, 525, 526, 494, 488cncfmptssg 40721 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ))
528 cnmbf 23717 . . . . . . . . . 10 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
529176, 527, 528sylancr 581 . . . . . . . . 9 (𝜑 → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn)
530513a1i 11 . . . . . . . . . . . . 13 (𝜑 → -π ∈ ℝ)
531 0red 10297 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
532 negpilt0 40132 . . . . . . . . . . . . . . . 16 -π < 0
533532a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → -π < 0)
53447a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 < π)
535530, 531, 101, 533, 534lttrd 10452 . . . . . . . . . . . . . 14 (𝜑 → -π < π)
536530, 101, 535ltled 10439 . . . . . . . . . . . . 13 (𝜑 → -π ≤ π)
537493, 512, 516, 502, 523cncfmptssg 40721 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538530, 101, 536, 537evthiccabs 40360 . . . . . . . . . . . 12 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑤))))
539538simpld 488 . . . . . . . . . . 11 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)))
540 eqidd 2766 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
541420fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
542541adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
543 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544518adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
545515, 543sseldi 3759 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
54658adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547545, 546resubcld 10712 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (-π[,]π)) → (𝑦𝑋) ∈ ℝ)
548544, 547ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
549540, 542, 543, 548fvmptd 6477 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
550549fveq2d 6379 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
551550adantlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
552 eqidd 2766 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋))))
553 oveq1 6849 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → (𝑥𝑋) = (𝑐𝑋))
554553fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
555554adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑐𝑋)))
556 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557518adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝐷𝑁):ℝ⟶ℝ)
558515, 556sseldi 3759 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
55958adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560558, 559resubcld 10712 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ (-π[,]π)) → (𝑐𝑋) ∈ ℝ)
561557, 560ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℝ)
562552, 555, 556, 561fvmptd 6477 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐) = ((𝐷𝑁)‘(𝑐𝑋)))
563562fveq2d 6379 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
564563adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) = (abs‘((𝐷𝑁)‘(𝑐𝑋))))
565551, 564breq12d 4822 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
566565ralbidva 3132 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
567566rexbidva 3196 . . . . . . . . . . 11 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
568539, 567mpbid 223 . . . . . . . . . 10 (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
569561recnd 10322 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ (-π[,]π)) → ((𝐷𝑁)‘(𝑐𝑋)) ∈ ℂ)
570569abscld 14460 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
5715703adant3 1162 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ)
572 nfv 2009 . . . . . . . . . . . . . 14 𝑦𝜑
573 nfv 2009 . . . . . . . . . . . . . 14 𝑦 𝑐 ∈ (-π[,]π)
574 nfra1 3088 . . . . . . . . . . . . . 14 𝑦𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))
575572, 573, 574nf3an 2000 . . . . . . . . . . . . 13 𝑦(𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
576 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
577482ralrimiva 3113 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ)
578 dmmptg 5818 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐶 ((𝐷𝑁)‘(𝑥𝑋)) ∈ ℝ → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
579577, 578syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
580579adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = 𝐶)
581576, 580eleqtrd 2846 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
5825813ad2antl1 1236 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → 𝑦𝐶)
583 eqidd 2766 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) = (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))))
584541adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦𝐶) ∧ 𝑥 = 𝑦) → ((𝐷𝑁)‘(𝑥𝑋)) = ((𝐷𝑁)‘(𝑦𝑋)))
585 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → 𝑦𝐶)
586518adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝐷𝑁):ℝ⟶ℝ)
587136, 585sseldi 3759 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑦 ∈ ℝ)
58858adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝐶) → 𝑋 ∈ ℝ)
589587, 588resubcld 10712 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝐶) → (𝑦𝑋) ∈ ℝ)
590586, 589ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝐶) → ((𝐷𝑁)‘(𝑦𝑋)) ∈ ℝ)
591583, 584, 585, 590fvmptd 6477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝐶) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦) = ((𝐷𝑁)‘(𝑦𝑋)))
592591fveq2d 6379 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
593592adantlr 706 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) = (abs‘((𝐷𝑁)‘(𝑦𝑋))))
594 simplr 785 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
595132sseli 3757 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐶𝑦 ∈ (-π[,]π))
596595adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → 𝑦 ∈ (-π[,]π))
597 rspa 3077 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
598594, 596, 597syl2anc 579 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
599593, 598eqbrtrd 4831 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
6005993adantl2 1208 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦𝐶) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
601582, 600syldan 585 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) ∧ 𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
602601ex 401 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → (𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) → (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
603575, 602ralrimi 3104 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))))
604 breq2 4813 . . . . . . . . . . . . . 14 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ((abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
605604ralbidv 3133 . . . . . . . . . . . . 13 (𝑏 = (abs‘((𝐷𝑁)‘(𝑐𝑋))) → (∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))))
606605rspcev 3461 . . . . . . . . . . . 12 (((abs‘((𝐷𝑁)‘(𝑐𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
607571, 603, 606syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
608607rexlimdv3a 3180 . . . . . . . . . 10 (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷𝑁)‘(𝑦𝑋))) ≤ (abs‘((𝐷𝑁)‘(𝑐𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏))
609568, 608mpd 15 . . . . . . . . 9 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏)
610 bddmulibl 23896 . . . . . . . . 9 (((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))(abs‘((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
611529, 140, 609, 610syl3anc 1490 . . . . . . . 8 (𝜑 → ((𝑥𝐶 ↦ ((𝐷𝑁)‘(𝑥𝑋))) ∘𝑓 · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
612491, 611eqeltrd 2844 . . . . . . 7 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) ∈ 𝐿1)
613142, 483, 612itgmulc2 23891 . . . . . 6 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
614142adantr 472 . . . . . . . . 9 ((𝜑𝑥𝐶) → π ∈ ℂ)
615120, 488, 614mul13d 40131 . . . . . . . 8 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))))
616489oveq2d 6858 . . . . . . . 8 ((𝜑𝑥𝐶) → (π · (((𝐷𝑁)‘(𝑥𝑋)) · (𝐹𝑥))) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
617615, 616eqtrd 2799 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))))
618617itgeq2dv 23839 . . . . . 6 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋)))) d𝑥)
619613, 618eqtr4d 2802 . . . . 5 (𝜑 → (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) = ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥)
620148adantr 472 . . . . . . . . 9 ((𝜑𝑥𝐶) → (1 / 2) ∈ ℂ)
621620, 120mulcomd 10315 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) = ((𝐹𝑥) · (1 / 2)))
622396an32s 642 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
623474, 120, 622fsummulc2 14800 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))))
624623eqcomd 2771 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) = ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
625621, 624oveq12d 6860 . . . . . . 7 ((𝜑𝑥𝐶) → (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
626474, 622fsumcl 14749 . . . . . . . 8 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))) ∈ ℂ)
627120, 620, 626adddid 10318 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = (((𝐹𝑥) · (1 / 2)) + ((𝐹𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))))
628481oveq1d 6857 . . . . . . . . 9 ((𝜑𝑥𝐶) → (((𝐷𝑁)‘(𝑥𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π))
629620, 626addcld 10313 . . . . . . . . . 10 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) ∈ ℂ)
630629, 614, 479divcan1d 11056 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))))
631628, 630eqtr2d 2800 . . . . . . . 8 ((𝜑𝑥𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋)))) = (((𝐷𝑁)‘(𝑥𝑋)) · π))
632631oveq2d 6858 . . . . . . 7 ((𝜑𝑥𝐶) → ((𝐹𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥𝑋))))) = ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)))
633625, 627, 6323eqtr2rd 2806 . . . . . 6 ((𝜑𝑥𝐶) → ((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) = (((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))))
634633itgeq2dv 23839 . . . . 5 (𝜑 → ∫𝐶((𝐹𝑥) · (((𝐷𝑁)‘(𝑥𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥)
635 remulcl 10274 . . . . . . 7 (((1 / 2) ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
636472, 119, 635sylancr 581 . . . . . 6 ((𝜑𝑥𝐶) → ((1 / 2) · (𝐹𝑥)) ∈ ℝ)
637148, 119, 140iblmulc2 23888 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ ((1 / 2) · (𝐹𝑥))) ∈ 𝐿1)
638391an32s 642 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
639474, 638fsumrecl 14750 . . . . . 6 ((𝜑𝑥𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) ∈ ℝ)
640453simpld 488 . . . . . 6 (𝜑 → (𝑥𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) ∈ 𝐿1)
641636, 637, 639, 640itgadd 23882 . . . . 5 (𝜑 → ∫𝐶(((1 / 2) · (𝐹𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥))
642619, 634, 6413eqtrrd 2804 . . . 4 (𝜑 → (∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) = (π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥))
643642oveq1d 6857 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π))
644636, 637itgcl 23841 . . . 4 (𝜑 → ∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 ∈ ℂ)
645639, 640itgcl 23841 . . . 4 (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 ∈ ℂ)
646644, 645, 142, 102divdird 11093 . . 3 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)))
647483, 612itgcl 23841 . . . 4 (𝜑 → ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥 ∈ ℂ)
648647, 142, 102divcan3d 11060 . . 3 (𝜑 → ((π · ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥) / π) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
649643, 646, 6483eqtr3d 2807 . 2 (𝜑 → ((∫𝐶((1 / 2) · (𝐹𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹𝑥) · (cos‘(𝑛 · (𝑥𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
65090, 458, 6493eqtrd 2803 1 (𝜑 → (𝑆𝑁) = ∫𝐶((𝐹𝑥) · ((𝐷𝑁)‘(𝑥𝑋))) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  wss 3732  ifcif 4243   class class class wbr 4809  cmpt 4888  dom cdm 5277  cres 5279  wf 6064  cfv 6068  (class class class)co 6842  𝑓 cof 7093  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194   < clt 10328  cle 10329  cmin 10520  -cneg 10521   / cdiv 10938  cn 11274  2c2 11327  0cn0 11538  (,)cioo 12377  [,]cicc 12380  ...cfz 12533   mod cmo 12876  abscabs 14259  Σcsu 14701  sincsin 15076  cosccos 15077  πcpi 15079  cnccncf 22958  volcvol 23521  MblFncmbf 23672  𝐿1cibl 23675  citg 23676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cc 9510  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-disj 4778  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-ofr 7096  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-omul 7769  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-acn 9019  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14092  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-limsup 14487  df-clim 14504  df-rlim 14505  df-sum 14702  df-ef 15080  df-sin 15082  df-cos 15083  df-pi 15085  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-sca 16230  df-vsca 16231  df-ip 16232  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-hom 16238  df-cco 16239  df-rest 16349  df-topn 16350  df-0g 16368  df-gsum 16369  df-topgen 16370  df-pt 16371  df-prds 16374  df-xrs 16428  df-qtop 16433  df-imas 16434  df-xps 16436  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-mulg 17808  df-cntz 18013  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-t1 21398  df-haus 21399  df-cmp 21470  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-ovol 23522  df-vol 23523  df-mbf 23677  df-itg1 23678  df-itg2 23679  df-ibl 23680  df-itg 23681  df-0p 23728  df-limc 23921  df-dv 23922
This theorem is referenced by:  fourierdlem111  41071
  Copyright terms: Public domain W3C validator