This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mulridd ⊢ ( 𝜑 → ( 𝑁 · 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 mulridd ⊢ ( 𝜑 → ( 1 · 1 ) = 1 )
85 83 84 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 · 2 ) + ( 1 · 1 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
86 82 85 eqtrd ⊢ ( 𝜑 → ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
87 8 mulridd ⊢ ( 𝜑 → ( 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 mulridd ⊢ ( 𝑠 ∈ ℝ → ( 2 · 1 ) = 2 )
121 119 120 eqtrid ⊢ ( 𝑠 ∈ ℝ → ( 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 ⊢ ( 𝜑 → 𝐹 = 𝐻 )