Metamath Proof Explorer

Theorem dirkertrigeqlem3

Description: Trigonometric equality lemma for the Dirichlet kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of _pi . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeqlem3.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dirkertrigeqlem3.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
dirkertrigeqlem3.a ⊢ 𝐴 = ( ( ( 2 · 𝐾 ) + 1 ) · π )
Assertion dirkertrigeqlem3 ( 𝜑 → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkertrigeqlem3.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 dirkertrigeqlem3.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
3 dirkertrigeqlem3.a ⊢ 𝐴 = ( ( ( 2 · 𝐾 ) + 1 ) · π )
4 3 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐴 = ( ( ( 2 · 𝐾 ) + 1 ) · π ) )
5 4 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 · 𝐴 ) = ( 𝑛 · ( ( ( 2 · 𝐾 ) + 1 ) · π ) ) )
6 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℤ )
7 6 zcnd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℂ )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℂ )
9 2cnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 2 ∈ ℂ )
10 2 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐾 ∈ ℂ )
12 9 11 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 2 · 𝐾 ) ∈ ℂ )
13 1cnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
14 12 13 addcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2 · 𝐾 ) + 1 ) ∈ ℂ )
15 picn ⊢ π ∈ ℂ
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → π ∈ ℂ )
17 14 16 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 2 · 𝐾 ) + 1 ) · π ) ∈ ℂ )
18 8 17 mulcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 · ( ( ( 2 · 𝐾 ) + 1 ) · π ) ) = ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) · 𝑛 ) )
19 14 16 8 mulassd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) · 𝑛 ) = ( ( ( 2 · 𝐾 ) + 1 ) · ( π · 𝑛 ) ) )
20 16 8 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( π · 𝑛 ) ∈ ℂ )
21 12 13 20 adddird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 2 · 𝐾 ) + 1 ) · ( π · 𝑛 ) ) = ( ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) + ( 1 · ( π · 𝑛 ) ) ) )
22 12 20 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) ∈ ℂ )
23 13 20 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 · ( π · 𝑛 ) ) ∈ ℂ )
24 22 23 addcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) + ( 1 · ( π · 𝑛 ) ) ) = ( ( 1 · ( π · 𝑛 ) ) + ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) ) )
25 15 a1i ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → π ∈ ℂ )
26 25 7 mulcld ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( π · 𝑛 ) ∈ ℂ )
27 26 mullidd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 1 · ( π · 𝑛 ) ) = ( π · 𝑛 ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 1 · ( π · 𝑛 ) ) = ( π · 𝑛 ) )
29 9 11 16 8 mul4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) = ( ( 2 · π ) · ( 𝐾 · 𝑛 ) ) )
30 9 16 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 2 · π ) ∈ ℂ )
31 11 8 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 · 𝑛 ) ∈ ℂ )
32 30 31 mulcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2 · π ) · ( 𝐾 · 𝑛 ) ) = ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) )
33 29 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) = ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) )
34 28 33 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 · ( π · 𝑛 ) ) + ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) ) = ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) )
35 24 34 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 2 · 𝐾 ) · ( π · 𝑛 ) ) + ( 1 · ( π · 𝑛 ) ) ) = ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) )
36 19 21 35 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) · 𝑛 ) = ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) )
37 5 18 36 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 · 𝐴 ) = ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( 𝑛 · 𝐴 ) ) = ( cos ‘ ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) ) )
39 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
40 6 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ℤ )
41 39 40 zmulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 · 𝑛 ) ∈ ℤ )
42 cosper ⊢ ( ( ( π · 𝑛 ) ∈ ℂ ∧ ( 𝐾 · 𝑛 ) ∈ ℤ ) → ( cos ‘ ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) ) = ( cos ‘ ( π · 𝑛 ) ) )
43 20 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( ( π · 𝑛 ) + ( ( 𝐾 · 𝑛 ) · ( 2 · π ) ) ) ) = ( cos ‘ ( π · 𝑛 ) ) )
44 38 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( 𝑛 · 𝐴 ) ) = ( cos ‘ ( π · 𝑛 ) ) )
45 44 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) )
46 45 oveq2d ⊢ ( 𝜑 → ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) = ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) )
47 46 oveq1d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) )
49 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
50 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
51 2ne0 ⊢ 2 ≠ 0
52 51 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
53 49 50 52 divcan2d ⊢ ( 𝜑 → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
54 53 eqcomd ⊢ ( 𝜑 → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
55 54 oveq2d ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) )
56 55 sumeq1d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( π · 𝑛 ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( π · 𝑛 ) ) )
58 15 a1i ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) → π ∈ ℂ )
59 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) → 𝑛 ∈ ℤ )
60 59 zcnd ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) → 𝑛 ∈ ℂ )
61 58 60 mulcomd ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) → ( π · 𝑛 ) = ( 𝑛 · π ) )
62 61 fveq2d ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( 𝑛 · π ) ) )
63 62 rgen ⊢ ∀ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( 𝑛 · π ) )
64 63 a1i ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ∀ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( 𝑛 · π ) ) )
65 64 sumeq2d ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( 𝑛 · π ) ) )
66 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 mod 2 ) = 0 )
67 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
68 67 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → 𝑁 ∈ ℝ )
69 2rp ⊢ 2 ∈ ℝ+
70 mod0 ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( 𝑁 mod 2 ) = 0 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
71 68 69 70 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 𝑁 mod 2 ) = 0 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
72 66 71 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 / 2 ) ∈ ℤ )
73 2re ⊢ 2 ∈ ℝ
74 73 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
75 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
76 2pos ⊢ 0 < 2
77 76 a1i ⊢ ( 𝜑 → 0 < 2 )
78 67 74 75 77 divgt0d ⊢ ( 𝜑 → 0 < ( 𝑁 / 2 ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → 0 < ( 𝑁 / 2 ) )
80 elnnz ⊢ ( ( 𝑁 / 2 ) ∈ ℕ ↔ ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 < ( 𝑁 / 2 ) ) )
81 72 79 80 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 / 2 ) ∈ ℕ )
82 dirkertrigeqlem1 ⊢ ( ( 𝑁 / 2 ) ∈ ℕ → Σ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )
83 81 82 syl ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... ( 2 · ( 𝑁 / 2 ) ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )
84 57 65 83 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = 0 )
85 84 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) = ( ( 1 / 2 ) + 0 ) )
86 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
87 86 addridi ⊢ ( ( 1 / 2 ) + 0 ) = ( 1 / 2 )
88 85 87 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) = ( 1 / 2 ) )
89 88 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) = ( ( 1 / 2 ) / π ) )
90 ax-1cn ⊢ 1 ∈ ℂ
91 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
92 pire ⊢ π ∈ ℝ
93 pipos ⊢ 0 < π
94 92 93 gt0ne0ii ⊢ π ≠ 0
95 15 94 pm3.2i ⊢ ( π ∈ ℂ ∧ π ≠ 0 )
96 divdiv1 ⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( π ∈ ℂ ∧ π ≠ 0 ) ) → ( ( 1 / 2 ) / π ) = ( 1 / ( 2 · π ) ) )
97 90 91 95 96 mp3an ⊢ ( ( 1 / 2 ) / π ) = ( 1 / ( 2 · π ) )
98 97 a1i ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 1 / 2 ) / π ) = ( 1 / ( 2 · π ) ) )
99 48 89 98 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( 1 / ( 2 · π ) ) )
100 3 oveq2i ⊢ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · 𝐾 ) + 1 ) · π ) )
101 100 a1i ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · 𝐾 ) + 1 ) · π ) ) )
102 86 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
103 49 102 addcld ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
104 50 10 mulcld ⊢ ( 𝜑 → ( 2 · 𝐾 ) ∈ ℂ )
105 peano2cn ⊢ ( ( 2 · 𝐾 ) ∈ ℂ → ( ( 2 · 𝐾 ) + 1 ) ∈ ℂ )
106 104 105 syl ⊢ ( 𝜑 → ( ( 2 · 𝐾 ) + 1 ) ∈ ℂ )
107 15 a1i ⊢ ( 𝜑 → π ∈ ℂ )
108 103 106 107 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) · π ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · 𝐾 ) + 1 ) · π ) ) )
109 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
110 49 102 104 109 muladdd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) = ( ( ( 𝑁 · ( 2 · 𝐾 ) ) + ( 1 · ( 1 / 2 ) ) ) + ( ( 𝑁 · 1 ) + ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) ) ) )
111 49 50 10 mul12d ⊢ ( 𝜑 → ( 𝑁 · ( 2 · 𝐾 ) ) = ( 2 · ( 𝑁 · 𝐾 ) ) )
112 102 mullidd ⊢ ( 𝜑 → ( 1 · ( 1 / 2 ) ) = ( 1 / 2 ) )
113 111 112 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 · ( 2 · 𝐾 ) ) + ( 1 · ( 1 / 2 ) ) ) = ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( 1 / 2 ) ) )
114 49 mulridd ⊢ ( 𝜑 → ( 𝑁 · 1 ) = 𝑁 )
115 50 10 mulcomd ⊢ ( 𝜑 → ( 2 · 𝐾 ) = ( 𝐾 · 2 ) )
116 115 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) = ( ( 𝐾 · 2 ) · ( 1 / 2 ) ) )
117 10 50 102 mulassd ⊢ ( 𝜑 → ( ( 𝐾 · 2 ) · ( 1 / 2 ) ) = ( 𝐾 · ( 2 · ( 1 / 2 ) ) ) )
118 2thalfe1 ⊢ ( 2 · ( 1 / 2 ) ) = 1
119 118 oveq2i ⊢ ( 𝐾 · ( 2 · ( 1 / 2 ) ) ) = ( 𝐾 · 1 )
120 10 mulridd ⊢ ( 𝜑 → ( 𝐾 · 1 ) = 𝐾 )
121 119 120 eqtrid ⊢ ( 𝜑 → ( 𝐾 · ( 2 · ( 1 / 2 ) ) ) = 𝐾 )
122 116 117 121 3eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) = 𝐾 )
123 114 122 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 · 1 ) + ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) ) = ( 𝑁 + 𝐾 ) )
124 113 123 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 · ( 2 · 𝐾 ) ) + ( 1 · ( 1 / 2 ) ) ) + ( ( 𝑁 · 1 ) + ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) ) ) = ( ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( 1 / 2 ) ) + ( 𝑁 + 𝐾 ) ) )
125 49 10 mulcld ⊢ ( 𝜑 → ( 𝑁 · 𝐾 ) ∈ ℂ )
126 50 125 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝑁 · 𝐾 ) ) ∈ ℂ )
127 49 10 addcld ⊢ ( 𝜑 → ( 𝑁 + 𝐾 ) ∈ ℂ )
128 126 102 127 addassd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( 1 / 2 ) ) + ( 𝑁 + 𝐾 ) ) = ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ) )
129 110 124 128 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) = ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ) )
130 102 127 addcld ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ∈ ℂ )
131 126 130 addcomd ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ) = ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( 2 · ( 𝑁 · 𝐾 ) ) ) )
132 50 125 mulcomd ⊢ ( 𝜑 → ( 2 · ( 𝑁 · 𝐾 ) ) = ( ( 𝑁 · 𝐾 ) · 2 ) )
133 132 oveq2d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( 2 · ( 𝑁 · 𝐾 ) ) ) = ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) )
134 129 131 133 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) = ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) )
135 134 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) · π ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) · π ) )
136 125 50 mulcld ⊢ ( 𝜑 → ( ( 𝑁 · 𝐾 ) · 2 ) ∈ ℂ )
137 130 136 107 adddird ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) · π ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( ( 𝑁 · 𝐾 ) · 2 ) · π ) ) )
138 125 50 107 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 · 𝐾 ) · 2 ) · π ) = ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) )
139 138 oveq2d ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( ( 𝑁 · 𝐾 ) · 2 ) · π ) ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) )
140 135 137 139 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) · π ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) )
141 101 108 140 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) )
142 141 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) = ( sin ‘ ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) ) )
143 130 107 mulcld ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ∈ ℂ )
144 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
145 144 2 zmulcld ⊢ ( 𝜑 → ( 𝑁 · 𝐾 ) ∈ ℤ )
146 sinper ⊢ ( ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ∈ ℂ ∧ ( 𝑁 · 𝐾 ) ∈ ℤ ) → ( sin ‘ ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ) )
147 143 145 146 syl2anc ⊢ ( 𝜑 → ( sin ‘ ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ) )
148 102 127 addcomd ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) = ( ( 𝑁 + 𝐾 ) + ( 1 / 2 ) ) )
149 49 10 102 addassd ⊢ ( 𝜑 → ( ( 𝑁 + 𝐾 ) + ( 1 / 2 ) ) = ( 𝑁 + ( 𝐾 + ( 1 / 2 ) ) ) )
150 10 102 addcld ⊢ ( 𝜑 → ( 𝐾 + ( 1 / 2 ) ) ∈ ℂ )
151 49 150 addcomd ⊢ ( 𝜑 → ( 𝑁 + ( 𝐾 + ( 1 / 2 ) ) ) = ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) )
152 148 149 151 3eqtrd ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) = ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) )
153 152 oveq1d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) = ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) )
154 153 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) )
155 142 147 154 3eqtrd ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) )
156 3 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( 2 · 𝐾 ) + 1 ) · π ) )
157 156 oveq1d ⊢ ( 𝜑 → ( 𝐴 / 2 ) = ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) / 2 ) )
158 106 107 50 52 div23d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) / 2 ) = ( ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) · π ) )
159 104 109 50 52 divdird ⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) = ( ( ( 2 · 𝐾 ) / 2 ) + ( 1 / 2 ) ) )
160 10 50 52 divcan3d ⊢ ( 𝜑 → ( ( 2 · 𝐾 ) / 2 ) = 𝐾 )
161 160 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) / 2 ) + ( 1 / 2 ) ) = ( 𝐾 + ( 1 / 2 ) ) )
162 159 161 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) = ( 𝐾 + ( 1 / 2 ) ) )
163 162 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) · π ) = ( ( 𝐾 + ( 1 / 2 ) ) · π ) )
164 157 158 163 3eqtrd ⊢ ( 𝜑 → ( 𝐴 / 2 ) = ( ( 𝐾 + ( 1 / 2 ) ) · π ) )
165 164 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( 𝐴 / 2 ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
166 165 oveq2d ⊢ ( 𝜑 → ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) )
167 155 166 oveq12d ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
168 167 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
169 150 49 107 adddird ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) )
170 169 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) )
171 170 oveq1d ⊢ ( 𝜑 → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
172 171 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
173 49 halfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℂ )
174 50 173 mulcomd ⊢ ( 𝜑 → ( 2 · ( 𝑁 / 2 ) ) = ( ( 𝑁 / 2 ) · 2 ) )
175 53 174 eqtr3d ⊢ ( 𝜑 → 𝑁 = ( ( 𝑁 / 2 ) · 2 ) )
176 175 oveq1d ⊢ ( 𝜑 → ( 𝑁 · π ) = ( ( ( 𝑁 / 2 ) · 2 ) · π ) )
177 173 50 107 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 / 2 ) · 2 ) · π ) = ( ( 𝑁 / 2 ) · ( 2 · π ) ) )
178 176 177 eqtrd ⊢ ( 𝜑 → ( 𝑁 · π ) = ( ( 𝑁 / 2 ) · ( 2 · π ) ) )
179 178 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) )
180 179 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) )
181 180 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) )
182 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → 𝐾 ∈ ℂ )
183 1cnd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → 1 ∈ ℂ )
184 183 halfcld ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 1 / 2 ) ∈ ℂ )
185 182 184 addcld ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 𝐾 + ( 1 / 2 ) ) ∈ ℂ )
186 15 a1i ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → π ∈ ℂ )
187 185 186 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ )
188 sinper ⊢ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
189 187 72 188 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
190 181 189 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
191 50 107 mulcld ⊢ ( 𝜑 → ( 2 · π ) ∈ ℂ )
192 150 107 mulcld ⊢ ( 𝜑 → ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ )
193 192 sincld ⊢ ( 𝜑 → ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ∈ ℂ )
194 191 193 mulcomd ⊢ ( 𝜑 → ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) )
195 194 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) )
196 190 195 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
197 94 a1i ⊢ ( 𝜑 → π ≠ 0 )
198 150 107 197 divcan4d ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) = ( 𝐾 + ( 1 / 2 ) ) )
199 2 zred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
200 69 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
201 200 rpreccld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ+ )
202 199 201 ltaddrpd ⊢ ( 𝜑 → 𝐾 < ( 𝐾 + ( 1 / 2 ) ) )
203 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
204 203 rehalfcld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
205 halflt1 ⊢ ( 1 / 2 ) < 1
206 205 a1i ⊢ ( 𝜑 → ( 1 / 2 ) < 1 )
207 204 203 199 206 ltadd2dd ⊢ ( 𝜑 → ( 𝐾 + ( 1 / 2 ) ) < ( 𝐾 + 1 ) )
208 btwnnz ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 < ( 𝐾 + ( 1 / 2 ) ) ∧ ( 𝐾 + ( 1 / 2 ) ) < ( 𝐾 + 1 ) ) → ¬ ( 𝐾 + ( 1 / 2 ) ) ∈ ℤ )
209 2 202 207 208 syl3anc ⊢ ( 𝜑 → ¬ ( 𝐾 + ( 1 / 2 ) ) ∈ ℤ )
210 198 209 eqneltrd ⊢ ( 𝜑 → ¬ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) ∈ ℤ )
211 sineq0 ⊢ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) = 0 ↔ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) ∈ ℤ ) )
212 192 211 syl ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) = 0 ↔ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) ∈ ℤ ) )
213 210 212 mtbird ⊢ ( 𝜑 → ¬ ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) = 0 )
214 213 neqned ⊢ ( 𝜑 → ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ≠ 0 )
215 50 107 52 197 mulne0d ⊢ ( 𝜑 → ( 2 · π ) ≠ 0 )
216 193 193 191 214 215 divdiv1d ⊢ ( 𝜑 → ( ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
217 193 214 dividd ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = 1 )
218 217 oveq1d ⊢ ( 𝜑 → ( ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( 1 / ( 2 · π ) ) )
219 216 218 eqtr3d ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) = ( 1 / ( 2 · π ) ) )
220 219 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) = ( 1 / ( 2 · π ) ) )
221 196 220 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( 1 / ( 2 · π ) ) )
222 168 172 221 3eqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 1 / ( 2 · π ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
223 99 222 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
224 47 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) )
225 144 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → 𝑁 ∈ ℤ )
226 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ¬ ( 𝑁 mod 2 ) = 0 )
227 226 neqned ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 mod 2 ) ≠ 0 )
228 oddfl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 mod 2 ) ≠ 0 ) → 𝑁 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
229 225 227 228 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → 𝑁 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
230 229 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 1 ... 𝑁 ) = ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
231 230 sumeq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) )
232 fvoveq1 ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ⌊ ‘ ( 1 / 2 ) ) )
233 halffl ⊢ ( ⌊ ‘ ( 1 / 2 ) ) = 0
234 232 233 eqtrdi ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 2 ) ) = 0 )
235 234 oveq2d ⊢ ( 𝑁 = 1 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) = ( 2 · 0 ) )
236 2t0e0 ⊢ ( 2 · 0 ) = 0
237 235 236 eqtrdi ⊢ ( 𝑁 = 1 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) = 0 )
238 237 oveq1d ⊢ ( 𝑁 = 1 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) = ( 0 + 1 ) )
239 90 addlidi ⊢ ( 0 + 1 ) = 1
240 238 239 eqtrdi ⊢ ( 𝑁 = 1 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) = 1 )
241 240 oveq2d ⊢ ( 𝑁 = 1 → ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) = ( 1 ... 1 ) )
242 241 sumeq1d ⊢ ( 𝑁 = 1 → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) )
243 1z ⊢ 1 ∈ ℤ
244 coscl ⊢ ( π ∈ ℂ → ( cos ‘ π ) ∈ ℂ )
245 15 244 ax-mp ⊢ ( cos ‘ π ) ∈ ℂ
246 oveq2 ⊢ ( 𝑛 = 1 → ( π · 𝑛 ) = ( π · 1 ) )
247 15 mulridi ⊢ ( π · 1 ) = π
248 246 247 eqtrdi ⊢ ( 𝑛 = 1 → ( π · 𝑛 ) = π )
249 248 fveq2d ⊢ ( 𝑛 = 1 → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π ) )
250 249 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ ( cos ‘ π ) ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π ) )
251 243 245 250 mp2an ⊢ Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π )
252 251 a1i ⊢ ( 𝑁 = 1 → Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π ) )
253 cospi ⊢ ( cos ‘ π ) = - 1
254 253 a1i ⊢ ( 𝑁 = 1 → ( cos ‘ π ) = - 1 )
255 242 252 254 3eqtrd ⊢ ( 𝑁 = 1 → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
256 255 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
257 2nn ⊢ 2 ∈ ℕ
258 257 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ∈ ℕ )
259 67 rehalfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℝ )
260 259 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
261 260 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
262 2div2e1 ⊢ ( 2 / 2 ) = 1
263 73 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ∈ ℝ )
264 67 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 𝑁 ∈ ℝ )
265 69 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ∈ ℝ+ )
266 neqne ⊢ ( ¬ 𝑁 = 1 → 𝑁 ≠ 1 )
267 nnne1ge2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )
268 1 266 267 syl2an ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ≤ 𝑁 )
269 263 264 265 268 lediv1dd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 2 / 2 ) ≤ ( 𝑁 / 2 ) )
270 262 269 eqbrtrrid ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 1 ≤ ( 𝑁 / 2 ) )
271 259 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 𝑁 / 2 ) ∈ ℝ )
272 flge ⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ ( 𝑁 / 2 ) ↔ 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
273 271 243 272 sylancl ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 1 ≤ ( 𝑁 / 2 ) ↔ 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
274 270 273 mpbid ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
275 elnnz1 ⊢ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
276 261 274 275 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℕ )
277 258 276 nnmulcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ∈ ℕ )
278 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
279 277 278 eleqtrdi ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ∈ ( ℤ≥ ‘ 1 ) )
280 15 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → π ∈ ℂ )
281 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) → 𝑛 ∈ ℤ )
282 281 zcnd ⊢ ( 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) → 𝑛 ∈ ℂ )
283 282 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → 𝑛 ∈ ℂ )
284 280 283 mulcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → ( π · 𝑛 ) ∈ ℂ )
285 284 coscld ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → ( cos ‘ ( π · 𝑛 ) ) ∈ ℂ )
286 oveq2 ⊢ ( 𝑛 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) → ( π · 𝑛 ) = ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
287 286 fveq2d ⊢ ( 𝑛 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) )
288 279 285 287 fsump1 ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) + ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) ) )
289 15 a1i ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → π ∈ ℂ )
290 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → 𝑛 ∈ ℤ )
291 290 zcnd ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → 𝑛 ∈ ℂ )
292 289 291 mulcomd ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → ( π · 𝑛 ) = ( 𝑛 · π ) )
293 292 fveq2d ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( 𝑛 · π ) ) )
294 293 sumeq2i ⊢ Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( 𝑛 · π ) )
295 dirkertrigeqlem1 ⊢ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )
296 276 295 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )
297 294 296 eqtrid ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) = 0 )
298 260 zcnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℂ )
299 50 298 mulcld ⊢ ( 𝜑 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ∈ ℂ )
300 107 299 109 adddid ⊢ ( 𝜑 → ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) = ( ( π · ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) + ( π · 1 ) ) )
301 107 50 298 mul13d ⊢ ( 𝜑 → ( π · ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) )
302 247 a1i ⊢ ( 𝜑 → ( π · 1 ) = π )
303 301 302 oveq12d ⊢ ( 𝜑 → ( ( π · ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) + ( π · 1 ) ) = ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) + π ) )
304 298 191 mulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ∈ ℂ )
305 304 107 addcomd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) + π ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
306 300 303 305 3eqtrd ⊢ ( 𝜑 → ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
307 306 fveq2d ⊢ ( 𝜑 → ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) = ( cos ‘ ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
308 cosper ⊢ ( ( π ∈ ℂ ∧ ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ) → ( cos ‘ ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
309 107 260 308 syl2anc ⊢ ( 𝜑 → ( cos ‘ ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
310 253 a1i ⊢ ( 𝜑 → ( cos ‘ π ) = - 1 )
311 307 309 310 3eqtrd ⊢ ( 𝜑 → ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) = - 1 )
312 311 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) = - 1 )
313 297 312 oveq12d ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) + ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) ) = ( 0 + - 1 ) )
314 neg1cn ⊢ - 1 ∈ ℂ
315 314 addlidi ⊢ ( 0 + - 1 ) = - 1
316 315 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 0 + - 1 ) = - 1 )
317 288 313 316 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
318 256 317 pm2.61dan ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
319 318 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
320 231 319 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
321 320 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) = ( ( 1 / 2 ) + - 1 ) )
322 321 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
323 167 171 eqtrd ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
324 323 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
325 229 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 · π ) = ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) )
326 299 109 107 adddird ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) = ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + ( 1 · π ) ) )
327 107 mullidd ⊢ ( 𝜑 → ( 1 · π ) = π )
328 327 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + ( 1 · π ) ) = ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + π ) )
329 299 107 mulcld ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ∈ ℂ )
330 329 107 addcomd ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + π ) = ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) )
331 326 328 330 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) = ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) )
332 331 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) = ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) )
333 50 298 mulcomd ⊢ ( 𝜑 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · 2 ) )
334 333 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) = ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · 2 ) · π ) )
335 298 50 107 mulassd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · 2 ) · π ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) )
336 334 335 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) )
337 336 oveq2d ⊢ ( 𝜑 → ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
338 337 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
339 325 332 338 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 · π ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
340 339 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
341 192 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ )
342 15 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → π ∈ ℂ )
343 304 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ∈ ℂ )
344 341 342 343 addassd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
345 340 344 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) = ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
346 345 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
347 346 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
348 192 107 addcld ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ∈ ℂ )
349 sinper ⊢ ( ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ∈ ℂ ∧ ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ) → ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) )
350 348 260 349 syl2anc ⊢ ( 𝜑 → ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) )
351 sinppi ⊢ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) = - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
352 192 351 syl ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) = - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
353 350 352 eqtrd ⊢ ( 𝜑 → ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
354 353 oveq1d ⊢ ( 𝜑 → ( ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
355 194 oveq2d ⊢ ( 𝜑 → ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
356 193 193 214 divnegd ⊢ ( 𝜑 → - ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) )
357 217 negeqd ⊢ ( 𝜑 → - ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = - 1 )
358 356 357 eqtr3d ⊢ ( 𝜑 → ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = - 1 )
359 358 oveq1d ⊢ ( 𝜑 → ( ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( - 1 / ( 2 · π ) ) )
360 193 negcld ⊢ ( 𝜑 → - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ∈ ℂ )
361 360 193 191 214 215 divdiv1d ⊢ ( 𝜑 → ( ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
362 86 90 negsubi ⊢ ( ( 1 / 2 ) + - 1 ) = ( ( 1 / 2 ) − 1 )
363 90 86 negsubdi2i ⊢ - ( 1 − ( 1 / 2 ) ) = ( ( 1 / 2 ) − 1 )
364 1mhlfehlf ⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
365 364 negeqi ⊢ - ( 1 − ( 1 / 2 ) ) = - ( 1 / 2 )
366 2cn ⊢ 2 ∈ ℂ
367 divneg ⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 1 / 2 ) = ( - 1 / 2 ) )
368 90 366 51 367 mp3an ⊢ - ( 1 / 2 ) = ( - 1 / 2 )
369 365 368 eqtri ⊢ - ( 1 − ( 1 / 2 ) ) = ( - 1 / 2 )
370 362 363 369 3eqtr2i ⊢ ( ( 1 / 2 ) + - 1 ) = ( - 1 / 2 )
371 370 oveq1i ⊢ ( ( ( 1 / 2 ) + - 1 ) / π ) = ( ( - 1 / 2 ) / π )
372 divdiv1 ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( π ∈ ℂ ∧ π ≠ 0 ) ) → ( ( - 1 / 2 ) / π ) = ( - 1 / ( 2 · π ) ) )
373 314 91 95 372 mp3an ⊢ ( ( - 1 / 2 ) / π ) = ( - 1 / ( 2 · π ) )
374 371 373 eqtr2i ⊢ ( - 1 / ( 2 · π ) ) = ( ( ( 1 / 2 ) + - 1 ) / π )
375 374 a1i ⊢ ( 𝜑 → ( - 1 / ( 2 · π ) ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
376 359 361 375 3eqtr3d ⊢ ( 𝜑 → ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
377 354 355 376 3eqtrd ⊢ ( 𝜑 → ( ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
378 377 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
379 324 347 378 3eqtrrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + - 1 ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
380 224 322 379 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
381 223 380 pm2.61dan ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )