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 45203
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 7419 . . . . . 6 (π‘š = 𝑁 β†’ (1...π‘š) = (1...𝑁))
43sumeq1d 15651 . . . . 5 (π‘š = 𝑁 β†’ Σ𝑛 ∈ (1...π‘š)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
54oveq2d 7427 . . . 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 12491 . . . . . . 7 0 ∈ β„•0
109a1i 11 . . . . . 6 (πœ‘ β†’ 0 ∈ β„•0)
119elexi 3492 . . . . . . 7 0 ∈ V
12 eleq1 2819 . . . . . . . . 9 (𝑛 = 0 β†’ (𝑛 ∈ β„•0 ↔ 0 ∈ β„•0))
1312anbi2d 627 . . . . . . . 8 (𝑛 = 0 β†’ ((πœ‘ ∧ 𝑛 ∈ β„•0) ↔ (πœ‘ ∧ 0 ∈ β„•0)))
14 fveq2 6890 . . . . . . . . 9 (𝑛 = 0 β†’ (π΄β€˜π‘›) = (π΄β€˜0))
1514eleq1d 2816 . . . . . . . 8 (𝑛 = 0 β†’ ((π΄β€˜π‘›) ∈ ℝ ↔ (π΄β€˜0) ∈ ℝ))
1613, 15imbi12d 343 . . . . . . 7 (𝑛 = 0 β†’ (((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π΄β€˜π‘›) ∈ ℝ) ↔ ((πœ‘ ∧ 0 ∈ β„•0) β†’ (π΄β€˜0) ∈ ℝ)))
17 fourierdlem83.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
18 fourierdlem83.c . . . . . . . . . 10 𝐢 = (-Ο€(,)Ο€)
19 fourierdlem83.fl1 . . . . . . . . . 10 (πœ‘ β†’ (𝐹 β†Ύ 𝐢) ∈ 𝐿1)
20 fourierdlem83.a . . . . . . . . . 10 𝐴 = (𝑛 ∈ β„•0 ↦ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
21 fourierdlem83.b . . . . . . . . . 10 𝐡 = (𝑛 ∈ β„• ↦ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
2217, 18, 19, 20, 21fourierdlem22 45143 . . . . . . . . 9 (πœ‘ β†’ ((𝑛 ∈ β„•0 β†’ (π΄β€˜π‘›) ∈ ℝ) ∧ (𝑛 ∈ β„• β†’ (π΅β€˜π‘›) ∈ ℝ)))
2322simpld 493 . . . . . . . 8 (πœ‘ β†’ (𝑛 ∈ β„•0 β†’ (π΄β€˜π‘›) ∈ ℝ))
2423imp 405 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π΄β€˜π‘›) ∈ ℝ)
2511, 16, 24vtocl 3544 . . . . . 6 ((πœ‘ ∧ 0 ∈ β„•0) β†’ (π΄β€˜0) ∈ ℝ)
268, 10, 25syl2anc 582 . . . . 5 (πœ‘ β†’ (π΄β€˜0) ∈ ℝ)
2726rehalfcld 12463 . . . 4 (πœ‘ β†’ ((π΄β€˜0) / 2) ∈ ℝ)
28 fzfid 13942 . . . . 5 (πœ‘ β†’ (1...𝑁) ∈ Fin)
29 eleq1 2819 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ (π‘˜ ∈ β„•0 ↔ 𝑛 ∈ β„•0))
3029anbi2d 627 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ ((πœ‘ ∧ π‘˜ ∈ β„•0) ↔ (πœ‘ ∧ 𝑛 ∈ β„•0)))
31 simpl 481 . . . . . . . . . . . . . . . . . 18 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ π‘˜ = 𝑛)
3231oveq1d 7426 . . . . . . . . . . . . . . . . 17 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ (π‘˜ Β· π‘₯) = (𝑛 Β· π‘₯))
3332fveq2d 6894 . . . . . . . . . . . . . . . 16 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(π‘˜ Β· π‘₯)) = (cosβ€˜(𝑛 Β· π‘₯)))
3433oveq2d 7427 . . . . . . . . . . . . . . 15 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))
3534itgeq2dv 25531 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯)
3635eleq1d 2816 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ ↔ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ))
3730, 36imbi12d 343 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ (((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ) ↔ ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)))
3817adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐹:β„βŸΆβ„)
3919adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝐹 β†Ύ 𝐢) ∈ 𝐿1)
40 simpr 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
4138, 18, 39, 20, 40fourierdlem16 45137 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π΄β€˜π‘˜) ∈ ℝ ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1) ∧ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ))
4241simprd 494 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ)
4337, 42chvarvv 2000 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
44 pire 26204 . . . . . . . . . . . 12 Ο€ ∈ ℝ
4544a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ Ο€ ∈ ℝ)
46 0re 11220 . . . . . . . . . . . . 13 0 ∈ ℝ
47 pipos 26206 . . . . . . . . . . . . 13 0 < Ο€
4846, 47gtneii 11330 . . . . . . . . . . . 12 Ο€ β‰  0
4948a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ Ο€ β‰  0)
5043, 45, 49redivcld 12046 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
5150, 20fmptd 7114 . . . . . . . . 9 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„)
5251adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐴:β„•0βŸΆβ„)
53 elfznn 13534 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„•)
5453nnnn0d 12536 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„•0)
5554adantl 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ β„•0)
5652, 55ffvelcdmd 7086 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΄β€˜π‘›) ∈ ℝ)
5755nn0red 12537 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ ℝ)
58 fourierdlem83.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
5958adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ ℝ)
6057, 59remulcld 11248 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝑛 Β· 𝑋) ∈ ℝ)
6160recoscld 16091 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
6256, 61remulcld 11248 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
63 eleq1 2819 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ (π‘˜ ∈ β„• ↔ 𝑛 ∈ β„•))
6463anbi2d 627 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ ((πœ‘ ∧ π‘˜ ∈ β„•) ↔ (πœ‘ ∧ 𝑛 ∈ β„•)))
65 oveq1 7418 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (π‘˜ Β· π‘₯) = (𝑛 Β· π‘₯))
6665fveq2d 6894 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (sinβ€˜(π‘˜ Β· π‘₯)) = (sinβ€˜(𝑛 Β· π‘₯)))
6766oveq2d 7427 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
6867adantr 479 . . . . . . . . . . . . . . 15 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
6968itgeq2dv 25531 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯)
7069eleq1d 2816 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ ↔ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ))
7164, 70imbi12d 343 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ (((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ) ↔ ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)))
7217adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„βŸΆβ„)
7319adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝐹 β†Ύ 𝐢) ∈ 𝐿1)
74 simpr 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
7572, 18, 73, 21, 74fourierdlem21 45142 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((π΅β€˜π‘˜) ∈ ℝ ∧ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯)))) ∈ 𝐿1) ∧ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ))
7675simprd 494 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ)
7771, 76chvarvv 2000 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
7844a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ ℝ)
7948a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ β‰  0)
8077, 78, 79redivcld 12046 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
8180, 21fmptd 7114 . . . . . . . . 9 (πœ‘ β†’ 𝐡:β„•βŸΆβ„)
8281adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐡:β„•βŸΆβ„)
8353adantl 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ β„•)
8482, 83ffvelcdmd 7086 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΅β€˜π‘›) ∈ ℝ)
8560resincld 16090 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
8684, 85remulcld 11248 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
8762, 86readdcld 11247 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
8828, 87fsumrecl 15684 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
8927, 88readdcld 11247 . . 3 (πœ‘ β†’ (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))) ∈ ℝ)
902, 6, 7, 89fvmptd 7004 . 2 (πœ‘ β†’ (π‘†β€˜π‘) = (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
9120a1i 11 . . . . . . 7 (πœ‘ β†’ 𝐴 = (𝑛 ∈ β„•0 ↦ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
92 oveq1 7418 . . . . . . . . . . . . 13 (𝑛 = 0 β†’ (𝑛 Β· π‘₯) = (0 Β· π‘₯))
9392fveq2d 6894 . . . . . . . . . . . 12 (𝑛 = 0 β†’ (cosβ€˜(𝑛 Β· π‘₯)) = (cosβ€˜(0 Β· π‘₯)))
9493oveq2d 7427 . . . . . . . . . . 11 (𝑛 = 0 β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))))
9594adantr 479 . . . . . . . . . 10 ((𝑛 = 0 ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))))
9695itgeq2dv 25531 . . . . . . . . 9 (𝑛 = 0 β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯)
9796adantl 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 = 0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯)
9897oveq1d 7426 . . . . . . 7 ((πœ‘ ∧ 𝑛 = 0) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€))
9917, 18, 19, 20, 10fourierdlem16 45137 . . . . . . . . 9 (πœ‘ β†’ (((π΄β€˜0) ∈ ℝ ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1) ∧ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ ∈ ℝ))
10099simprd 494 . . . . . . . 8 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ ∈ ℝ)
10144a1i 11 . . . . . . . 8 (πœ‘ β†’ Ο€ ∈ ℝ)
10248a1i 11 . . . . . . . 8 (πœ‘ β†’ Ο€ β‰  0)
103100, 101, 102redivcld 12046 . . . . . . 7 (πœ‘ β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
10491, 98, 10, 103fvmptd 7004 . . . . . 6 (πœ‘ β†’ (π΄β€˜0) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€))
105 ioosscn 13390 . . . . . . . . . . . . . . 15 (-Ο€(,)Ο€) βŠ† β„‚
106 id 22 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ 𝐢)
107106, 18eleqtrdi 2841 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ (-Ο€(,)Ο€))
108105, 107sselid 3979 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ β„‚)
109108mul02d 11416 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐢 β†’ (0 Β· π‘₯) = 0)
110109fveq2d 6894 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐢 β†’ (cosβ€˜(0 Β· π‘₯)) = (cosβ€˜0))
111 cos0 16097 . . . . . . . . . . . 12 (cosβ€˜0) = 1
112110, 111eqtrdi 2786 . . . . . . . . . . 11 (π‘₯ ∈ 𝐢 β†’ (cosβ€˜(0 Β· π‘₯)) = 1)
113112oveq2d 7427 . . . . . . . . . 10 (π‘₯ ∈ 𝐢 β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· 1))
114113adantl 480 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· 1))
11517adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐹:β„βŸΆβ„)
116 ioossre 13389 . . . . . . . . . . . . . 14 (-Ο€(,)Ο€) βŠ† ℝ
117116, 107sselid 3979 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ ℝ)
118117adantl 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
119115, 118ffvelcdmd 7086 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
120119recnd 11246 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
121120mulridd 11235 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· 1) = (πΉβ€˜π‘₯))
122114, 121eqtrd 2770 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) = (πΉβ€˜π‘₯))
123122itgeq2dv 25531 . . . . . . 7 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ = ∫𝐢(πΉβ€˜π‘₯) dπ‘₯)
124123oveq1d 7426 . . . . . 6 (πœ‘ β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€) = (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€))
125104, 124eqtrd 2770 . . . . 5 (πœ‘ β†’ (π΄β€˜0) = (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€))
126125oveq1d 7426 . . . 4 (πœ‘ β†’ ((π΄β€˜0) / 2) = ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€) / 2))
12717feqmptd 6959 . . . . . . . . 9 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)))
128127reseq1d 5979 . . . . . . . 8 (πœ‘ β†’ (𝐹 β†Ύ 𝐢) = ((π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)) β†Ύ 𝐢))
12944a1i 11 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐢 β†’ Ο€ ∈ ℝ)
130129renegcld 11645 . . . . . . . . . . 11 (π‘₯ ∈ 𝐢 β†’ -Ο€ ∈ ℝ)
131 ioossicc 13414 . . . . . . . . . . . . 13 (-Ο€(,)Ο€) βŠ† (-Ο€[,]Ο€)
13218, 131eqsstri 4015 . . . . . . . . . . . 12 𝐢 βŠ† (-Ο€[,]Ο€)
133132sseli 3977 . . . . . . . . . . 11 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ (-Ο€[,]Ο€))
134 eliccre 44516 . . . . . . . . . . 11 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ π‘₯ ∈ ℝ)
135130, 129, 133, 134syl3anc 1369 . . . . . . . . . 10 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ ℝ)
136135ssriv 3985 . . . . . . . . 9 𝐢 βŠ† ℝ
137 resmpt 6036 . . . . . . . . 9 (𝐢 βŠ† ℝ β†’ ((π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)) β†Ύ 𝐢) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
138136, 137mp1i 13 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)) β†Ύ 𝐢) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
139128, 138eqtr2d 2771 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (𝐹 β†Ύ 𝐢))
140139, 19eqeltrd 2831 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
141119, 140itgcl 25533 . . . . 5 (πœ‘ β†’ ∫𝐢(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
142101recnd 11246 . . . . 5 (πœ‘ β†’ Ο€ ∈ β„‚)
143 2cnd 12294 . . . . 5 (πœ‘ β†’ 2 ∈ β„‚)
144 2ne0 12320 . . . . . 6 2 β‰  0
145144a1i 11 . . . . 5 (πœ‘ β†’ 2 β‰  0)
146141, 142, 143, 102, 145divdiv32d 12019 . . . 4 (πœ‘ β†’ ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€) / 2) = ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) / Ο€))
147141, 143, 145divrecd 11997 . . . . . 6 (πœ‘ β†’ (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) = (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ Β· (1 / 2)))
148143, 145reccld 11987 . . . . . . 7 (πœ‘ β†’ (1 / 2) ∈ β„‚)
149141, 148mulcomd 11239 . . . . . 6 (πœ‘ β†’ (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ Β· (1 / 2)) = ((1 / 2) Β· ∫𝐢(πΉβ€˜π‘₯) dπ‘₯))
150148, 119, 140itgmulc2 25583 . . . . . 6 (πœ‘ β†’ ((1 / 2) Β· ∫𝐢(πΉβ€˜π‘₯) dπ‘₯) = ∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯)
151147, 149, 1503eqtrd 2774 . . . . 5 (πœ‘ β†’ (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) = ∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯)
152151oveq1d 7426 . . . 4 (πœ‘ β†’ ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) / Ο€) = (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€))
153126, 146, 1523eqtrd 2774 . . 3 (πœ‘ β†’ ((π΄β€˜0) / 2) = (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€))
15455, 50syldan 589 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
15520fvmpt2 7008 . . . . . . . . . 10 ((𝑛 ∈ β„•0 ∧ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ) β†’ (π΄β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
15655, 154, 155syl2anc 582 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΄β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
157156oveq1d 7426 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) = ((∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (cosβ€˜(𝑛 Β· 𝑋))))
158154recnd 11246 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ β„‚)
15961recnd 11246 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
160158, 159mulcomd 11239 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (cosβ€˜(𝑛 Β· 𝑋))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
16155, 43syldan 589 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
162161recnd 11246 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ β„‚)
163142adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ Ο€ ∈ β„‚)
16448a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ Ο€ β‰  0)
165159, 162, 163, 164divassd 12029 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
16617ad2antrr 722 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ 𝐹:β„βŸΆβ„)
167117adantl 480 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
168166, 167ffvelcdmd 7086 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
169 nn0re 12485 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„•0 β†’ 𝑛 ∈ ℝ)
170169ad2antlr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
171170, 167remulcld 11248 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ ℝ)
172171recoscld 16091 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
173168, 172remulcld 11248 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
17454, 173sylanl2 677 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
175 ioombl 25314 . . . . . . . . . . . . . . . . . . 19 (-Ο€(,)Ο€) ∈ dom vol
17618, 175eqeltri 2827 . . . . . . . . . . . . . . . . . 18 𝐢 ∈ dom vol
177176elexi 3492 . . . . . . . . . . . . . . . . 17 𝐢 ∈ V
178177a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ 𝐢 ∈ V)
179 eqidd 2731 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))))
180 eqidd 2731 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
181178, 172, 168, 179, 180offval2 7692 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
182172recnd 11246 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
183120adantlr 711 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
184182, 183mulcomd 11239 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))
185184mpteq2dva 5247 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
186181, 185eqtr2d 2771 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
187 coscn 26193 . . . . . . . . . . . . . . . . . 18 cos ∈ (ℂ–cnβ†’β„‚)
188187a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ cos ∈ (ℂ–cnβ†’β„‚))
189 ax-resscn 11169 . . . . . . . . . . . . . . . . . . . . 21 ℝ βŠ† β„‚
190136, 189sstri 3990 . . . . . . . . . . . . . . . . . . . 20 𝐢 βŠ† β„‚
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ 𝐢 βŠ† β„‚)
192169recnd 11246 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„•0 β†’ 𝑛 ∈ β„‚)
193192adantl 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ 𝑛 ∈ β„‚)
194 ssid 4003 . . . . . . . . . . . . . . . . . . . 20 β„‚ βŠ† β„‚
195194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ β„‚ βŠ† β„‚)
196191, 193, 195constcncfg 44886 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ 𝑛) ∈ (𝐢–cnβ†’β„‚))
197191, 195idcncfg 44887 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ π‘₯) ∈ (𝐢–cnβ†’β„‚))
198196, 197mulcncf 25194 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· π‘₯)) ∈ (𝐢–cnβ†’β„‚))
199188, 198cncfmpt1f 24654 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚))
200 cnmbf 25408 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
201176, 199, 200sylancr 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
202140adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
203 1re 11218 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
204 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))))
205169adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
206117adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
207205, 206remulcld 11248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ ℝ)
208207recoscld 16091 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
209208ralrimiva 3144 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ β„•0 β†’ βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
210209adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
211 dmmptg 6240 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = 𝐢)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = 𝐢)
213204, 212eleqtrd 2833 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ 𝐢)
214 eqidd 2731 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))))
215 oveq2 7419 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = 𝑦 β†’ (𝑛 Β· π‘₯) = (𝑛 Β· 𝑦))
216215fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑦 β†’ (cosβ€˜(𝑛 Β· π‘₯)) = (cosβ€˜(𝑛 Β· 𝑦)))
217216adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ (cosβ€˜(𝑛 Β· π‘₯)) = (cosβ€˜(𝑛 Β· 𝑦)))
218 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
219169adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
220136, 218sselid 3979 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
221219, 220remulcld 11248 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (𝑛 Β· 𝑦) ∈ ℝ)
222221recoscld 16091 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· 𝑦)) ∈ ℝ)
223214, 217, 218, 222fvmptd 7004 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦) = (cosβ€˜(𝑛 Β· 𝑦)))
224223fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) = (absβ€˜(cosβ€˜(𝑛 Β· 𝑦))))
225 abscosbd 44286 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 Β· 𝑦) ∈ ℝ β†’ (absβ€˜(cosβ€˜(𝑛 Β· 𝑦))) ≀ 1)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜(cosβ€˜(𝑛 Β· 𝑦))) ≀ 1)
227224, 226eqbrtrd 5169 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
228213, 227syldan 589 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
229228ralrimiva 3144 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„•0 β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
230 breq2 5151 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
231230ralbidv 3175 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
232231rspcev 3611 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
233203, 229, 232sylancr 585 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„•0 β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
234233adantl 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
235 bddmulibl 25588 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
236201, 202, 234, 235syl3anc 1369 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
237186, 236eqeltrd 2831 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
23855, 237syldan 589 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
239159, 174, 238itgmulc2 25583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) dπ‘₯)
240159adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
241120adantlr 711 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
24254, 182sylanl2 677 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
243240, 241, 242mul12d 11427 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· 𝑋)) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
244240, 242mulcomd 11239 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· (cosβ€˜(𝑛 Β· π‘₯))) = ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))))
245244oveq2d 7427 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· 𝑋)) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))))
246243, 245eqtrd 2770 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))))
247246itgeq2dv 25531 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
248239, 247eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
249248oveq1d 7426 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
250165, 249eqtr3d 2772 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)) = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
251157, 160, 2503eqtrd 2774 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
25283, 80syldan 589 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
25321fvmpt2 7008 . . . . . . . . . 10 ((𝑛 ∈ β„• ∧ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ) β†’ (π΅β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
25483, 252, 253syl2anc 582 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΅β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
255254oveq1d 7426 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))) = ((∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (sinβ€˜(𝑛 Β· 𝑋))))
256252recnd 11246 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ β„‚)
25785recnd 11246 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
258256, 257mulcomd 11239 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (sinβ€˜(𝑛 Β· 𝑋))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
25983, 77syldan 589 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
260259recnd 11246 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ β„‚)
261257, 260, 163, 164divassd 12029 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
262119adantlr 711 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
263 nnre 12223 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
264263adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
265117adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
266264, 265remulcld 11248 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ ℝ)
267266resincld 16090 . . . . . . . . . . . . . . 15 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
268267adantll 710 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
269262, 268remulcld 11248 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
27053, 269sylanl2 677 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
271177a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐢 ∈ V)
272 eqidd 2731 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))))
273 eqidd 2731 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
274271, 268, 262, 272, 273offval2 7692 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
275268recnd 11246 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
276120adantlr 711 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
277275, 276mulcomd 11239 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
278277mpteq2dva 5247 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
279274, 278eqtr2d 2771 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
280 sincn 26192 . . . . . . . . . . . . . . . . . 18 sin ∈ (ℂ–cnβ†’β„‚)
281280a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sin ∈ (ℂ–cnβ†’β„‚))
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„• β†’ 𝐢 βŠ† β„‚)
283263recnd 11246 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚)
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„• β†’ β„‚ βŠ† β„‚)
285282, 283, 284constcncfg 44886 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ β„• β†’ (π‘₯ ∈ 𝐢 ↦ 𝑛) ∈ (𝐢–cnβ†’β„‚))
286282, 284idcncfg 44887 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ β„• β†’ (π‘₯ ∈ 𝐢 ↦ π‘₯) ∈ (𝐢–cnβ†’β„‚))
287285, 286mulcncf 25194 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· π‘₯)) ∈ (𝐢–cnβ†’β„‚))
288287adantl 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· π‘₯)) ∈ (𝐢–cnβ†’β„‚))
289281, 288cncfmpt1f 24654 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚))
290 cnmbf 25408 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
291176, 289, 290sylancr 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
292140adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
293 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))))
294267ralrimiva 3144 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ β„• β†’ βˆ€π‘₯ ∈ 𝐢 (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
295 dmmptg 6240 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘₯ ∈ 𝐢 (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = 𝐢)
296294, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ β„• β†’ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = 𝐢)
297296adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = 𝐢)
298293, 297eleqtrd 2833 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ 𝐢)
299 eqidd 2731 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))))
300215fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑦 β†’ (sinβ€˜(𝑛 Β· π‘₯)) = (sinβ€˜(𝑛 Β· 𝑦)))
301300adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ (sinβ€˜(𝑛 Β· π‘₯)) = (sinβ€˜(𝑛 Β· 𝑦)))
302 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
303263adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
304136, 302sselid 3979 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
305303, 304remulcld 11248 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (𝑛 Β· 𝑦) ∈ ℝ)
306305resincld 16090 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· 𝑦)) ∈ ℝ)
307299, 301, 302, 306fvmptd 7004 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦) = (sinβ€˜(𝑛 Β· 𝑦)))
308307fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) = (absβ€˜(sinβ€˜(𝑛 Β· 𝑦))))
309 abssinbd 44303 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 Β· 𝑦) ∈ ℝ β†’ (absβ€˜(sinβ€˜(𝑛 Β· 𝑦))) ≀ 1)
310305, 309syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜(sinβ€˜(𝑛 Β· 𝑦))) ≀ 1)
311308, 310eqbrtrd 5169 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
312298, 311syldan 589 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
313312ralrimiva 3144 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„• β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
314 breq2 5151 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
315314ralbidv 3175 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
316315rspcev 3611 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
317203, 313, 316sylancr 585 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
318317adantl 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
319 bddmulibl 25588 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
320291, 292, 318, 319syl3anc 1369 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
321279, 320eqeltrd 2831 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
32283, 321syldan 589 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
323257, 270, 322itgmulc2 25583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) dπ‘₯)
324257adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
32553, 275sylanl2 677 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
326324, 241, 325mul12d 11427 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· 𝑋)) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
327324, 325mulcomd 11239 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· (sinβ€˜(𝑛 Β· π‘₯))) = ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))
328327oveq2d 7427 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· 𝑋)) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
329326, 328eqtrd 2770 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
330329itgeq2dv 25531 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
331323, 330eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
332331oveq1d 7426 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
333261, 332eqtr3d 2772 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)) = (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
334255, 258, 3333eqtrd 2774 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))) = (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
335251, 334oveq12d 7429 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€) + (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€)))
33654, 168sylanl2 677 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
33755, 208sylan 578 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
33861adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
339337, 338remulcld 11248 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
340336, 339remulcld 11248 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
341241, 242, 240mul13d 44287 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
342242, 241mulcomd 11239 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))
343342oveq2d 7427 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
344341, 343eqtrd 2770 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
345344mpteq2dva 5247 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))))) = (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))))
346159, 174, 238iblmulc2 25580 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))) ∈ 𝐿1)
347345, 346eqeltrd 2831 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))))) ∈ 𝐿1)
348340, 347itgcl 25533 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ ∈ β„‚)
34983, 267sylan 578 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
35085adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
351349, 350remulcld 11248 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
352336, 351remulcld 11248 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
353241, 325, 324mul13d 44287 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
354325, 241mulcomd 11239 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
355354oveq2d 7427 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
356353, 355eqtrd 2770 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
357356mpteq2dva 5247 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) = (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))))
358257, 270, 322iblmulc2 25580 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))) ∈ 𝐿1)
359357, 358eqeltrd 2831 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) ∈ 𝐿1)
360352, 359itgcl 25533 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ ∈ β„‚)
361348, 360, 163, 164divdird 12032 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯) / Ο€) = ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€) + (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€)))
36253nncnd 12232 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„‚)
363362ad2antlr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ β„‚)
364108adantl 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ β„‚)
36558recnd 11246 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ β„‚)
366365ad2antrr 722 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑋 ∈ β„‚)
367363, 364, 366subdid 11674 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· (π‘₯ βˆ’ 𝑋)) = ((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋)))
368367fveq2d 6894 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (cosβ€˜((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋))))
369363, 364mulcld 11238 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ β„‚)
370363, 366mulcld 11238 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· 𝑋) ∈ β„‚)
371 cossub 16116 . . . . . . . . . . . . 13 (((𝑛 Β· π‘₯) ∈ β„‚ ∧ (𝑛 Β· 𝑋) ∈ β„‚) β†’ (cosβ€˜((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋))) = (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
372369, 370, 371syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋))) = (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
373368, 372eqtrd 2770 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
374373oveq2d 7427 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = ((πΉβ€˜π‘₯) Β· (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
375339recnd 11246 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) ∈ β„‚)
376351recnd 11246 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))) ∈ β„‚)
377241, 375, 376adddid 11242 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) = (((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
378374, 377eqtrd 2770 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
379378itgeq2dv 25531 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = ∫𝐢(((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) dπ‘₯)
380340, 347, 352, 359itgadd 25574 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢(((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) dπ‘₯ = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯))
381379, 380eqtr2d 2771 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯)
382381oveq1d 7426 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯) / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
383335, 361, 3823eqtr2d 2776 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
384383sumeq2dv 15653 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
38557adantr 479 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
386117adantl 480 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
38758ad2antrr 722 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
388386, 387resubcld 11646 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
389385, 388remulcld 11248 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· (π‘₯ βˆ’ 𝑋)) ∈ ℝ)
390389recoscld 16091 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
391336, 390remulcld 11248 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
392177a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ V)
393 eqidd 2731 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
394 eqidd 2731 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
395392, 390, 336, 393, 394offval2 7692 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) Β· (πΉβ€˜π‘₯))))
396390recnd 11246 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ β„‚)
397396, 241mulcomd 11239 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
398397mpteq2dva 5247 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
399395, 398eqtr2d 2771 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
400187a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ cos ∈ (ℂ–cnβ†’β„‚))
40183, 285syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ 𝑛) ∈ (𝐢–cnβ†’β„‚))
40283, 286syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ π‘₯) ∈ (𝐢–cnβ†’β„‚))
403190a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 βŠ† β„‚)
404365adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
405194a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ β„‚ βŠ† β„‚)
406403, 404, 405constcncfg 44886 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ 𝑋) ∈ (𝐢–cnβ†’β„‚))
407402, 406subcncf 25193 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (π‘₯ βˆ’ 𝑋)) ∈ (𝐢–cnβ†’β„‚))
408401, 407mulcncf 25194 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ (𝐢–cnβ†’β„‚))
409400, 408cncfmpt1f 24654 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ (𝐢–cnβ†’β„‚))
410 cnmbf 25408 . . . . . . . . 9 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ MblFn)
411176, 409, 410sylancr 585 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ MblFn)
412140adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
413 simpr 483 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
414390ralrimiva 3144 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
415 dmmptg 6240 . . . . . . . . . . . . . 14 (βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = 𝐢)
416414, 415syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = 𝐢)
417416adantr 479 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = 𝐢)
418413, 417eleqtrd 2833 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ 𝑦 ∈ 𝐢)
419 eqidd 2731 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
420 oveq1 7418 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ (π‘₯ βˆ’ 𝑋) = (𝑦 βˆ’ 𝑋))
421420oveq2d 7427 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ (𝑛 Β· (π‘₯ βˆ’ 𝑋)) = (𝑛 Β· (𝑦 βˆ’ 𝑋)))
422421fveq2d 6894 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))))
423422adantl 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))))
424 simpr 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
42557adantr 479 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
42655, 220sylan 578 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
42758ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
428426, 427resubcld 11646 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 βˆ’ 𝑋) ∈ ℝ)
429425, 428remulcld 11248 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (𝑛 Β· (𝑦 βˆ’ 𝑋)) ∈ ℝ)
430429recoscld 16091 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))) ∈ ℝ)
431419, 423, 424, 430fvmptd 7004 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦) = (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))))
432431fveq2d 6894 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) = (absβ€˜(cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋)))))
433 abscosbd 44286 . . . . . . . . . . . . 13 ((𝑛 Β· (𝑦 βˆ’ 𝑋)) ∈ ℝ β†’ (absβ€˜(cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋)))) ≀ 1)
434429, 433syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜(cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋)))) ≀ 1)
435432, 434eqbrtrd 5169 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1)
436418, 435syldan 589 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1)
437436ralrimiva 3144 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1)
438 breq2 5151 . . . . . . . . . . 11 (𝑏 = 1 β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1))
439438ralbidv 3175 . . . . . . . . . 10 (𝑏 = 1 β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1))
440439rspcev 3611 . . . . . . . . 9 ((1 ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏)
441203, 437, 440sylancr 585 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏)
442 bddmulibl 25588 . . . . . . . 8 (((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
443411, 412, 441, 442syl3anc 1369 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
444399, 443eqeltrd 2831 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) ∈ 𝐿1)
445391, 444itgcl 25533 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ ∈ β„‚)
44628, 142, 445, 102fsumdivc 15736 . . . 4 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€) = Σ𝑛 ∈ (1...𝑁)(∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
447176a1i 11 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ dom vol)
448 anass 467 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) ↔ (πœ‘ ∧ (𝑛 ∈ (1...𝑁) ∧ π‘₯ ∈ 𝐢)))
449 ancom 459 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ π‘₯ ∈ 𝐢) ↔ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁)))
450449anbi2i 621 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ (1...𝑁) ∧ π‘₯ ∈ 𝐢)) ↔ (πœ‘ ∧ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁))))
451448, 450bitri 274 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) ↔ (πœ‘ ∧ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁))))
452451, 391sylbir 234 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁))) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
453447, 28, 452, 444itgfsum 25576 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ 𝐢 ↦ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) ∈ 𝐿1 ∧ βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯))
454453simprd 494 . . . . . 6 (πœ‘ β†’ βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯)
455454eqcomd 2736 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯)
456455oveq1d 7426 . . . 4 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€) = (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
457384, 446, 4563eqtr2d 2776 . . 3 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
458153, 457oveq12d 7429 . 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 2730 . . . . . . . . . . 11 (π·β€˜π‘) = (π·β€˜π‘)
462 eqid 2730 . . . . . . . . . . 11 (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€))
463459, 460, 461, 462dirkertrigeq 45115 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (π·β€˜π‘) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€)))
464 oveq2 7419 . . . . . . . . . . . . . . 15 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ (𝑛 Β· 𝑠) = (𝑛 Β· (π‘₯ βˆ’ 𝑋)))
465464fveq2d 6894 . . . . . . . . . . . . . 14 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ (cosβ€˜(𝑛 Β· 𝑠)) = (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))
466465sumeq2sdv 15654 . . . . . . . . . . . . 13 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))
467466oveq2d 7427 . . . . . . . . . . . 12 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
468467oveq1d 7426 . . . . . . . . . . 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 11646 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
472 halfre 12430 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
473472a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (1 / 2) ∈ ℝ)
474 fzfid 13942 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (1...𝑁) ∈ Fin)
475390an32s 648 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
476474, 475fsumrecl 15684 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
477473, 476readdcld 11247 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
47844a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Ο€ ∈ ℝ)
47948a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Ο€ β‰  0)
480477, 478, 479redivcld 12046 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€) ∈ ℝ)
481463, 469, 471, 480fvmptd 7004 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€))
482481, 480eqeltrd 2831 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ)
483119, 482remulcld 11248 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ ℝ)
484177a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ V)
485 eqidd 2731 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
486 eqidd 2731 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
487484, 482, 119, 485, 486offval2 7692 . . . . . . . . 9 (πœ‘ β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))))
488482recnd 11246 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ β„‚)
489488, 120mulcomd 11239 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
490489mpteq2dva 5247 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))))
491487, 490eqtr2d 2771 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) = ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
492 eqid 2730 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))
493 eqid 2730 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))
494194a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ β„‚ βŠ† β„‚)
495 cncfss 24639 . . . . . . . . . . . . . 14 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (ℝ–cn→ℝ) βŠ† (ℝ–cnβ†’β„‚))
496189, 494, 495sylancr 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (ℝ–cn→ℝ) βŠ† (ℝ–cnβ†’β„‚))
497 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ π‘₯ ∈ ℝ)
49858adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 𝑋 ∈ ℝ)
499497, 498resubcld 11646 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
500 eqid 2730 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) = (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋))
501499, 500fmptd 7114 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)):β„βŸΆβ„)
502189a1i 11 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ℝ βŠ† β„‚)
503502, 494idcncfg 44887 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ π‘₯) ∈ (ℝ–cnβ†’β„‚))
504502, 365, 494constcncfg 44886 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ 𝑋) ∈ (ℝ–cnβ†’β„‚))
505503, 504subcncf 25193 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cnβ†’β„‚))
506 cncfcdm 24638 . . . . . . . . . . . . . . . 16 ((ℝ βŠ† β„‚ ∧ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cnβ†’β„‚)) β†’ ((π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)):β„βŸΆβ„))
507189, 505, 506sylancr 585 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)):β„βŸΆβ„))
508501, 507mpbird 256 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cn→ℝ))
509459dirkercncf 45121 . . . . . . . . . . . . . . 15 (𝑁 ∈ β„• β†’ (π·β€˜π‘) ∈ (ℝ–cn→ℝ))
5107, 509syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π·β€˜π‘) ∈ (ℝ–cn→ℝ))
511508, 510cncfcompt 44897 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (ℝ–cn→ℝ))
512496, 511sseldd 3982 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (ℝ–cnβ†’β„‚))
51344renegcli 11525 . . . . . . . . . . . . . 14 -Ο€ ∈ ℝ
514 iccssre 13410 . . . . . . . . . . . . . 14 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (-Ο€[,]Ο€) βŠ† ℝ)
515513, 44, 514mp2an 688 . . . . . . . . . . . . 13 (-Ο€[,]Ο€) βŠ† ℝ
516515a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (-Ο€[,]Ο€) βŠ† ℝ)
517459dirkerf 45111 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„• β†’ (π·β€˜π‘):β„βŸΆβ„)
5187, 517syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π·β€˜π‘):β„βŸΆβ„)
519518adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ (π·β€˜π‘):β„βŸΆβ„)
520516sselda 3981 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ π‘₯ ∈ ℝ)
52158adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ 𝑋 ∈ ℝ)
522520, 521resubcld 11646 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
523519, 522ffvelcdmd 7086 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ)
524523recnd 11246 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ β„‚)
525493, 512, 516, 494, 524cncfmptssg 44885 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
526132a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 βŠ† (-Ο€[,]Ο€))
527492, 525, 526, 494, 488cncfmptssg 44885 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (𝐢–cnβ†’β„‚))
528 cnmbf 25408 . . . . . . . . . 10 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ MblFn)
529176, 527, 528sylancr 585 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ MblFn)
530513a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ -Ο€ ∈ ℝ)
531 0red 11221 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 0 ∈ ℝ)
532 negpilt0 44288 . . . . . . . . . . . . . . . 16 -Ο€ < 0
533532a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ -Ο€ < 0)
53447a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 0 < Ο€)
535530, 531, 101, 533, 534lttrd 11379 . . . . . . . . . . . . . 14 (πœ‘ β†’ -Ο€ < Ο€)
536530, 101, 535ltled 11366 . . . . . . . . . . . . 13 (πœ‘ β†’ -Ο€ ≀ Ο€)
537493, 512, 516, 502, 523cncfmptssg 44885 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
538530, 101, 536, 537evthiccabs 44507 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ∧ βˆƒπ‘§ ∈ (-Ο€[,]Ο€)βˆ€π‘€ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘§)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘€))))
539538simpld 493 . . . . . . . . . . 11 (πœ‘ β†’ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)))
540 eqidd 2731 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
541420fveq2d 6894 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
542541adantl 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) ∧ π‘₯ = 𝑦) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
543 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ 𝑦 ∈ (-Ο€[,]Ο€))
544518adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (π·β€˜π‘):β„βŸΆβ„)
545515, 543sselid 3979 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ 𝑦 ∈ ℝ)
54658adantr 479 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ 𝑋 ∈ ℝ)
547545, 546resubcld 11646 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (𝑦 βˆ’ 𝑋) ∈ ℝ)
548544, 547ffvelcdmd 7086 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)) ∈ ℝ)
549540, 542, 543, 548fvmptd 7004 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ ((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
550549fveq2d 6894 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
551550adantlr 711 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
552 eqidd 2731 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
553 oveq1 7418 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑐 β†’ (π‘₯ βˆ’ 𝑋) = (𝑐 βˆ’ 𝑋))
554553fveq2d 6894 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑐 β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
555554adantl 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ π‘₯ = 𝑐) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
556 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 𝑐 ∈ (-Ο€[,]Ο€))
557518adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (π·β€˜π‘):β„βŸΆβ„)
558515, 556sselid 3979 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 𝑐 ∈ ℝ)
55958adantr 479 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 𝑋 ∈ ℝ)
560558, 559resubcld 11646 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (𝑐 βˆ’ 𝑋) ∈ ℝ)
561557, 560ffvelcdmd 7086 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)) ∈ ℝ)
562552, 555, 556, 561fvmptd 7004 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘) = ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
563562fveq2d 6894 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
564563adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
565551, 564breq12d 5160 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ ((absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ↔ (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
566565ralbidva 3173 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ↔ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
567566rexbidva 3174 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ↔ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
568539, 567mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
569561recnd 11246 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)) ∈ β„‚)
570569abscld 15387 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∈ ℝ)
5715703adant3 1130 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∈ ℝ)
572 nfv 1915 . . . . . . . . . . . . . 14 β„²π‘¦πœ‘
573 nfv 1915 . . . . . . . . . . . . . 14 Ⅎ𝑦 𝑐 ∈ (-Ο€[,]Ο€)
574 nfra1 3279 . . . . . . . . . . . . . 14 β„²π‘¦βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
575572, 573, 574nf3an 1902 . . . . . . . . . . . . 13 Ⅎ𝑦(πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
576 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
577482ralrimiva 3144 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐢 ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ)
578 dmmptg 6240 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝐢 ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = 𝐢)
579577, 578syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = 𝐢)
580579adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = 𝐢)
581576, 580eleqtrd 2833 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ 𝑦 ∈ 𝐢)
5825813ad2antl1 1183 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ 𝑦 ∈ 𝐢)
583 eqidd 2731 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
584541adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
585 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
586518adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (π·β€˜π‘):β„βŸΆβ„)
587136, 585sselid 3979 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
58858adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
589587, 588resubcld 11646 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 βˆ’ 𝑋) ∈ ℝ)
590586, 589ffvelcdmd 7086 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)) ∈ ℝ)
591583, 584, 585, 590fvmptd 7004 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
592591fveq2d 6894 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
593592adantlr 711 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
594 simplr 765 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
595132sseli 3977 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝐢 β†’ 𝑦 ∈ (-Ο€[,]Ο€))
596595adantl 480 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ (-Ο€[,]Ο€))
597 rspa 3243 . . . . . . . . . . . . . . . . . 18 ((βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
598594, 596, 597syl2anc 582 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
599593, 598eqbrtrd 5169 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
6005993adantl2 1165 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
601582, 600syldan 589 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
602601ex 411 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ (𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
603575, 602ralrimi 3252 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
604 breq2 5151 . . . . . . . . . . . . . 14 (𝑏 = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
605604ralbidv 3175 . . . . . . . . . . . . 13 (𝑏 = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
606605rspcev 3611 . . . . . . . . . . . 12 (((absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏)
607571, 603, 606syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏)
608607rexlimdv3a 3157 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏))
609568, 608mpd 15 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏)
610 bddmulibl 25588 . . . . . . . . 9 (((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
611529, 140, 609, 610syl3anc 1369 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
612491, 611eqeltrd 2831 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) ∈ 𝐿1)
613142, 483, 612itgmulc2 25583 . . . . . 6 (πœ‘ β†’ (Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) = ∫𝐢(Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) dπ‘₯)
614142adantr 479 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Ο€ ∈ β„‚)
615120, 488, 614mul13d 44287 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) = (Ο€ Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))))
616489oveq2d 7427 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (Ο€ Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))) = (Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))))
617615, 616eqtrd 2770 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) = (Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))))
618617itgeq2dv 25531 . . . . . 6 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) dπ‘₯ = ∫𝐢(Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) dπ‘₯)
619613, 618eqtr4d 2773 . . . . 5 (πœ‘ β†’ (Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) dπ‘₯)
620148adantr 479 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (1 / 2) ∈ β„‚)
621620, 120mulcomd 11239 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (1 / 2)))
622396an32s 648 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ β„‚)
623474, 120, 622fsummulc2 15734 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
624623eqcomd 2736 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
625621, 624oveq12d 7429 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = (((πΉβ€˜π‘₯) Β· (1 / 2)) + ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
626474, 622fsumcl 15683 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ β„‚)
627120, 620, 626adddid 11242 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = (((πΉβ€˜π‘₯) Β· (1 / 2)) + ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
628481oveq1d 7426 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€) Β· Ο€))
629620, 626addcld 11237 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ β„‚)
630629, 614, 479divcan1d 11995 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€) Β· Ο€) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
631628, 630eqtr2d 2771 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€))
632631oveq2d 7427 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)))
633625, 627, 6323eqtr2rd 2777 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) = (((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
634633itgeq2dv 25531 . . . . 5 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) dπ‘₯ = ∫𝐢(((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) dπ‘₯)
635 remulcl 11197 . . . . . . 7 (((1 / 2) ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ℝ) β†’ ((1 / 2) Β· (πΉβ€˜π‘₯)) ∈ ℝ)
636472, 119, 635sylancr 585 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) Β· (πΉβ€˜π‘₯)) ∈ ℝ)
637148, 119, 140iblmulc2 25580 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((1 / 2) Β· (πΉβ€˜π‘₯))) ∈ 𝐿1)
638391an32s 648 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
639474, 638fsumrecl 15684 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
640453simpld 493 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) ∈ 𝐿1)
641636, 637, 639, 640itgadd 25574 . . . . 5 (πœ‘ β†’ ∫𝐢(((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) dπ‘₯ = (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯))
642619, 634, 6413eqtrrd 2775 . . . 4 (πœ‘ β†’ (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯) = (Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯))
643642oveq1d 7426 . . 3 (πœ‘ β†’ ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯) / Ο€) = ((Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) / Ο€))
644636, 637itgcl 25533 . . . 4 (πœ‘ β†’ ∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ ∈ β„‚)
645639, 640itgcl 25533 . . . 4 (πœ‘ β†’ βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ ∈ β„‚)
646644, 645, 142, 102divdird 12032 . . 3 (πœ‘ β†’ ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯) / Ο€) = ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€) + (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€)))
647483, 612itgcl 25533 . . . 4 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯ ∈ β„‚)
648647, 142, 102divcan3d 11999 . . 3 (πœ‘ β†’ ((Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) / Ο€) = ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯)
649643, 646, 6483eqtr3d 2778 . 2 (πœ‘ β†’ ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€) + (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€)) = ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯)
65090, 458, 6493eqtrd 2774 1 (πœ‘ β†’ (π‘†β€˜π‘) = ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βŠ† wss 3947  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675   β†Ύ cres 5677  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ∘f cof 7670  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  -cneg 11449   / cdiv 11875  β„•cn 12216  2c2 12271  β„•0cn0 12476  (,)cioo 13328  [,]cicc 13331  ...cfz 13488   mod cmo 13838  abscabs 15185  Ξ£csu 15636  sincsin 16011  cosccos 16012  Ο€cpi 16014  β€“cnβ†’ccncf 24616  volcvol 25212  MblFncmbf 25363  πΏ1cibl 25366  βˆ«citg 25367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cc 10432  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-ofr 7673  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-omul 8473  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-acn 9939  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-fac 14238  df-bc 14267  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-ef 16015  df-sin 16017  df-cos 16018  df-pi 16020  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-prds 17397  df-xrs 17452  df-qtop 17457  df-imas 17458  df-xps 17460  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18987  df-cntz 19222  df-cmn 19691  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-lp 22860  df-perf 22861  df-cn 22951  df-cnp 22952  df-t1 23038  df-haus 23039  df-cmp 23111  df-tx 23286  df-hmeo 23479  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-xms 24046  df-ms 24047  df-tms 24048  df-cncf 24618  df-ovol 25213  df-vol 25214  df-mbf 25368  df-itg1 25369  df-itg2 25370  df-ibl 25371  df-itg 25372  df-0p 25419  df-limc 25615  df-dv 25616
This theorem is referenced by:  fourierdlem111  45231
  Copyright terms: Public domain W3C validator