Metamath Proof Explorer


Theorem dirkertrigeq

Description: Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeq.d 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
dirkertrigeq.n ( 𝜑𝑁 ∈ ℕ )
dirkertrigeq.f 𝐹 = ( 𝐷𝑁 )
dirkertrigeq.h 𝐻 = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
Assertion dirkertrigeq ( 𝜑𝐹 = 𝐻 )

Proof

Step Hyp Ref Expression
1 dirkertrigeq.d 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2 dirkertrigeq.n ( 𝜑𝑁 ∈ ℕ )
3 dirkertrigeq.f 𝐹 = ( 𝐷𝑁 )
4 dirkertrigeq.h 𝐻 = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
5 3 a1i ( 𝜑𝐹 = ( 𝐷𝑁 ) )
6 1 dirkerval ( 𝑁 ∈ ℕ → ( 𝐷𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
7 2 6 syl ( 𝜑 → ( 𝐷𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
8 2cnd ( 𝜑 → 2 ∈ ℂ )
9 2 nncnd ( 𝜑𝑁 ∈ ℂ )
10 8 9 mulcld ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
11 peano2cn ( ( 2 · 𝑁 ) ∈ ℂ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
12 10 11 syl ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
13 picn π ∈ ℂ
14 13 a1i ( 𝜑 → π ∈ ℂ )
15 2ne0 2 ≠ 0
16 15 a1i ( 𝜑 → 2 ≠ 0 )
17 pire π ∈ ℝ
18 pipos 0 < π
19 17 18 gt0ne0ii π ≠ 0
20 19 a1i ( 𝜑 → π ≠ 0 )
21 12 8 14 16 20 divdiv1d ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
22 21 eqcomd ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
23 22 ad2antrr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
24 iftrue ( ( 𝑠 mod ( 2 · π ) ) = 0 → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
25 24 adantl ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
26 elfzelz ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
27 26 zcnd ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
28 27 adantl ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
29 recn ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
30 29 ad2antrr ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
31 2cn 2 ∈ ℂ
32 31 13 mulcli ( 2 · π ) ∈ ℂ
33 32 a1i ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 · π ) ∈ ℂ )
34 31 13 15 19 mulne0i ( 2 · π ) ≠ 0
35 34 a1i ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 · π ) ≠ 0 )
36 28 30 33 35 divassd ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) = ( 𝑘 · ( 𝑠 / ( 2 · π ) ) ) )
37 26 adantl ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
38 simpr ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 mod ( 2 · π ) ) = 0 )
39 simpl ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → 𝑠 ∈ ℝ )
40 2rp 2 ∈ ℝ+
41 pirp π ∈ ℝ+
42 rpmulcl ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
43 40 41 42 mp2an ( 2 · π ) ∈ ℝ+
44 mod0 ( ( 𝑠 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑠 mod ( 2 · π ) ) = 0 ↔ ( 𝑠 / ( 2 · π ) ) ∈ ℤ ) )
45 39 43 44 sylancl ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 𝑠 mod ( 2 · π ) ) = 0 ↔ ( 𝑠 / ( 2 · π ) ) ∈ ℤ ) )
46 38 45 mpbid ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 / ( 2 · π ) ) ∈ ℤ )
47 46 adantr ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 / ( 2 · π ) ) ∈ ℤ )
48 37 47 zmulcld ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · ( 𝑠 / ( 2 · π ) ) ) ∈ ℤ )
49 36 48 eqeltrd ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ )
50 27 adantl ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
51 29 adantr ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
52 50 51 mulcld ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · 𝑠 ) ∈ ℂ )
53 coseq1 ( ( 𝑘 · 𝑠 ) ∈ ℂ → ( ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 ↔ ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ ) )
54 52 53 syl ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 ↔ ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ ) )
55 54 adantlr ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 ↔ ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ ) )
56 49 55 mpbird ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 )
57 56 ralrimiva ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 )
58 57 adantll ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 )
59 58 sumeq2d ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 )
60 fzfid ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 1 ... 𝑁 ) ∈ Fin )
61 1cnd ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → 1 ∈ ℂ )
62 fsumconst ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) )
63 60 61 62 syl2anc ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) )
64 2 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
65 hashfz1 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
66 64 65 syl ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
67 66 oveq1d ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) = ( 𝑁 · 1 ) )
68 9 mulid1d ( 𝜑 → ( 𝑁 · 1 ) = 𝑁 )
69 67 68 eqtrd ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) = 𝑁 )
70 69 ad2antrr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) = 𝑁 )
71 59 63 70 3eqtrd ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = 𝑁 )
72 71 oveq2d ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( 1 / 2 ) + 𝑁 ) )
73 9 div1d ( 𝜑 → ( 𝑁 / 1 ) = 𝑁 )
74 73 eqcomd ( 𝜑𝑁 = ( 𝑁 / 1 ) )
75 74 oveq2d ( 𝜑 → ( ( 1 / 2 ) + 𝑁 ) = ( ( 1 / 2 ) + ( 𝑁 / 1 ) ) )
76 1cnd ( 𝜑 → 1 ∈ ℂ )
77 ax-1ne0 1 ≠ 0
78 77 a1i ( 𝜑 → 1 ≠ 0 )
79 76 8 9 76 16 78 divadddivd ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 / 1 ) ) = ( ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) / ( 2 · 1 ) ) )
80 76 76 mulcld ( 𝜑 → ( 1 · 1 ) ∈ ℂ )
81 9 8 mulcld ( 𝜑 → ( 𝑁 · 2 ) ∈ ℂ )
82 80 81 addcomd ( 𝜑 → ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) = ( ( 𝑁 · 2 ) + ( 1 · 1 ) ) )
83 9 8 mulcomd ( 𝜑 → ( 𝑁 · 2 ) = ( 2 · 𝑁 ) )
84 76 mulid1d ( 𝜑 → ( 1 · 1 ) = 1 )
85 83 84 oveq12d ( 𝜑 → ( ( 𝑁 · 2 ) + ( 1 · 1 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
86 82 85 eqtrd ( 𝜑 → ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
87 8 mulid1d ( 𝜑 → ( 2 · 1 ) = 2 )
88 86 87 oveq12d ( 𝜑 → ( ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) / ( 2 · 1 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
89 75 79 88 3eqtrd ( 𝜑 → ( ( 1 / 2 ) + 𝑁 ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
90 89 ad2antrr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / 2 ) + 𝑁 ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
91 72 90 eqtrd ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
92 91 oveq1d ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
93 23 25 92 3eqtr4rd ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
94 iffalse ( ¬ ( 𝑠 mod ( 2 · π ) ) = 0 → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
95 94 adantl ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
96 13 a1i ( 𝑠 ∈ ℝ → π ∈ ℂ )
97 19 a1i ( 𝑠 ∈ ℝ → π ≠ 0 )
98 29 96 97 divcan1d ( 𝑠 ∈ ℝ → ( ( 𝑠 / π ) · π ) = 𝑠 )
99 98 eqcomd ( 𝑠 ∈ ℝ → 𝑠 = ( ( 𝑠 / π ) · π ) )
100 99 ad2antrr ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → 𝑠 = ( ( 𝑠 / π ) · π ) )
101 simpr ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 mod π ) = 0 )
102 simpl ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → 𝑠 ∈ ℝ )
103 mod0 ( ( 𝑠 ∈ ℝ ∧ π ∈ ℝ+ ) → ( ( 𝑠 mod π ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
104 102 41 103 sylancl ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 mod π ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
105 101 104 mpbid ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) ∈ ℤ )
106 105 adantlr ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) ∈ ℤ )
107 rpreccl ( π ∈ ℝ+ → ( 1 / π ) ∈ ℝ+ )
108 41 107 ax-mp ( 1 / π ) ∈ ℝ+
109 moddi ( ( ( 1 / π ) ∈ ℝ+𝑠 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) = ( ( ( 1 / π ) · 𝑠 ) mod ( ( 1 / π ) · ( 2 · π ) ) ) )
110 108 43 109 mp3an13 ( 𝑠 ∈ ℝ → ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) = ( ( ( 1 / π ) · 𝑠 ) mod ( ( 1 / π ) · ( 2 · π ) ) ) )
111 29 96 97 divrec2d ( 𝑠 ∈ ℝ → ( 𝑠 / π ) = ( ( 1 / π ) · 𝑠 ) )
112 111 eqcomd ( 𝑠 ∈ ℝ → ( ( 1 / π ) · 𝑠 ) = ( 𝑠 / π ) )
113 96 97 reccld ( 𝑠 ∈ ℝ → ( 1 / π ) ∈ ℂ )
114 32 a1i ( 𝑠 ∈ ℝ → ( 2 · π ) ∈ ℂ )
115 113 114 mulcomd ( 𝑠 ∈ ℝ → ( ( 1 / π ) · ( 2 · π ) ) = ( ( 2 · π ) · ( 1 / π ) ) )
116 2cnd ( 𝑠 ∈ ℝ → 2 ∈ ℂ )
117 116 96 113 mulassd ( 𝑠 ∈ ℝ → ( ( 2 · π ) · ( 1 / π ) ) = ( 2 · ( π · ( 1 / π ) ) ) )
118 13 19 recidi ( π · ( 1 / π ) ) = 1
119 118 oveq2i ( 2 · ( π · ( 1 / π ) ) ) = ( 2 · 1 )
120 116 mulid1d ( 𝑠 ∈ ℝ → ( 2 · 1 ) = 2 )
121 119 120 syl5eq ( 𝑠 ∈ ℝ → ( 2 · ( π · ( 1 / π ) ) ) = 2 )
122 115 117 121 3eqtrd ( 𝑠 ∈ ℝ → ( ( 1 / π ) · ( 2 · π ) ) = 2 )
123 112 122 oveq12d ( 𝑠 ∈ ℝ → ( ( ( 1 / π ) · 𝑠 ) mod ( ( 1 / π ) · ( 2 · π ) ) ) = ( ( 𝑠 / π ) mod 2 ) )
124 110 123 eqtr2d ( 𝑠 ∈ ℝ → ( ( 𝑠 / π ) mod 2 ) = ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) )
125 124 adantr ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 𝑠 / π ) mod 2 ) = ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) )
126 113 adantr ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 1 / π ) ∈ ℂ )
127 id ( 𝑠 ∈ ℝ → 𝑠 ∈ ℝ )
128 43 a1i ( 𝑠 ∈ ℝ → ( 2 · π ) ∈ ℝ+ )
129 127 128 modcld ( 𝑠 ∈ ℝ → ( 𝑠 mod ( 2 · π ) ) ∈ ℝ )
130 129 recnd ( 𝑠 ∈ ℝ → ( 𝑠 mod ( 2 · π ) ) ∈ ℂ )
131 130 adantr ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 mod ( 2 · π ) ) ∈ ℂ )
132 ax-1cn 1 ∈ ℂ
133 132 13 77 19 divne0i ( 1 / π ) ≠ 0
134 133 a1i ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 1 / π ) ≠ 0 )
135 neqne ( ¬ ( 𝑠 mod ( 2 · π ) ) = 0 → ( 𝑠 mod ( 2 · π ) ) ≠ 0 )
136 135 adantl ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 mod ( 2 · π ) ) ≠ 0 )
137 126 131 134 136 mulne0d ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) ≠ 0 )
138 125 137 eqnetrd ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 𝑠 / π ) mod 2 ) ≠ 0 )
139 138 adantr ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 / π ) mod 2 ) ≠ 0 )
140 oddfl ( ( ( 𝑠 / π ) ∈ ℤ ∧ ( ( 𝑠 / π ) mod 2 ) ≠ 0 ) → ( 𝑠 / π ) = ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) )
141 106 139 140 syl2anc ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) = ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) )
142 141 oveq1d ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 / π ) · π ) = ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) )
143 100 142 eqtrd ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → 𝑠 = ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) )
144 143 oveq2d ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑘 · 𝑠 ) = ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) )
145 144 fveq2d ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) = ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) )
146 145 sumeq2sdv ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) )
147 146 oveq2d ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) )
148 147 oveq1d ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) )
149 148 adantlll ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) )
150 2 ad2antrr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod π ) = 0 ) → 𝑁 ∈ ℕ )
151 17 a1i ( 𝑠 ∈ ℝ → π ∈ ℝ )
152 127 151 97 redivcld ( 𝑠 ∈ ℝ → ( 𝑠 / π ) ∈ ℝ )
153 152 rehalfcld ( 𝑠 ∈ ℝ → ( ( 𝑠 / π ) / 2 ) ∈ ℝ )
154 153 flcld ( 𝑠 ∈ ℝ → ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ∈ ℤ )
155 154 ad2antlr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod π ) = 0 ) → ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ∈ ℤ )
156 eqid ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) = ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π )
157 150 155 156 dirkertrigeqlem3 ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) )
158 157 adantlr ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) )
159 141 adantlll ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) = ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) )
160 159 eqcomd ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) = ( 𝑠 / π ) )
161 160 oveq1d ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) = ( ( 𝑠 / π ) · π ) )
162 161 oveq2d ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) )
163 162 fveq2d ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) )
164 161 fvoveq1d ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) = ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) )
165 164 oveq2d ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) )
166 163 165 oveq12d ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) )
167 98 oveq2d ( 𝑠 ∈ ℝ → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) )
168 167 fveq2d ( 𝑠 ∈ ℝ → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
169 98 fvoveq1d ( 𝑠 ∈ ℝ → ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
170 169 oveq2d ( 𝑠 ∈ ℝ → ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) )
171 168 170 oveq12d ( 𝑠 ∈ ℝ → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
172 171 adantl ( ( 𝜑𝑠 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
173 172 ad2antrr ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
174 166 173 eqtrd ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
175 149 158 174 3eqtrrd ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
176 simplr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → 𝑠 ∈ ℝ )
177 simpr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ¬ ( 𝑠 mod π ) = 0 )
178 176 41 103 sylancl ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 mod π ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
179 177 178 mtbid ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ¬ ( 𝑠 / π ) ∈ ℤ )
180 176 recnd ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → 𝑠 ∈ ℂ )
181 sineq0 ( 𝑠 ∈ ℂ → ( ( sin ‘ 𝑠 ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
182 180 181 syl ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ 𝑠 ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
183 179 182 mtbird ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ¬ ( sin ‘ 𝑠 ) = 0 )
184 183 neqned ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( sin ‘ 𝑠 ) ≠ 0 )
185 2 ad2antrr ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → 𝑁 ∈ ℕ )
186 176 184 185 dirkertrigeqlem2 ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
187 186 eqcomd ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
188 187 adantlr ( ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
189 175 188 pm2.61dan ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
190 95 189 eqtr2d ( ( ( 𝜑𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
191 93 190 pm2.61dan ( ( 𝜑𝑠 ∈ ℝ ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
192 191 mpteq2dva ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
193 4 192 eqtr2id ( 𝜑 → ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = 𝐻 )
194 5 7 193 3eqtrd ( 𝜑𝐹 = 𝐻 )