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 44905
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 7417 . . . . . 6 (π‘š = 𝑁 β†’ (1...π‘š) = (1...𝑁))
43sumeq1d 15647 . . . . 5 (π‘š = 𝑁 β†’ Σ𝑛 ∈ (1...π‘š)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
54oveq2d 7425 . . . 4 (π‘š = 𝑁 β†’ (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...π‘š)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))) = (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
65adantl 483 . . 3 ((πœ‘ ∧ π‘š = 𝑁) β†’ (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...π‘š)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))) = (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
7 fourierdlem83.n . . 3 (πœ‘ β†’ 𝑁 ∈ β„•)
8 id 22 . . . . . 6 (πœ‘ β†’ πœ‘)
9 0nn0 12487 . . . . . . 7 0 ∈ β„•0
109a1i 11 . . . . . 6 (πœ‘ β†’ 0 ∈ β„•0)
119elexi 3494 . . . . . . 7 0 ∈ V
12 eleq1 2822 . . . . . . . . 9 (𝑛 = 0 β†’ (𝑛 ∈ β„•0 ↔ 0 ∈ β„•0))
1312anbi2d 630 . . . . . . . 8 (𝑛 = 0 β†’ ((πœ‘ ∧ 𝑛 ∈ β„•0) ↔ (πœ‘ ∧ 0 ∈ β„•0)))
14 fveq2 6892 . . . . . . . . 9 (𝑛 = 0 β†’ (π΄β€˜π‘›) = (π΄β€˜0))
1514eleq1d 2819 . . . . . . . 8 (𝑛 = 0 β†’ ((π΄β€˜π‘›) ∈ ℝ ↔ (π΄β€˜0) ∈ ℝ))
1613, 15imbi12d 345 . . . . . . 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 44845 . . . . . . . . 9 (πœ‘ β†’ ((𝑛 ∈ β„•0 β†’ (π΄β€˜π‘›) ∈ ℝ) ∧ (𝑛 ∈ β„• β†’ (π΅β€˜π‘›) ∈ ℝ)))
2322simpld 496 . . . . . . . 8 (πœ‘ β†’ (𝑛 ∈ β„•0 β†’ (π΄β€˜π‘›) ∈ ℝ))
2423imp 408 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π΄β€˜π‘›) ∈ ℝ)
2511, 16, 24vtocl 3550 . . . . . 6 ((πœ‘ ∧ 0 ∈ β„•0) β†’ (π΄β€˜0) ∈ ℝ)
268, 10, 25syl2anc 585 . . . . 5 (πœ‘ β†’ (π΄β€˜0) ∈ ℝ)
2726rehalfcld 12459 . . . 4 (πœ‘ β†’ ((π΄β€˜0) / 2) ∈ ℝ)
28 fzfid 13938 . . . . 5 (πœ‘ β†’ (1...𝑁) ∈ Fin)
29 eleq1 2822 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ (π‘˜ ∈ β„•0 ↔ 𝑛 ∈ β„•0))
3029anbi2d 630 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ ((πœ‘ ∧ π‘˜ ∈ β„•0) ↔ (πœ‘ ∧ 𝑛 ∈ β„•0)))
31 simpl 484 . . . . . . . . . . . . . . . . . 18 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ π‘˜ = 𝑛)
3231oveq1d 7424 . . . . . . . . . . . . . . . . 17 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ (π‘˜ Β· π‘₯) = (𝑛 Β· π‘₯))
3332fveq2d 6896 . . . . . . . . . . . . . . . 16 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(π‘˜ Β· π‘₯)) = (cosβ€˜(𝑛 Β· π‘₯)))
3433oveq2d 7425 . . . . . . . . . . . . . . 15 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))
3534itgeq2dv 25299 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯)
3635eleq1d 2819 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ ↔ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ))
3730, 36imbi12d 345 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ (((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ) ↔ ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)))
3817adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐹:β„βŸΆβ„)
3919adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝐹 β†Ύ 𝐢) ∈ 𝐿1)
40 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
4138, 18, 39, 20, 40fourierdlem16 44839 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π΄β€˜π‘˜) ∈ ℝ ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1) ∧ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ))
4241simprd 497 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ)
4337, 42chvarvv 2003 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
44 pire 25968 . . . . . . . . . . . 12 Ο€ ∈ ℝ
4544a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ Ο€ ∈ ℝ)
46 0re 11216 . . . . . . . . . . . . 13 0 ∈ ℝ
47 pipos 25970 . . . . . . . . . . . . 13 0 < Ο€
4846, 47gtneii 11326 . . . . . . . . . . . 12 Ο€ β‰  0
4948a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ Ο€ β‰  0)
5043, 45, 49redivcld 12042 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
5150, 20fmptd 7114 . . . . . . . . 9 (πœ‘ β†’ 𝐴:β„•0βŸΆβ„)
5251adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐴:β„•0βŸΆβ„)
53 elfznn 13530 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„•)
5453nnnn0d 12532 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„•0)
5554adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ β„•0)
5652, 55ffvelcdmd 7088 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΄β€˜π‘›) ∈ ℝ)
5755nn0red 12533 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ ℝ)
58 fourierdlem83.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
5958adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ ℝ)
6057, 59remulcld 11244 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝑛 Β· 𝑋) ∈ ℝ)
6160recoscld 16087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
6256, 61remulcld 11244 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
63 eleq1 2822 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ (π‘˜ ∈ β„• ↔ 𝑛 ∈ β„•))
6463anbi2d 630 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ ((πœ‘ ∧ π‘˜ ∈ β„•) ↔ (πœ‘ ∧ 𝑛 ∈ β„•)))
65 oveq1 7416 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (π‘˜ Β· π‘₯) = (𝑛 Β· π‘₯))
6665fveq2d 6896 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (sinβ€˜(π‘˜ Β· π‘₯)) = (sinβ€˜(𝑛 Β· π‘₯)))
6766oveq2d 7425 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
6867adantr 482 . . . . . . . . . . . . . . 15 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
6968itgeq2dv 25299 . . . . . . . . . . . . . 14 (π‘˜ = 𝑛 β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯)
7069eleq1d 2819 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ ↔ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ))
7164, 70imbi12d 345 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ (((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ) ↔ ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)))
7217adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„βŸΆβ„)
7319adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝐹 β†Ύ 𝐢) ∈ 𝐿1)
74 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
7572, 18, 73, 21, 74fourierdlem21 44844 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (((π΅β€˜π‘˜) ∈ ℝ ∧ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯)))) ∈ 𝐿1) ∧ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ))
7675simprd 497 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(π‘˜ Β· π‘₯))) dπ‘₯ ∈ ℝ)
7771, 76chvarvv 2003 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
7844a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ ∈ ℝ)
7948a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ο€ β‰  0)
8077, 78, 79redivcld 12042 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
8180, 21fmptd 7114 . . . . . . . . 9 (πœ‘ β†’ 𝐡:β„•βŸΆβ„)
8281adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐡:β„•βŸΆβ„)
8353adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑛 ∈ β„•)
8482, 83ffvelcdmd 7088 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΅β€˜π‘›) ∈ ℝ)
8560resincld 16086 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
8684, 85remulcld 11244 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
8762, 86readdcld 11243 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
8828, 87fsumrecl 15680 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
8927, 88readdcld 11243 . . 3 (πœ‘ β†’ (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))) ∈ ℝ)
902, 6, 7, 89fvmptd 7006 . 2 (πœ‘ β†’ (π‘†β€˜π‘) = (((π΄β€˜0) / 2) + Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
9120a1i 11 . . . . . . 7 (πœ‘ β†’ 𝐴 = (𝑛 ∈ β„•0 ↦ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
92 oveq1 7416 . . . . . . . . . . . . 13 (𝑛 = 0 β†’ (𝑛 Β· π‘₯) = (0 Β· π‘₯))
9392fveq2d 6896 . . . . . . . . . . . 12 (𝑛 = 0 β†’ (cosβ€˜(𝑛 Β· π‘₯)) = (cosβ€˜(0 Β· π‘₯)))
9493oveq2d 7425 . . . . . . . . . . 11 (𝑛 = 0 β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))))
9594adantr 482 . . . . . . . . . 10 ((𝑛 = 0 ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))))
9695itgeq2dv 25299 . . . . . . . . 9 (𝑛 = 0 β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯)
9796adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑛 = 0) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯)
9897oveq1d 7424 . . . . . . 7 ((πœ‘ ∧ 𝑛 = 0) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€))
9917, 18, 19, 20, 10fourierdlem16 44839 . . . . . . . . 9 (πœ‘ β†’ (((π΄β€˜0) ∈ ℝ ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1) ∧ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ ∈ ℝ))
10099simprd 497 . . . . . . . 8 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ ∈ ℝ)
10144a1i 11 . . . . . . . 8 (πœ‘ β†’ Ο€ ∈ ℝ)
10248a1i 11 . . . . . . . 8 (πœ‘ β†’ Ο€ β‰  0)
103100, 101, 102redivcld 12042 . . . . . . 7 (πœ‘ β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
10491, 98, 10, 103fvmptd 7006 . . . . . 6 (πœ‘ β†’ (π΄β€˜0) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€))
105 ioosscn 13386 . . . . . . . . . . . . . . 15 (-Ο€(,)Ο€) βŠ† β„‚
106 id 22 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ 𝐢)
107106, 18eleqtrdi 2844 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ (-Ο€(,)Ο€))
108105, 107sselid 3981 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ β„‚)
109108mul02d 11412 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐢 β†’ (0 Β· π‘₯) = 0)
110109fveq2d 6896 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐢 β†’ (cosβ€˜(0 Β· π‘₯)) = (cosβ€˜0))
111 cos0 16093 . . . . . . . . . . . 12 (cosβ€˜0) = 1
112110, 111eqtrdi 2789 . . . . . . . . . . 11 (π‘₯ ∈ 𝐢 β†’ (cosβ€˜(0 Β· π‘₯)) = 1)
113112oveq2d 7425 . . . . . . . . . 10 (π‘₯ ∈ 𝐢 β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· 1))
114113adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) = ((πΉβ€˜π‘₯) Β· 1))
11517adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐹:β„βŸΆβ„)
116 ioossre 13385 . . . . . . . . . . . . . 14 (-Ο€(,)Ο€) βŠ† ℝ
117116, 107sselid 3981 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ ℝ)
118117adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
119115, 118ffvelcdmd 7088 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
120119recnd 11242 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
121120mulridd 11231 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· 1) = (πΉβ€˜π‘₯))
122114, 121eqtrd 2773 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) = (πΉβ€˜π‘₯))
123122itgeq2dv 25299 . . . . . . 7 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ = ∫𝐢(πΉβ€˜π‘₯) dπ‘₯)
124123oveq1d 7424 . . . . . 6 (πœ‘ β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(0 Β· π‘₯))) dπ‘₯ / Ο€) = (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€))
125104, 124eqtrd 2773 . . . . 5 (πœ‘ β†’ (π΄β€˜0) = (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€))
126125oveq1d 7424 . . . 4 (πœ‘ β†’ ((π΄β€˜0) / 2) = ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€) / 2))
12717feqmptd 6961 . . . . . . . . 9 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)))
128127reseq1d 5981 . . . . . . . 8 (πœ‘ β†’ (𝐹 β†Ύ 𝐢) = ((π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)) β†Ύ 𝐢))
12944a1i 11 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐢 β†’ Ο€ ∈ ℝ)
130129renegcld 11641 . . . . . . . . . . 11 (π‘₯ ∈ 𝐢 β†’ -Ο€ ∈ ℝ)
131 ioossicc 13410 . . . . . . . . . . . . 13 (-Ο€(,)Ο€) βŠ† (-Ο€[,]Ο€)
13218, 131eqsstri 4017 . . . . . . . . . . . 12 𝐢 βŠ† (-Ο€[,]Ο€)
133132sseli 3979 . . . . . . . . . . 11 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ (-Ο€[,]Ο€))
134 eliccre 44218 . . . . . . . . . . 11 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ π‘₯ ∈ ℝ)
135130, 129, 133, 134syl3anc 1372 . . . . . . . . . 10 (π‘₯ ∈ 𝐢 β†’ π‘₯ ∈ ℝ)
136135ssriv 3987 . . . . . . . . 9 𝐢 βŠ† ℝ
137 resmpt 6038 . . . . . . . . 9 (𝐢 βŠ† ℝ β†’ ((π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)) β†Ύ 𝐢) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
138136, 137mp1i 13 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)) β†Ύ 𝐢) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
139128, 138eqtr2d 2774 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (𝐹 β†Ύ 𝐢))
140139, 19eqeltrd 2834 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
141119, 140itgcl 25301 . . . . 5 (πœ‘ β†’ ∫𝐢(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
142101recnd 11242 . . . . 5 (πœ‘ β†’ Ο€ ∈ β„‚)
143 2cnd 12290 . . . . 5 (πœ‘ β†’ 2 ∈ β„‚)
144 2ne0 12316 . . . . . 6 2 β‰  0
145144a1i 11 . . . . 5 (πœ‘ β†’ 2 β‰  0)
146141, 142, 143, 102, 145divdiv32d 12015 . . . 4 (πœ‘ β†’ ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / Ο€) / 2) = ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) / Ο€))
147141, 143, 145divrecd 11993 . . . . . 6 (πœ‘ β†’ (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) = (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ Β· (1 / 2)))
148143, 145reccld 11983 . . . . . . 7 (πœ‘ β†’ (1 / 2) ∈ β„‚)
149141, 148mulcomd 11235 . . . . . 6 (πœ‘ β†’ (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ Β· (1 / 2)) = ((1 / 2) Β· ∫𝐢(πΉβ€˜π‘₯) dπ‘₯))
150148, 119, 140itgmulc2 25351 . . . . . 6 (πœ‘ β†’ ((1 / 2) Β· ∫𝐢(πΉβ€˜π‘₯) dπ‘₯) = ∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯)
151147, 149, 1503eqtrd 2777 . . . . 5 (πœ‘ β†’ (∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) = ∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯)
152151oveq1d 7424 . . . 4 (πœ‘ β†’ ((∫𝐢(πΉβ€˜π‘₯) dπ‘₯ / 2) / Ο€) = (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€))
153126, 146, 1523eqtrd 2777 . . 3 (πœ‘ β†’ ((π΄β€˜0) / 2) = (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€))
15455, 50syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
15520fvmpt2 7010 . . . . . . . . . 10 ((𝑛 ∈ β„•0 ∧ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ) β†’ (π΄β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
15655, 154, 155syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΄β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
157156oveq1d 7424 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) = ((∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (cosβ€˜(𝑛 Β· 𝑋))))
158154recnd 11242 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ β„‚)
15961recnd 11242 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
160158, 159mulcomd 11235 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (cosβ€˜(𝑛 Β· 𝑋))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
16155, 43syldan 592 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
162161recnd 11242 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ β„‚)
163142adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ Ο€ ∈ β„‚)
16448a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ Ο€ β‰  0)
165159, 162, 163, 164divassd 12025 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
16617ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ 𝐹:β„βŸΆβ„)
167117adantl 483 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
168166, 167ffvelcdmd 7088 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
169 nn0re 12481 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„•0 β†’ 𝑛 ∈ ℝ)
170169ad2antlr 726 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
171170, 167remulcld 11244 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ ℝ)
172171recoscld 16087 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
173168, 172remulcld 11244 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
17454, 173sylanl2 680 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
175 ioombl 25082 . . . . . . . . . . . . . . . . . . 19 (-Ο€(,)Ο€) ∈ dom vol
17618, 175eqeltri 2830 . . . . . . . . . . . . . . . . . 18 𝐢 ∈ dom vol
177176elexi 3494 . . . . . . . . . . . . . . . . 17 𝐢 ∈ V
178177a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ 𝐢 ∈ V)
179 eqidd 2734 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))))
180 eqidd 2734 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
181178, 172, 168, 179, 180offval2 7690 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
182172recnd 11242 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
183120adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
184182, 183mulcomd 11235 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•0) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))
185184mpteq2dva 5249 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
186181, 185eqtr2d 2774 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
187 coscn 25957 . . . . . . . . . . . . . . . . . 18 cos ∈ (ℂ–cnβ†’β„‚)
188187a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ cos ∈ (ℂ–cnβ†’β„‚))
189 ax-resscn 11167 . . . . . . . . . . . . . . . . . . . . 21 ℝ βŠ† β„‚
190136, 189sstri 3992 . . . . . . . . . . . . . . . . . . . 20 𝐢 βŠ† β„‚
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ 𝐢 βŠ† β„‚)
192169recnd 11242 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„•0 β†’ 𝑛 ∈ β„‚)
193192adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ 𝑛 ∈ β„‚)
194 ssid 4005 . . . . . . . . . . . . . . . . . . . 20 β„‚ βŠ† β„‚
195194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ β„‚ βŠ† β„‚)
196191, 193, 195constcncfg 44588 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ 𝑛) ∈ (𝐢–cnβ†’β„‚))
197191, 195idcncfg 44589 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ π‘₯) ∈ (𝐢–cnβ†’β„‚))
198196, 197mulcncf 24963 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· π‘₯)) ∈ (𝐢–cnβ†’β„‚))
199188, 198cncfmpt1f 24430 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚))
200 cnmbf 25176 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
201176, 199, 200sylancr 588 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
202140adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
203 1re 11214 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
204 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))))
205169adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
206117adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
207205, 206remulcld 11244 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ ℝ)
208207recoscld 16087 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„•0 ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
209208ralrimiva 3147 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ β„•0 β†’ βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
210209adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
211 dmmptg 6242 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = 𝐢)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = 𝐢)
213204, 212eleqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ 𝐢)
214 eqidd 2734 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))))
215 oveq2 7417 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = 𝑦 β†’ (𝑛 Β· π‘₯) = (𝑛 Β· 𝑦))
216215fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑦 β†’ (cosβ€˜(𝑛 Β· π‘₯)) = (cosβ€˜(𝑛 Β· 𝑦)))
217216adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ (cosβ€˜(𝑛 Β· π‘₯)) = (cosβ€˜(𝑛 Β· 𝑦)))
218 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
219169adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
220136, 218sselid 3981 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
221219, 220remulcld 11244 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (𝑛 Β· 𝑦) ∈ ℝ)
222221recoscld 16087 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· 𝑦)) ∈ ℝ)
223214, 217, 218, 222fvmptd 7006 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦) = (cosβ€˜(𝑛 Β· 𝑦)))
224223fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) = (absβ€˜(cosβ€˜(𝑛 Β· 𝑦))))
225 abscosbd 43988 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 Β· 𝑦) ∈ ℝ β†’ (absβ€˜(cosβ€˜(𝑛 Β· 𝑦))) ≀ 1)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜(cosβ€˜(𝑛 Β· 𝑦))) ≀ 1)
227224, 226eqbrtrd 5171 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
228213, 227syldan 592 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ β„•0 ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
229228ralrimiva 3147 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„•0 β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
230 breq2 5153 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
231230ralbidv 3178 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
232231rspcev 3613 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
233203, 229, 232sylancr 588 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„•0 β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
234233adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
235 bddmulibl 25356 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
236201, 202, 234, 235syl3anc 1372 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
237186, 236eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•0) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
23855, 237syldan 592 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
239159, 174, 238itgmulc2 25351 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) dπ‘₯)
240159adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
241120adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
24254, 182sylanl2 680 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
243240, 241, 242mul12d 11423 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· 𝑋)) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
244240, 242mulcomd 11235 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· (cosβ€˜(𝑛 Β· π‘₯))) = ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))))
245244oveq2d 7425 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· 𝑋)) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))))
246243, 245eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))))
247246itgeq2dv 25299 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
248239, 247eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
249248oveq1d 7424 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((cosβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
250165, 249eqtr3d 2775 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)) = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
251157, 160, 2503eqtrd 2777 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
25283, 80syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ)
25321fvmpt2 7010 . . . . . . . . . 10 ((𝑛 ∈ β„• ∧ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ ℝ) β†’ (π΅β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
25483, 252, 253syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π΅β€˜π‘›) = (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€))
255254oveq1d 7424 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))) = ((∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (sinβ€˜(𝑛 Β· 𝑋))))
256252recnd 11242 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) ∈ β„‚)
25785recnd 11242 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
258256, 257mulcomd 11235 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€) Β· (sinβ€˜(𝑛 Β· 𝑋))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
25983, 77syldan 592 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ ℝ)
260259recnd 11242 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ ∈ β„‚)
261257, 260, 163, 164divassd 12025 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)))
262119adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
263 nnre 12219 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• β†’ 𝑛 ∈ ℝ)
264263adantr 482 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
265117adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
266264, 265remulcld 11244 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ ℝ)
267266resincld 16086 . . . . . . . . . . . . . . 15 ((𝑛 ∈ β„• ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
268267adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
269262, 268remulcld 11244 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
27053, 269sylanl2 680 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) ∈ ℝ)
271177a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐢 ∈ V)
272 eqidd 2734 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))))
273 eqidd 2734 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
274271, 268, 262, 272, 273offval2 7690 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
275268recnd 11242 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
276120adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
277275, 276mulcomd 11235 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
278277mpteq2dva 5249 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
279274, 278eqtr2d 2774 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
280 sincn 25956 . . . . . . . . . . . . . . . . . 18 sin ∈ (ℂ–cnβ†’β„‚)
281280a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sin ∈ (ℂ–cnβ†’β„‚))
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„• β†’ 𝐢 βŠ† β„‚)
283263recnd 11242 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚)
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„• β†’ β„‚ βŠ† β„‚)
285282, 283, 284constcncfg 44588 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ β„• β†’ (π‘₯ ∈ 𝐢 ↦ 𝑛) ∈ (𝐢–cnβ†’β„‚))
286282, 284idcncfg 44589 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ β„• β†’ (π‘₯ ∈ 𝐢 ↦ π‘₯) ∈ (𝐢–cnβ†’β„‚))
287285, 286mulcncf 24963 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· π‘₯)) ∈ (𝐢–cnβ†’β„‚))
288287adantl 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· π‘₯)) ∈ (𝐢–cnβ†’β„‚))
289281, 288cncfmpt1f 24430 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚))
290 cnmbf 25176 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
291176, 289, 290sylancr 588 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ MblFn)
292140adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
293 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))))
294267ralrimiva 3147 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ β„• β†’ βˆ€π‘₯ ∈ 𝐢 (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
295 dmmptg 6242 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘₯ ∈ 𝐢 (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = 𝐢)
296294, 295syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ β„• β†’ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = 𝐢)
297296adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = 𝐢)
298293, 297eleqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ 𝑦 ∈ 𝐢)
299 eqidd 2734 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))))
300215fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑦 β†’ (sinβ€˜(𝑛 Β· π‘₯)) = (sinβ€˜(𝑛 Β· 𝑦)))
301300adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ (sinβ€˜(𝑛 Β· π‘₯)) = (sinβ€˜(𝑛 Β· 𝑦)))
302 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
303263adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
304136, 302sselid 3981 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
305303, 304remulcld 11244 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (𝑛 Β· 𝑦) ∈ ℝ)
306305resincld 16086 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· 𝑦)) ∈ ℝ)
307299, 301, 302, 306fvmptd 7006 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦) = (sinβ€˜(𝑛 Β· 𝑦)))
308307fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) = (absβ€˜(sinβ€˜(𝑛 Β· 𝑦))))
309 abssinbd 44005 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 Β· 𝑦) ∈ ℝ β†’ (absβ€˜(sinβ€˜(𝑛 Β· 𝑦))) ≀ 1)
310305, 309syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜(sinβ€˜(𝑛 Β· 𝑦))) ≀ 1)
311308, 310eqbrtrd 5171 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„• ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
312298, 311syldan 592 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ β„• ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
313312ralrimiva 3147 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„• β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1)
314 breq2 5153 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 1 β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
315314ralbidv 3178 . . . . . . . . . . . . . . . . . 18 (𝑏 = 1 β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1))
316315rspcev 3613 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 1) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
317203, 313, 316sylancr 588 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
318317adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏)
319 bddmulibl 25356 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯)))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
320291, 292, 318, 319syl3anc 1372 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘₯ ∈ 𝐢 ↦ (sinβ€˜(𝑛 Β· π‘₯))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
321279, 320eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
32283, 321syldan 592 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) ∈ 𝐿1)
323257, 270, 322itgmulc2 25351 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) dπ‘₯)
324257adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ β„‚)
32553, 275sylanl2 680 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ β„‚)
326324, 241, 325mul12d 11423 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· 𝑋)) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
327324, 325mulcomd 11235 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· (sinβ€˜(𝑛 Β· π‘₯))) = ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))
328327oveq2d 7425 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· 𝑋)) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
329326, 328eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) = ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
330329itgeq2dv 25299 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))) dπ‘₯ = ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
331323, 330eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯)
332331oveq1d 7424 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((sinβ€˜(𝑛 Β· 𝑋)) Β· ∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯) / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
333261, 332eqtr3d 2775 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· (∫𝐢((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))) dπ‘₯ / Ο€)) = (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
334255, 258, 3333eqtrd 2777 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋))) = (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€))
335251, 334oveq12d 7427 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€) + (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€)))
33654, 168sylanl2 680 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
33755, 208sylan 581 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
33861adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
339337, 338remulcld 11244 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
340336, 339remulcld 11244 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
341241, 242, 240mul13d 43989 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
342242, 241mulcomd 11235 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))
343342oveq2d 7425 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
344341, 343eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) = ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯)))))
345344mpteq2dva 5249 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))))) = (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))))
346159, 174, 238iblmulc2 25348 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· π‘₯))))) ∈ 𝐿1)
347345, 346eqeltrd 2834 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))))) ∈ 𝐿1)
348340, 347itgcl 25301 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ ∈ β„‚)
34983, 267sylan 581 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· π‘₯)) ∈ ℝ)
35085adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (sinβ€˜(𝑛 Β· 𝑋)) ∈ ℝ)
351349, 350remulcld 11244 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))) ∈ ℝ)
352336, 351remulcld 11244 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) ∈ ℝ)
353241, 325, 324mul13d 43989 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))))
354325, 241mulcomd 11235 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))
355354oveq2d 7425 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (πΉβ€˜π‘₯))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
356353, 355eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯)))))
357356mpteq2dva 5249 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) = (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))))
358257, 270, 322iblmulc2 25348 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((sinβ€˜(𝑛 Β· 𝑋)) Β· ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑛 Β· π‘₯))))) ∈ 𝐿1)
359357, 358eqeltrd 2834 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) ∈ 𝐿1)
360352, 359itgcl 25301 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ ∈ β„‚)
361348, 360, 163, 164divdird 12028 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯) / Ο€) = ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€) + (∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ / Ο€)))
36253nncnd 12228 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„‚)
363362ad2antlr 726 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ β„‚)
364108adantl 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ β„‚)
36558recnd 11242 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ β„‚)
366365ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑋 ∈ β„‚)
367363, 364, 366subdid 11670 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· (π‘₯ βˆ’ 𝑋)) = ((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋)))
368367fveq2d 6896 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (cosβ€˜((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋))))
369363, 364mulcld 11234 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· π‘₯) ∈ β„‚)
370363, 366mulcld 11234 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· 𝑋) ∈ β„‚)
371 cossub 16112 . . . . . . . . . . . . 13 (((𝑛 Β· π‘₯) ∈ β„‚ ∧ (𝑛 Β· 𝑋) ∈ β„‚) β†’ (cosβ€˜((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋))) = (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
372369, 370, 371syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜((𝑛 Β· π‘₯) βˆ’ (𝑛 Β· 𝑋))) = (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
373368, 372eqtrd 2773 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))))
374373oveq2d 7425 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = ((πΉβ€˜π‘₯) Β· (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
375339recnd 11242 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) ∈ β„‚)
376351recnd 11242 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))) ∈ β„‚)
377241, 375, 376adddid 11238 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) = (((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
378374, 377eqtrd 2773 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))))
379378itgeq2dv 25299 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = ∫𝐢(((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) dπ‘₯)
380340, 347, 352, 359itgadd 25342 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢(((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) + ((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋))))) dπ‘₯ = (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯))
381379, 380eqtr2d 2774 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯)
382381oveq1d 7424 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((∫𝐢((πΉβ€˜π‘₯) Β· ((cosβ€˜(𝑛 Β· π‘₯)) Β· (cosβ€˜(𝑛 Β· 𝑋)))) dπ‘₯ + ∫𝐢((πΉβ€˜π‘₯) Β· ((sinβ€˜(𝑛 Β· π‘₯)) Β· (sinβ€˜(𝑛 Β· 𝑋)))) dπ‘₯) / Ο€) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
383335, 361, 3823eqtr2d 2779 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = (∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
384383sumeq2dv 15649 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
38557adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
386117adantl 483 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ℝ)
38758ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
388386, 387resubcld 11642 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
389385, 388remulcld 11244 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (𝑛 Β· (π‘₯ βˆ’ 𝑋)) ∈ ℝ)
390389recoscld 16087 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
391336, 390remulcld 11244 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
392177a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝐢 ∈ V)
393 eqidd 2734 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
394 eqidd 2734 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
395392, 390, 336, 393, 394offval2 7690 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) Β· (πΉβ€˜π‘₯))))
396390recnd 11242 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ β„‚)
397396, 241mulcomd 11235 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) β†’ ((cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
398397mpteq2dva 5249 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
399395, 398eqtr2d 2774 . . . . . . 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 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ 𝑋 ∈ β„‚)
405194a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ β„‚ βŠ† β„‚)
406403, 404, 405constcncfg 44588 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ 𝑋) ∈ (𝐢–cnβ†’β„‚))
407402, 406subcncf 24962 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (π‘₯ βˆ’ 𝑋)) ∈ (𝐢–cnβ†’β„‚))
408401, 407mulcncf 24963 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ (𝐢–cnβ†’β„‚))
409400, 408cncfmpt1f 24430 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ (𝐢–cnβ†’β„‚))
410 cnmbf 25176 . . . . . . . . 9 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ MblFn)
411176, 409, 410sylancr 588 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ MblFn)
412140adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
413 simpr 486 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
414390ralrimiva 3147 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
415 dmmptg 6242 . . . . . . . . . . . . . 14 (βˆ€π‘₯ ∈ 𝐢 (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = 𝐢)
416414, 415syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = 𝐢)
417416adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = 𝐢)
418413, 417eleqtrd 2836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ 𝑦 ∈ 𝐢)
419 eqidd 2734 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
420 oveq1 7416 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ (π‘₯ βˆ’ 𝑋) = (𝑦 βˆ’ 𝑋))
421420oveq2d 7425 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ (𝑛 Β· (π‘₯ βˆ’ 𝑋)) = (𝑛 Β· (𝑦 βˆ’ 𝑋)))
422421fveq2d 6896 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))))
423422adantl 483 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) = (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))))
424 simpr 486 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
42557adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑛 ∈ ℝ)
42655, 220sylan 581 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
42758ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
428426, 427resubcld 11642 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 βˆ’ 𝑋) ∈ ℝ)
429425, 428remulcld 11244 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (𝑛 Β· (𝑦 βˆ’ 𝑋)) ∈ ℝ)
430429recoscld 16087 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))) ∈ ℝ)
431419, 423, 424, 430fvmptd 7006 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦) = (cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋))))
432431fveq2d 6896 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) = (absβ€˜(cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋)))))
433 abscosbd 43988 . . . . . . . . . . . . 13 ((𝑛 Β· (𝑦 βˆ’ 𝑋)) ∈ ℝ β†’ (absβ€˜(cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋)))) ≀ 1)
434429, 433syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜(cosβ€˜(𝑛 Β· (𝑦 βˆ’ 𝑋)))) ≀ 1)
435432, 434eqbrtrd 5171 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1)
436418, 435syldan 592 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1)
437436ralrimiva 3147 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1)
438 breq2 5153 . . . . . . . . . . 11 (𝑏 = 1 β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1))
439438ralbidv 3178 . . . . . . . . . 10 (𝑏 = 1 β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1))
440439rspcev 3613 . . . . . . . . 9 ((1 ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 1) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏)
441203, 437, 440sylancr 588 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏)
442 bddmulibl 25356 . . . . . . . 8 (((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))(absβ€˜((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
443411, 412, 441, 442syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ((π‘₯ ∈ 𝐢 ↦ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
444399, 443eqeltrd 2834 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) ∈ 𝐿1)
445391, 444itgcl 25301 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ ∈ β„‚)
44628, 142, 445, 102fsumdivc 15732 . . . 4 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€) = Σ𝑛 ∈ (1...𝑁)(∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
447176a1i 11 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ dom vol)
448 anass 470 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) ↔ (πœ‘ ∧ (𝑛 ∈ (1...𝑁) ∧ π‘₯ ∈ 𝐢)))
449 ancom 462 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ π‘₯ ∈ 𝐢) ↔ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁)))
450449anbi2i 624 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ (1...𝑁) ∧ π‘₯ ∈ 𝐢)) ↔ (πœ‘ ∧ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁))))
451448, 450bitri 275 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) ∧ π‘₯ ∈ 𝐢) ↔ (πœ‘ ∧ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁))))
452451, 391sylbir 234 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝐢 ∧ 𝑛 ∈ (1...𝑁))) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
453447, 28, 452, 444itgfsum 25344 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ 𝐢 ↦ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) ∈ 𝐿1 ∧ βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯))
454453simprd 497 . . . . . 6 (πœ‘ β†’ βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯)
455454eqcomd 2739 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ = βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯)
456455oveq1d 7424 . . . 4 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝑁)∫𝐢((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€) = (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
457384, 446, 4563eqtr2d 2779 . . 3 (πœ‘ β†’ Σ𝑛 ∈ (1...𝑁)(((π΄β€˜π‘›) Β· (cosβ€˜(𝑛 Β· 𝑋))) + ((π΅β€˜π‘›) Β· (sinβ€˜(𝑛 Β· 𝑋)))) = (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€))
458153, 457oveq12d 7427 . 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 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝑁 ∈ β„•)
461 eqid 2733 . . . . . . . . . . 11 (π·β€˜π‘) = (π·β€˜π‘)
462 eqid 2733 . . . . . . . . . . 11 (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€))
463459, 460, 461, 462dirkertrigeq 44817 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (π·β€˜π‘) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€)))
464 oveq2 7417 . . . . . . . . . . . . . . 15 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ (𝑛 Β· 𝑠) = (𝑛 Β· (π‘₯ βˆ’ 𝑋)))
465464fveq2d 6896 . . . . . . . . . . . . . 14 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ (cosβ€˜(𝑛 Β· 𝑠)) = (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))
466465sumeq2sdv 15650 . . . . . . . . . . . . 13 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))
467466oveq2d 7425 . . . . . . . . . . . 12 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
468467oveq1d 7424 . . . . . . . . . . 11 (𝑠 = (π‘₯ βˆ’ 𝑋) β†’ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€))
469468adantl 483 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑠 = (π‘₯ βˆ’ 𝑋)) β†’ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· 𝑠))) / Ο€) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€))
47058adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
471118, 470resubcld 11642 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
472 halfre 12426 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
473472a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (1 / 2) ∈ ℝ)
474 fzfid 13938 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (1...𝑁) ∈ Fin)
475390an32s 651 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
476474, 475fsumrecl 15680 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ ℝ)
477473, 476readdcld 11243 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
47844a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Ο€ ∈ ℝ)
47948a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Ο€ β‰  0)
480477, 478, 479redivcld 12042 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€) ∈ ℝ)
481463, 469, 471, 480fvmptd 7006 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€))
482481, 480eqeltrd 2834 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ)
483119, 482remulcld 11244 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ ℝ)
484177a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ V)
485 eqidd 2734 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
486 eqidd 2734 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) = (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)))
487484, 482, 119, 485, 486offval2 7690 . . . . . . . . 9 (πœ‘ β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))))
488482recnd 11242 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ β„‚)
489488, 120mulcomd 11235 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
490489mpteq2dva 5249 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))) = (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))))
491487, 490eqtr2d 2774 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) = ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))))
492 eqid 2733 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))
493 eqid 2733 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))
494194a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ β„‚ βŠ† β„‚)
495 cncfss 24415 . . . . . . . . . . . . . 14 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (ℝ–cn→ℝ) βŠ† (ℝ–cnβ†’β„‚))
496189, 494, 495sylancr 588 . . . . . . . . . . . . 13 (πœ‘ β†’ (ℝ–cn→ℝ) βŠ† (ℝ–cnβ†’β„‚))
497 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ π‘₯ ∈ ℝ)
49858adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 𝑋 ∈ ℝ)
499497, 498resubcld 11642 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
500 eqid 2733 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) = (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋))
501499, 500fmptd 7114 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)):β„βŸΆβ„)
502189a1i 11 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ℝ βŠ† β„‚)
503502, 494idcncfg 44589 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ π‘₯) ∈ (ℝ–cnβ†’β„‚))
504502, 365, 494constcncfg 44588 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ 𝑋) ∈ (ℝ–cnβ†’β„‚))
505503, 504subcncf 24962 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cnβ†’β„‚))
506 cncfcdm 24414 . . . . . . . . . . . . . . . 16 ((ℝ βŠ† β„‚ ∧ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cnβ†’β„‚)) β†’ ((π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)):β„βŸΆβ„))
507189, 505, 506sylancr 588 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)):β„βŸΆβ„))
508501, 507mpbird 257 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (π‘₯ βˆ’ 𝑋)) ∈ (ℝ–cn→ℝ))
509459dirkercncf 44823 . . . . . . . . . . . . . . 15 (𝑁 ∈ β„• β†’ (π·β€˜π‘) ∈ (ℝ–cn→ℝ))
5107, 509syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π·β€˜π‘) ∈ (ℝ–cn→ℝ))
511508, 510cncfcompt 44599 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (ℝ–cn→ℝ))
512496, 511sseldd 3984 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (ℝ–cnβ†’β„‚))
51344renegcli 11521 . . . . . . . . . . . . . 14 -Ο€ ∈ ℝ
514 iccssre 13406 . . . . . . . . . . . . . 14 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (-Ο€[,]Ο€) βŠ† ℝ)
515513, 44, 514mp2an 691 . . . . . . . . . . . . 13 (-Ο€[,]Ο€) βŠ† ℝ
516515a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (-Ο€[,]Ο€) βŠ† ℝ)
517459dirkerf 44813 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„• β†’ (π·β€˜π‘):β„βŸΆβ„)
5187, 517syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π·β€˜π‘):β„βŸΆβ„)
519518adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ (π·β€˜π‘):β„βŸΆβ„)
520516sselda 3983 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ π‘₯ ∈ ℝ)
52158adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ 𝑋 ∈ ℝ)
522520, 521resubcld 11642 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ (π‘₯ βˆ’ 𝑋) ∈ ℝ)
523519, 522ffvelcdmd 7088 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ)
524523recnd 11242 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ β„‚)
525493, 512, 516, 494, 524cncfmptssg 44587 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
526132a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 βŠ† (-Ο€[,]Ο€))
527492, 525, 526, 494, 488cncfmptssg 44587 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (𝐢–cnβ†’β„‚))
528 cnmbf 25176 . . . . . . . . . 10 ((𝐢 ∈ dom vol ∧ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ (𝐢–cnβ†’β„‚)) β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ MblFn)
529176, 527, 528sylancr 588 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ MblFn)
530513a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ -Ο€ ∈ ℝ)
531 0red 11217 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 0 ∈ ℝ)
532 negpilt0 43990 . . . . . . . . . . . . . . . 16 -Ο€ < 0
533532a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ -Ο€ < 0)
53447a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 0 < Ο€)
535530, 531, 101, 533, 534lttrd 11375 . . . . . . . . . . . . . 14 (πœ‘ β†’ -Ο€ < Ο€)
536530, 101, 535ltled 11362 . . . . . . . . . . . . 13 (πœ‘ β†’ -Ο€ ≀ Ο€)
537493, 512, 516, 502, 523cncfmptssg 44587 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
538530, 101, 536, 537evthiccabs 44209 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ∧ βˆƒπ‘§ ∈ (-Ο€[,]Ο€)βˆ€π‘€ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘§)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘€))))
539538simpld 496 . . . . . . . . . . 11 (πœ‘ β†’ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)))
540 eqidd 2734 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
541420fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
542541adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) ∧ π‘₯ = 𝑦) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
543 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ 𝑦 ∈ (-Ο€[,]Ο€))
544518adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (π·β€˜π‘):β„βŸΆβ„)
545515, 543sselid 3981 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ 𝑦 ∈ ℝ)
54658adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ 𝑋 ∈ ℝ)
547545, 546resubcld 11642 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (𝑦 βˆ’ 𝑋) ∈ ℝ)
548544, 547ffvelcdmd 7088 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)) ∈ ℝ)
549540, 542, 543, 548fvmptd 7006 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ ((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
550549fveq2d 6896 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
551550adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
552 eqidd 2734 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
553 oveq1 7416 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑐 β†’ (π‘₯ βˆ’ 𝑋) = (𝑐 βˆ’ 𝑋))
554553fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑐 β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
555554adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ π‘₯ = 𝑐) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
556 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 𝑐 ∈ (-Ο€[,]Ο€))
557518adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (π·β€˜π‘):β„βŸΆβ„)
558515, 556sselid 3981 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 𝑐 ∈ ℝ)
55958adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 𝑋 ∈ ℝ)
560558, 559resubcld 11642 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (𝑐 βˆ’ 𝑋) ∈ ℝ)
561557, 560ffvelcdmd 7088 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)) ∈ ℝ)
562552, 555, 556, 561fvmptd 7006 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘) = ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
563562fveq2d 6896 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
564563adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
565551, 564breq12d 5162 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ ((absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ↔ (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
566565ralbidva 3176 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ↔ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
567566rexbidva 3177 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π‘₯ ∈ (-Ο€[,]Ο€) ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘)) ↔ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
568539, 567mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
569561recnd 11242 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)) ∈ β„‚)
570569abscld 15383 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∈ ℝ)
5715703adant3 1133 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∈ ℝ)
572 nfv 1918 . . . . . . . . . . . . . 14 β„²π‘¦πœ‘
573 nfv 1918 . . . . . . . . . . . . . 14 Ⅎ𝑦 𝑐 ∈ (-Ο€[,]Ο€)
574 nfra1 3282 . . . . . . . . . . . . . 14 β„²π‘¦βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))
575572, 573, 574nf3an 1905 . . . . . . . . . . . . 13 Ⅎ𝑦(πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
576 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
577482ralrimiva 3147 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐢 ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ)
578 dmmptg 6242 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝐢 ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) ∈ ℝ β†’ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = 𝐢)
579577, 578syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = 𝐢)
580579adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = 𝐢)
581576, 580eleqtrd 2836 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ 𝑦 ∈ 𝐢)
5825813ad2antl1 1186 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ 𝑦 ∈ 𝐢)
583 eqidd 2734 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) = (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))))
584541adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑦 ∈ 𝐢) ∧ π‘₯ = 𝑦) β†’ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
585 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ 𝐢)
586518adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (π·β€˜π‘):β„βŸΆβ„)
587136, 585sselid 3981 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ ℝ)
58858adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ 𝑋 ∈ ℝ)
589587, 588resubcld 11642 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (𝑦 βˆ’ 𝑋) ∈ ℝ)
590586, 589ffvelcdmd 7088 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)) ∈ ℝ)
591583, 584, 585, 590fvmptd 7006 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦) = ((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋)))
592591fveq2d 6896 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
593592adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) = (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))))
594 simplr 768 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
595132sseli 3979 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝐢 β†’ 𝑦 ∈ (-Ο€[,]Ο€))
596595adantl 483 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ 𝑦 ∈ (-Ο€[,]Ο€))
597 rspa 3246 . . . . . . . . . . . . . . . . . 18 ((βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∧ 𝑦 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
598594, 596, 597syl2anc 585 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
599593, 598eqbrtrd 5171 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
6005993adantl2 1168 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ 𝐢) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
601582, 600syldan 592 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) ∧ 𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
602601ex 414 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ (𝑦 ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) β†’ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
603575, 602ralrimi 3255 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))))
604 breq2 5153 . . . . . . . . . . . . . 14 (𝑏 = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) β†’ ((absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏 ↔ (absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
605604ralbidv 3178 . . . . . . . . . . . . 13 (𝑏 = (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) β†’ (βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏 ↔ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))))
606605rspcev 3613 . . . . . . . . . . . 12 (((absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) ∈ ℝ ∧ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏)
607571, 603, 606syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋)))) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏)
608607rexlimdv3a 3160 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜((π·β€˜π‘)β€˜(𝑦 βˆ’ 𝑋))) ≀ (absβ€˜((π·β€˜π‘)β€˜(𝑐 βˆ’ 𝑋))) β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏))
609568, 608mpd 15 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏)
610 bddmulibl 25356 . . . . . . . . 9 (((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∈ MblFn ∧ (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1 ∧ βˆƒπ‘ ∈ ℝ βˆ€π‘¦ ∈ dom (π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))(absβ€˜((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))β€˜π‘¦)) ≀ 𝑏) β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
611529, 140, 609, 610syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝐢 ↦ ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) ∘f Β· (π‘₯ ∈ 𝐢 ↦ (πΉβ€˜π‘₯))) ∈ 𝐿1)
612491, 611eqeltrd 2834 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) ∈ 𝐿1)
613142, 483, 612itgmulc2 25351 . . . . . 6 (πœ‘ β†’ (Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) = ∫𝐢(Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) dπ‘₯)
614142adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Ο€ ∈ β„‚)
615120, 488, 614mul13d 43989 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) = (Ο€ Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))))
616489oveq2d 7425 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (Ο€ Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· (πΉβ€˜π‘₯))) = (Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))))
617615, 616eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) = (Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))))
618617itgeq2dv 25299 . . . . . 6 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) dπ‘₯ = ∫𝐢(Ο€ Β· ((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)))) dπ‘₯)
619613, 618eqtr4d 2776 . . . . 5 (πœ‘ β†’ (Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) = ∫𝐢((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) dπ‘₯)
620148adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (1 / 2) ∈ β„‚)
621620, 120mulcomd 11235 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) Β· (πΉβ€˜π‘₯)) = ((πΉβ€˜π‘₯) Β· (1 / 2)))
622396an32s 651 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑛 ∈ (1...𝑁)) β†’ (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ β„‚)
623474, 120, 622fsummulc2 15730 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
624623eqcomd 2739 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
625621, 624oveq12d 7427 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = (((πΉβ€˜π‘₯) Β· (1 / 2)) + ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
626474, 622fsumcl 15679 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))) ∈ β„‚)
627120, 620, 626adddid 11238 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = (((πΉβ€˜π‘₯) Β· (1 / 2)) + ((πΉβ€˜π‘₯) Β· Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
628481oveq1d 7424 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€) Β· Ο€))
629620, 626addcld 11233 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ β„‚)
630629, 614, 479divcan1d 11991 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) / Ο€) Β· Ο€) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))))
631628, 630eqtr2d 2774 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) = (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€))
632631oveq2d 7425 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) = ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)))
633625, 627, 6323eqtr2rd 2780 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) = (((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))))
634633itgeq2dv 25299 . . . . 5 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· (((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋)) Β· Ο€)) dπ‘₯ = ∫𝐢(((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) dπ‘₯)
635 remulcl 11195 . . . . . . 7 (((1 / 2) ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ℝ) β†’ ((1 / 2) Β· (πΉβ€˜π‘₯)) ∈ ℝ)
636472, 119, 635sylancr 588 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((1 / 2) Β· (πΉβ€˜π‘₯)) ∈ ℝ)
637148, 119, 140iblmulc2 25348 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ ((1 / 2) Β· (πΉβ€˜π‘₯))) ∈ 𝐿1)
638391an32s 651 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
639474, 638fsumrecl 15680 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) ∈ ℝ)
640453simpld 496 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) ∈ 𝐿1)
641636, 637, 639, 640itgadd 25342 . . . . 5 (πœ‘ β†’ ∫𝐢(((1 / 2) Β· (πΉβ€˜π‘₯)) + Σ𝑛 ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋))))) dπ‘₯ = (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯))
642619, 634, 6413eqtrrd 2778 . . . 4 (πœ‘ β†’ (∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯) = (Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯))
643642oveq1d 7424 . . 3 (πœ‘ β†’ ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯) / Ο€) = ((Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) / Ο€))
644636, 637itgcl 25301 . . . 4 (πœ‘ β†’ ∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ ∈ β„‚)
645639, 640itgcl 25301 . . . 4 (πœ‘ β†’ βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ ∈ β„‚)
646644, 645, 142, 102divdird 12028 . . 3 (πœ‘ β†’ ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ + βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯) / Ο€) = ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€) + (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€)))
647483, 612itgcl 25301 . . . 4 (πœ‘ β†’ ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯ ∈ β„‚)
648647, 142, 102divcan3d 11995 . . 3 (πœ‘ β†’ ((Ο€ Β· ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯) / Ο€) = ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯)
649643, 646, 6483eqtr3d 2781 . 2 (πœ‘ β†’ ((∫𝐢((1 / 2) Β· (πΉβ€˜π‘₯)) dπ‘₯ / Ο€) + (βˆ«πΆΞ£π‘› ∈ (1...𝑁)((πΉβ€˜π‘₯) Β· (cosβ€˜(𝑛 Β· (π‘₯ βˆ’ 𝑋)))) dπ‘₯ / Ο€)) = ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯)
65090, 458, 6493eqtrd 2777 1 (πœ‘ β†’ (π‘†β€˜π‘) = ∫𝐢((πΉβ€˜π‘₯) Β· ((π·β€˜π‘)β€˜(π‘₯ βˆ’ 𝑋))) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βŠ† wss 3949  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677   β†Ύ cres 5679  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∘f cof 7668  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444  -cneg 11445   / cdiv 11871  β„•cn 12212  2c2 12267  β„•0cn0 12472  (,)cioo 13324  [,]cicc 13327  ...cfz 13484   mod cmo 13834  abscabs 15181  Ξ£csu 15632  sincsin 16007  cosccos 16008  Ο€cpi 16010  β€“cnβ†’ccncf 24392  volcvol 24980  MblFncmbf 25131  πΏ1cibl 25134  βˆ«citg 25135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cc 10430  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-ofr 7671  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-omul 8471  df-er 8703  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-fi 9406  df-sup 9437  df-inf 9438  df-oi 9505  df-dju 9896  df-card 9934  df-acn 9937  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-ioo 13328  df-ioc 13329  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-fac 14234  df-bc 14263  df-hash 14291  df-shft 15014  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-limsup 15415  df-clim 15432  df-rlim 15433  df-sum 15633  df-ef 16011  df-sin 16013  df-cos 16014  df-pi 16016  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-hom 17221  df-cco 17222  df-rest 17368  df-topn 17369  df-0g 17387  df-gsum 17388  df-topgen 17389  df-pt 17390  df-prds 17393  df-xrs 17448  df-qtop 17453  df-imas 17454  df-xps 17456  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-mulg 18951  df-cntz 19181  df-cmn 19650  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-fbas 20941  df-fg 20942  df-cnfld 20945  df-top 22396  df-topon 22413  df-topsp 22435  df-bases 22449  df-cld 22523  df-ntr 22524  df-cls 22525  df-nei 22602  df-lp 22640  df-perf 22641  df-cn 22731  df-cnp 22732  df-t1 22818  df-haus 22819  df-cmp 22891  df-tx 23066  df-hmeo 23259  df-fil 23350  df-fm 23442  df-flim 23443  df-flf 23444  df-xms 23826  df-ms 23827  df-tms 23828  df-cncf 24394  df-ovol 24981  df-vol 24982  df-mbf 25136  df-itg1 25137  df-itg2 25138  df-ibl 25139  df-itg 25140  df-0p 25187  df-limc 25383  df-dv 25384
This theorem is referenced by:  fourierdlem111  44933
  Copyright terms: Public domain W3C validator