Metamath Proof Explorer


Theorem dirkeritg

Description: The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkeritg.d 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ) )
dirkeritg.n ( 𝜑𝑁 ∈ ℕ )
dirkeritg.f 𝐹 = ( 𝐷𝑁 )
dirkeritg.a ( 𝜑𝐴 ∈ ℝ )
dirkeritg.b ( 𝜑𝐵 ∈ ℝ )
dirkeritg.aleb ( 𝜑𝐴𝐵 )
dirkeritg.g 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑥 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) ) / π ) )
Assertion dirkeritg ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑥 ) d 𝑥 = ( ( 𝐺𝐵 ) − ( 𝐺𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dirkeritg.d 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ) )
2 dirkeritg.n ( 𝜑𝑁 ∈ ℕ )
3 dirkeritg.f 𝐹 = ( 𝐷𝑁 )
4 dirkeritg.a ( 𝜑𝐴 ∈ ℝ )
5 dirkeritg.b ( 𝜑𝐵 ∈ ℝ )
6 dirkeritg.aleb ( 𝜑𝐴𝐵 )
7 dirkeritg.g 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑥 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) ) / π ) )
8 fveq2 ( 𝑥 = 𝑠 → ( 𝐹𝑥 ) = ( 𝐹𝑠 ) )
9 8 cbvitgv ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑠 ) d 𝑠
10 9 a1i ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑠 ) d 𝑠 )
11 elioore ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
12 11 adantl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
13 halfre ( 1 / 2 ) ∈ ℝ
14 13 a1i ( 𝑠 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
15 fzfid ( 𝑠 ∈ ℝ → ( 1 ... 𝑁 ) ∈ Fin )
16 elfzelz ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
17 16 zred ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℝ )
18 17 adantl ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
19 simpl ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℝ )
20 18 19 remulcld ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · 𝑠 ) ∈ ℝ )
21 20 recoscld ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℝ )
22 15 21 fsumrecl ( 𝑠 ∈ ℝ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℝ )
23 14 22 readdcld ( 𝑠 ∈ ℝ → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℝ )
24 pire π ∈ ℝ
25 24 a1i ( 𝑠 ∈ ℝ → π ∈ ℝ )
26 pipos 0 < π
27 24 26 gt0ne0ii π ≠ 0
28 27 a1i ( 𝑠 ∈ ℝ → π ≠ 0 )
29 23 25 28 redivcld ( 𝑠 ∈ ℝ → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ∈ ℝ )
30 12 29 syl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ∈ ℝ )
31 eqid ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
32 31 fvmpt2 ( ( 𝑠 ∈ ℝ ∧ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ∈ ℝ ) → ( ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ‘ 𝑠 ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
33 12 30 32 syl2anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ‘ 𝑠 ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
34 oveq1 ( 𝑥 = 𝑠 → ( 𝑥 mod ( 2 · π ) ) = ( 𝑠 mod ( 2 · π ) ) )
35 34 eqeq1d ( 𝑥 = 𝑠 → ( ( 𝑥 mod ( 2 · π ) ) = 0 ↔ ( 𝑠 mod ( 2 · π ) ) = 0 ) )
36 oveq2 ( 𝑥 = 𝑠 → ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) = ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) )
37 36 fveq2d ( 𝑥 = 𝑠 → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
38 oveq1 ( 𝑥 = 𝑠 → ( 𝑥 / 2 ) = ( 𝑠 / 2 ) )
39 38 fveq2d ( 𝑥 = 𝑠 → ( sin ‘ ( 𝑥 / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
40 39 oveq2d ( 𝑥 = 𝑠 → ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) )
41 37 40 oveq12d ( 𝑥 = 𝑠 → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
42 35 41 ifbieq2d ( 𝑥 = 𝑠 → if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
43 42 cbvmptv ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
44 43 mpteq2i ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
45 1 44 eqtri 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
46 45 2 3 31 dirkertrigeq ( 𝜑𝐹 = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) )
47 46 fveq1d ( 𝜑 → ( 𝐹𝑠 ) = ( ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ‘ 𝑠 ) )
48 47 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹𝑠 ) = ( ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ‘ 𝑠 ) )
49 oveq2 ( 𝑥 = 𝑠 → ( 𝑘 · 𝑥 ) = ( 𝑘 · 𝑠 ) )
50 49 fveq2d ( 𝑥 = 𝑠 → ( sin ‘ ( 𝑘 · 𝑥 ) ) = ( sin ‘ ( 𝑘 · 𝑠 ) ) )
51 50 oveq1d ( 𝑥 = 𝑠 → ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) = ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) )
52 51 sumeq2sdv ( 𝑥 = 𝑠 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) )
53 38 52 oveq12d ( 𝑥 = 𝑠 → ( ( 𝑥 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) ) = ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) )
54 53 oveq1d ( 𝑥 = 𝑠 → ( ( ( 𝑥 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) ) / π ) = ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) )
55 54 cbvmptv ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑥 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑥 ) ) / 𝑘 ) ) / π ) ) = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) )
56 7 55 eqtri 𝐺 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) )
57 56 oveq2i ( ℝ D 𝐺 ) = ( ℝ D ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ) )
58 reelprrecn ℝ ∈ { ℝ , ℂ }
59 58 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
60 recn ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
61 60 halfcld ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) ∈ ℂ )
62 16 zcnd ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
63 62 adantl ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
64 60 adantr ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
65 63 64 mulcld ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · 𝑠 ) ∈ ℂ )
66 65 sincld ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( sin ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
67 0red ( 𝑘 ∈ ( 1 ... 𝑁 ) → 0 ∈ ℝ )
68 1red ( 𝑘 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℝ )
69 0lt1 0 < 1
70 69 a1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → 0 < 1 )
71 elfzle1 ( 𝑘 ∈ ( 1 ... 𝑁 ) → 1 ≤ 𝑘 )
72 67 68 17 70 71 ltletrd ( 𝑘 ∈ ( 1 ... 𝑁 ) → 0 < 𝑘 )
73 72 gt0ne0d ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ≠ 0 )
74 73 adantl ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ≠ 0 )
75 66 63 74 divcld ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ∈ ℂ )
76 15 75 fsumcl ( 𝑠 ∈ ℝ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ∈ ℂ )
77 61 76 addcld ( 𝑠 ∈ ℝ → ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ∈ ℂ )
78 picn π ∈ ℂ
79 78 a1i ( 𝑠 ∈ ℝ → π ∈ ℂ )
80 77 79 28 divcld ( 𝑠 ∈ ℝ → ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ∈ ℂ )
81 80 adantl ( ( 𝜑𝑠 ∈ ℝ ) → ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ∈ ℂ )
82 29 adantl ( ( 𝜑𝑠 ∈ ℝ ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ∈ ℝ )
83 77 adantl ( ( 𝜑𝑠 ∈ ℝ ) → ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ∈ ℂ )
84 23 adantl ( ( 𝜑𝑠 ∈ ℝ ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℝ )
85 61 adantl ( ( 𝜑𝑠 ∈ ℝ ) → ( 𝑠 / 2 ) ∈ ℂ )
86 13 a1i ( ( 𝜑𝑠 ∈ ℝ ) → ( 1 / 2 ) ∈ ℝ )
87 60 adantl ( ( 𝜑𝑠 ∈ ℝ ) → 𝑠 ∈ ℂ )
88 1red ( ( 𝜑𝑠 ∈ ℝ ) → 1 ∈ ℝ )
89 59 dvmptid ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ 1 ) )
90 2cnd ( 𝜑 → 2 ∈ ℂ )
91 2ne0 2 ≠ 0
92 91 a1i ( 𝜑 → 2 ≠ 0 )
93 59 87 88 89 90 92 dvmptdivc ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 𝑠 / 2 ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 1 / 2 ) ) )
94 76 adantl ( ( 𝜑𝑠 ∈ ℝ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ∈ ℂ )
95 22 adantl ( ( 𝜑𝑠 ∈ ℝ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℝ )
96 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
97 96 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
98 reopn ℝ ∈ ( topGen ‘ ran (,) )
99 98 a1i ( 𝜑 → ℝ ∈ ( topGen ‘ ran (,) ) )
100 fzfid ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
101 75 ancoms ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ∈ ℂ )
102 101 3adant1 ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ∈ ℂ )
103 21 ancoms ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℝ )
104 103 recnd ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
105 104 3adant1 ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
106 58 a1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → ℝ ∈ { ℝ , ℂ } )
107 66 ancoms ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( sin ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
108 62 adantr ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℂ ) → 𝑘 ∈ ℂ )
109 simpr ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℂ ) → 𝑠 ∈ ℂ )
110 108 109 mulcld ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℂ ) → ( 𝑘 · 𝑠 ) ∈ ℂ )
111 110 coscld ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℂ ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
112 108 111 mulcld ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℂ ) → ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℂ )
113 60 112 sylan2 ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℂ )
114 ax-resscn ℝ ⊆ ℂ
115 resmpt ( ℝ ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) )
116 114 115 mp1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) )
117 116 eqcomd ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ℝ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ↾ ℝ ) )
118 117 oveq2d ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ↾ ℝ ) ) )
119 110 sincld ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℂ ) → ( sin ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
120 119 fmpttd ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) : ℂ ⟶ ℂ )
121 112 ralrimiva ( 𝑘 ∈ ( 1 ... 𝑁 ) → ∀ 𝑠 ∈ ℂ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℂ )
122 dmmptg ( ∀ 𝑠 ∈ ℂ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℂ → dom ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) = ℂ )
123 121 122 syl ( 𝑘 ∈ ( 1 ... 𝑁 ) → dom ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) = ℂ )
124 114 123 sseqtrrid ( 𝑘 ∈ ( 1 ... 𝑁 ) → ℝ ⊆ dom ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
125 dvsinax ( 𝑘 ∈ ℂ → ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
126 62 125 syl ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
127 126 dmeqd ( 𝑘 ∈ ( 1 ... 𝑁 ) → dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) = dom ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
128 124 127 sseqtrrd ( 𝑘 ∈ ( 1 ... 𝑁 ) → ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) )
129 dvcnre ( ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) ) → ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) )
130 120 128 129 syl2anc ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) )
131 126 reseq1d ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) = ( ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) )
132 resmpt ( ℝ ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
133 114 132 ax-mp ( ( 𝑠 ∈ ℂ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) )
134 131 133 eqtrdi ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
135 118 130 134 3eqtrd ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
136 106 107 113 135 62 73 dvmptdivc ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / 𝑘 ) ) )
137 62 adantr ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → 𝑘 ∈ ℂ )
138 73 adantr ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → 𝑘 ≠ 0 )
139 104 137 138 divcan3d ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ℝ ) → ( ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / 𝑘 ) = ( cos ‘ ( 𝑘 · 𝑠 ) ) )
140 139 mpteq2dva ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝑘 · ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / 𝑘 ) ) = ( 𝑠 ∈ ℝ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) )
141 136 140 eqtrd ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ) = ( 𝑠 ∈ ℝ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) )
142 141 adantl ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ) = ( 𝑠 ∈ ℝ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) )
143 97 96 59 99 100 102 105 142 dvmptfsum ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ) = ( 𝑠 ∈ ℝ ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) )
144 59 85 86 93 94 95 143 dvmptadd ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) )
145 78 a1i ( 𝜑 → π ∈ ℂ )
146 27 a1i ( 𝜑 → π ≠ 0 )
147 59 83 84 144 145 146 dvmptdivc ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ) ) = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) )
148 4 5 iccssred ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
149 iccntr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
150 4 5 149 syl2anc ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
151 59 81 82 147 148 97 96 150 dvmptres2 ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) )
152 57 151 syl5eq ( 𝜑 → ( ℝ D 𝐺 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) )
153 152 30 fvmpt2d ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑠 ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
154 33 48 153 3eqtr4d ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹𝑠 ) = ( ( ℝ D 𝐺 ) ‘ 𝑠 ) )
155 154 itgeq2dv ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐺 ) ‘ 𝑠 ) d 𝑠 )
156 ioosscn ( 𝐴 (,) 𝐵 ) ⊆ ℂ
157 156 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
158 halfcn ( 1 / 2 ) ∈ ℂ
159 158 a1i ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
160 ssid ℂ ⊆ ℂ
161 160 a1i ( 𝜑 → ℂ ⊆ ℂ )
162 157 159 161 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 2 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
163 eqid ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) )
164 coscn cos ∈ ( ℂ –cn→ ℂ )
165 164 a1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → cos ∈ ( ℂ –cn→ ℂ ) )
166 eqid ( 𝑠 ∈ ℂ ↦ ( 𝑘 · 𝑠 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑘 · 𝑠 ) )
167 166 mulc1cncf ( 𝑘 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 𝑘 · 𝑠 ) ) ∈ ( ℂ –cn→ ℂ ) )
168 62 167 syl ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ℂ ↦ ( 𝑘 · 𝑠 ) ) ∈ ( ℂ –cn→ ℂ ) )
169 165 168 cncfmpt1f ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
170 156 a1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
171 160 a1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → ℂ ⊆ ℂ )
172 11 104 sylan2 ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
173 163 169 170 171 172 cncfmptssg ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
174 173 adantl ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
175 157 100 174 fsumcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
176 162 175 addcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
177 eqid ( 𝑠 ∈ ℂ ↦ π ) = ( 𝑠 ∈ ℂ ↦ π )
178 cncfmptc ( ( π ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑠 ∈ ℂ ↦ π ) ∈ ( ℂ –cn→ ℂ ) )
179 78 160 160 178 mp3an ( 𝑠 ∈ ℂ ↦ π ) ∈ ( ℂ –cn→ ℂ )
180 179 a1i ( 𝜑 → ( 𝑠 ∈ ℂ ↦ π ) ∈ ( ℂ –cn→ ℂ ) )
181 difssd ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
182 eldifsn ( π ∈ ( ℂ ∖ { 0 } ) ↔ ( π ∈ ℂ ∧ π ≠ 0 ) )
183 78 27 182 mpbir2an π ∈ ( ℂ ∖ { 0 } )
184 183 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → π ∈ ( ℂ ∖ { 0 } ) )
185 177 180 157 181 184 cncfmptssg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ π ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
186 176 185 divcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
187 152 186 eqeltrd ( 𝜑 → ( ℝ D 𝐺 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
188 ioossicc ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
189 188 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
190 ioombl ( 𝐴 (,) 𝐵 ) ∈ dom vol
191 190 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
192 13 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 1 / 2 ) ∈ ℝ )
193 fzfid ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
194 17 adantl ( ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
195 148 sselda ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℝ )
196 195 adantr ( ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℝ )
197 194 196 remulcld ( ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · 𝑠 ) ∈ ℝ )
198 197 recoscld ( ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℝ )
199 193 198 fsumrecl ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℝ )
200 192 199 readdcld ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ℝ )
201 24 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → π ∈ ℝ )
202 27 a1i ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → π ≠ 0 )
203 200 201 202 redivcld ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ∈ ℝ )
204 148 114 sstrdi ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
205 204 159 161 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 1 / 2 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
206 eqid ( 𝑠 ∈ ℂ ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( 𝑠 ∈ ℂ ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) )
207 169 adantl ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
208 161 100 207 fsumcncf ( 𝜑 → ( 𝑠 ∈ ℂ ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
209 199 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
210 206 208 204 161 209 cncfmptssg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
211 205 210 addcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
212 183 a1i ( 𝜑 → π ∈ ( ℂ ∖ { 0 } ) )
213 204 212 181 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ π ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
214 211 213 divcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
215 cniccibl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ∈ 𝐿1 )
216 4 5 214 215 syl3anc ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ∈ 𝐿1 )
217 189 191 203 216 iblss ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) ∈ 𝐿1 )
218 152 217 eqeltrd ( 𝜑 → ( ℝ D 𝐺 ) ∈ 𝐿1 )
219 204 161 idcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑠 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
220 2cn 2 ∈ ℂ
221 eldifsn ( 2 ∈ ( ℂ ∖ { 0 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
222 220 91 221 mpbir2an 2 ∈ ( ℂ ∖ { 0 } )
223 222 a1i ( 𝜑 → 2 ∈ ( ℂ ∖ { 0 } ) )
224 204 223 181 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ 2 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
225 219 224 divcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑠 / 2 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
226 eqid ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) = ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) )
227 sincn sin ∈ ( ℂ –cn→ ℂ )
228 227 a1i ( 𝑘 ∈ ( 1 ... 𝑁 ) → sin ∈ ( ℂ –cn→ ℂ ) )
229 228 168 cncfmpt1f ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
230 229 adantl ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 ∈ ℂ ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
231 204 adantr ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
232 160 a1i ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ℂ ⊆ ℂ )
233 62 ad2antlr ( ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑘 ∈ ℂ )
234 195 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℂ )
235 234 adantlr ( ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℂ )
236 233 235 mulcld ( ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑘 · 𝑠 ) ∈ ℂ )
237 236 sincld ( ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ ( 𝑘 · 𝑠 ) ) ∈ ℂ )
238 226 230 231 232 237 cncfmptssg ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( sin ‘ ( 𝑘 · 𝑠 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
239 eldifsn ( 𝑘 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
240 62 73 239 sylanbrc ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ( ℂ ∖ { 0 } ) )
241 240 adantl ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ( ℂ ∖ { 0 } ) )
242 difssd ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ℂ ∖ { 0 } ) ⊆ ℂ )
243 231 241 242 constcncfg ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑘 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
244 238 243 divcncf ( ( 𝜑𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
245 204 100 244 fsumcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
246 225 245 addcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
247 246 213 divcncf ( 𝜑 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
248 56 247 eqeltrid ( 𝜑𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
249 4 5 6 187 218 248 ftc2 ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐺 ) ‘ 𝑠 ) d 𝑠 = ( ( 𝐺𝐵 ) − ( 𝐺𝐴 ) ) )
250 10 155 249 3eqtrd ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹𝑥 ) d 𝑥 = ( ( 𝐺𝐵 ) − ( 𝐺𝐴 ) ) )