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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
97 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
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 96 97 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 96 97 150 dvmptres2 ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝑠 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( sin ‘ ( 𝑘 · 𝑠 ) ) / 𝑘 ) ) / π ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) )
152 57 151 eqtrid ⊢ ( 𝜑 → ( ℝ 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 𝑥 = ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) )