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 mulid2d ⊢ ( 𝑛 ∈ ( 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 addid1i ⊢ ( ( 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 mulid2d ⊢ ( 𝜑 → ( 1 · ( 1 / 2 ) ) = ( 1 / 2 ) )
113 111 112 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 · ( 2 · 𝐾 ) ) + ( 1 · ( 1 / 2 ) ) ) = ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( 1 / 2 ) ) )
114 49 mulid1d ⊢ ( 𝜑 → ( 𝑁 · 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 2cn ⊢ 2 ∈ ℂ
119 118 51 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
120 119 oveq2i ⊢ ( 𝐾 · ( 2 · ( 1 / 2 ) ) ) = ( 𝐾 · 1 )
121 10 mulid1d ⊢ ( 𝜑 → ( 𝐾 · 1 ) = 𝐾 )
122 120 121 eqtrid ⊢ ( 𝜑 → ( 𝐾 · ( 2 · ( 1 / 2 ) ) ) = 𝐾 )
123 116 117 122 3eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) = 𝐾 )
124 114 123 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 · 1 ) + ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) ) = ( 𝑁 + 𝐾 ) )
125 113 124 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 · ( 2 · 𝐾 ) ) + ( 1 · ( 1 / 2 ) ) ) + ( ( 𝑁 · 1 ) + ( ( 2 · 𝐾 ) · ( 1 / 2 ) ) ) ) = ( ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( 1 / 2 ) ) + ( 𝑁 + 𝐾 ) ) )
126 49 10 mulcld ⊢ ( 𝜑 → ( 𝑁 · 𝐾 ) ∈ ℂ )
127 50 126 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝑁 · 𝐾 ) ) ∈ ℂ )
128 49 10 addcld ⊢ ( 𝜑 → ( 𝑁 + 𝐾 ) ∈ ℂ )
129 127 102 128 addassd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( 1 / 2 ) ) + ( 𝑁 + 𝐾 ) ) = ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ) )
130 110 125 129 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) = ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ) )
131 102 128 addcld ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ∈ ℂ )
132 127 131 addcomd ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 · 𝐾 ) ) + ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) ) = ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( 2 · ( 𝑁 · 𝐾 ) ) ) )
133 50 126 mulcomd ⊢ ( 𝜑 → ( 2 · ( 𝑁 · 𝐾 ) ) = ( ( 𝑁 · 𝐾 ) · 2 ) )
134 133 oveq2d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( 2 · ( 𝑁 · 𝐾 ) ) ) = ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) )
135 130 132 134 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) = ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) )
136 135 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) · π ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) · π ) )
137 126 50 mulcld ⊢ ( 𝜑 → ( ( 𝑁 · 𝐾 ) · 2 ) ∈ ℂ )
138 131 137 107 adddird ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) + ( ( 𝑁 · 𝐾 ) · 2 ) ) · π ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( ( 𝑁 · 𝐾 ) · 2 ) · π ) ) )
139 126 50 107 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 · 𝐾 ) · 2 ) · π ) = ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) )
140 139 oveq2d ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( ( 𝑁 · 𝐾 ) · 2 ) · π ) ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) )
141 136 138 140 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 2 · 𝐾 ) + 1 ) ) · π ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) )
142 101 108 141 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) = ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) )
143 142 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) = ( sin ‘ ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) ) )
144 131 107 mulcld ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ∈ ℂ )
145 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
146 145 2 zmulcld ⊢ ( 𝜑 → ( 𝑁 · 𝐾 ) ∈ ℤ )
147 sinper ⊢ ( ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ∈ ℂ ∧ ( 𝑁 · 𝐾 ) ∈ ℤ ) → ( sin ‘ ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ) )
148 144 146 147 syl2anc ⊢ ( 𝜑 → ( sin ‘ ( ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) + ( ( 𝑁 · 𝐾 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ) )
149 102 128 addcomd ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) = ( ( 𝑁 + 𝐾 ) + ( 1 / 2 ) ) )
150 49 10 102 addassd ⊢ ( 𝜑 → ( ( 𝑁 + 𝐾 ) + ( 1 / 2 ) ) = ( 𝑁 + ( 𝐾 + ( 1 / 2 ) ) ) )
151 10 102 addcld ⊢ ( 𝜑 → ( 𝐾 + ( 1 / 2 ) ) ∈ ℂ )
152 49 151 addcomd ⊢ ( 𝜑 → ( 𝑁 + ( 𝐾 + ( 1 / 2 ) ) ) = ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) )
153 149 150 152 3eqtrd ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) = ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) )
154 153 oveq1d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) = ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) )
155 154 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( ( 1 / 2 ) + ( 𝑁 + 𝐾 ) ) · π ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) )
156 143 148 155 3eqtrd ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) )
157 3 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( 2 · 𝐾 ) + 1 ) · π ) )
158 157 oveq1d ⊢ ( 𝜑 → ( 𝐴 / 2 ) = ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) / 2 ) )
159 106 107 50 52 div23d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐾 ) + 1 ) · π ) / 2 ) = ( ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) · π ) )
160 104 109 50 52 divdird ⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) = ( ( ( 2 · 𝐾 ) / 2 ) + ( 1 / 2 ) ) )
161 10 50 52 divcan3d ⊢ ( 𝜑 → ( ( 2 · 𝐾 ) / 2 ) = 𝐾 )
162 161 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) / 2 ) + ( 1 / 2 ) ) = ( 𝐾 + ( 1 / 2 ) ) )
163 160 162 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) = ( 𝐾 + ( 1 / 2 ) ) )
164 163 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐾 ) + 1 ) / 2 ) · π ) = ( ( 𝐾 + ( 1 / 2 ) ) · π ) )
165 158 159 164 3eqtrd ⊢ ( 𝜑 → ( 𝐴 / 2 ) = ( ( 𝐾 + ( 1 / 2 ) ) · π ) )
166 165 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( 𝐴 / 2 ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
167 166 oveq2d ⊢ ( 𝜑 → ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) )
168 156 167 oveq12d ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
170 151 49 107 adddird ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) )
171 170 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) )
172 171 oveq1d ⊢ ( 𝜑 → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
173 172 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) + 𝑁 ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
174 49 halfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℂ )
175 50 174 mulcomd ⊢ ( 𝜑 → ( 2 · ( 𝑁 / 2 ) ) = ( ( 𝑁 / 2 ) · 2 ) )
176 53 175 eqtr3d ⊢ ( 𝜑 → 𝑁 = ( ( 𝑁 / 2 ) · 2 ) )
177 176 oveq1d ⊢ ( 𝜑 → ( 𝑁 · π ) = ( ( ( 𝑁 / 2 ) · 2 ) · π ) )
178 174 50 107 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 / 2 ) · 2 ) · π ) = ( ( 𝑁 / 2 ) · ( 2 · π ) ) )
179 177 178 eqtrd ⊢ ( 𝜑 → ( 𝑁 · π ) = ( ( 𝑁 / 2 ) · ( 2 · π ) ) )
180 179 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) )
181 180 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) )
182 181 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) )
183 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → 𝐾 ∈ ℂ )
184 1cnd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → 1 ∈ ℂ )
185 184 halfcld ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 1 / 2 ) ∈ ℂ )
186 183 185 addcld ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 𝐾 + ( 1 / 2 ) ) ∈ ℂ )
187 15 a1i ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → π ∈ ℂ )
188 186 187 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ )
189 sinper ⊢ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
190 188 72 189 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( ( 𝑁 / 2 ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
191 182 190 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
192 50 107 mulcld ⊢ ( 𝜑 → ( 2 · π ) ∈ ℂ )
193 151 107 mulcld ⊢ ( 𝜑 → ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ )
194 193 sincld ⊢ ( 𝜑 → ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ∈ ℂ )
195 192 194 mulcomd ⊢ ( 𝜑 → ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) )
196 195 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) )
197 191 196 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
198 94 a1i ⊢ ( 𝜑 → π ≠ 0 )
199 151 107 198 divcan4d ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) = ( 𝐾 + ( 1 / 2 ) ) )
200 2 zred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
201 69 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
202 201 rpreccld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ+ )
203 200 202 ltaddrpd ⊢ ( 𝜑 → 𝐾 < ( 𝐾 + ( 1 / 2 ) ) )
204 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
205 204 rehalfcld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
206 halflt1 ⊢ ( 1 / 2 ) < 1
207 206 a1i ⊢ ( 𝜑 → ( 1 / 2 ) < 1 )
208 205 204 200 207 ltadd2dd ⊢ ( 𝜑 → ( 𝐾 + ( 1 / 2 ) ) < ( 𝐾 + 1 ) )
209 btwnnz ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 < ( 𝐾 + ( 1 / 2 ) ) ∧ ( 𝐾 + ( 1 / 2 ) ) < ( 𝐾 + 1 ) ) → ¬ ( 𝐾 + ( 1 / 2 ) ) ∈ ℤ )
210 2 203 208 209 syl3anc ⊢ ( 𝜑 → ¬ ( 𝐾 + ( 1 / 2 ) ) ∈ ℤ )
211 199 210 eqneltrd ⊢ ( 𝜑 → ¬ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) ∈ ℤ )
212 sineq0 ⊢ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) = 0 ↔ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) ∈ ℤ ) )
213 193 212 syl ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) = 0 ↔ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) / π ) ∈ ℤ ) )
214 211 213 mtbird ⊢ ( 𝜑 → ¬ ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) = 0 )
215 214 neqned ⊢ ( 𝜑 → ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ≠ 0 )
216 50 107 52 198 mulne0d ⊢ ( 𝜑 → ( 2 · π ) ≠ 0 )
217 194 194 192 215 216 divdiv1d ⊢ ( 𝜑 → ( ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
218 194 215 dividd ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = 1 )
219 218 oveq1d ⊢ ( 𝜑 → ( ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( 1 / ( 2 · π ) ) )
220 217 219 eqtr3d ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) = ( 1 / ( 2 · π ) ) )
221 220 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) = ( 1 / ( 2 · π ) ) )
222 197 221 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( 1 / ( 2 · π ) ) )
223 169 173 222 3eqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( 1 / ( 2 · π ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
224 99 223 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
225 47 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) )
226 145 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → 𝑁 ∈ ℤ )
227 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ¬ ( 𝑁 mod 2 ) = 0 )
228 227 neqned ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 mod 2 ) ≠ 0 )
229 oddfl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 mod 2 ) ≠ 0 ) → 𝑁 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
230 226 228 229 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → 𝑁 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
231 230 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 1 ... 𝑁 ) = ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
232 231 sumeq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) )
233 fvoveq1 ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ⌊ ‘ ( 1 / 2 ) ) )
234 halffl ⊢ ( ⌊ ‘ ( 1 / 2 ) ) = 0
235 233 234 eqtrdi ⊢ ( 𝑁 = 1 → ( ⌊ ‘ ( 𝑁 / 2 ) ) = 0 )
236 235 oveq2d ⊢ ( 𝑁 = 1 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) = ( 2 · 0 ) )
237 2t0e0 ⊢ ( 2 · 0 ) = 0
238 236 237 eqtrdi ⊢ ( 𝑁 = 1 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) = 0 )
239 238 oveq1d ⊢ ( 𝑁 = 1 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) = ( 0 + 1 ) )
240 90 addid2i ⊢ ( 0 + 1 ) = 1
241 239 240 eqtrdi ⊢ ( 𝑁 = 1 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) = 1 )
242 241 oveq2d ⊢ ( 𝑁 = 1 → ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) = ( 1 ... 1 ) )
243 242 sumeq1d ⊢ ( 𝑁 = 1 → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) )
244 1z ⊢ 1 ∈ ℤ
245 coscl ⊢ ( π ∈ ℂ → ( cos ‘ π ) ∈ ℂ )
246 15 245 ax-mp ⊢ ( cos ‘ π ) ∈ ℂ
247 oveq2 ⊢ ( 𝑛 = 1 → ( π · 𝑛 ) = ( π · 1 ) )
248 15 mulid1i ⊢ ( π · 1 ) = π
249 247 248 eqtrdi ⊢ ( 𝑛 = 1 → ( π · 𝑛 ) = π )
250 249 fveq2d ⊢ ( 𝑛 = 1 → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π ) )
251 250 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ ( cos ‘ π ) ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π ) )
252 244 246 251 mp2an ⊢ Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π )
253 252 a1i ⊢ ( 𝑁 = 1 → Σ 𝑛 ∈ ( 1 ... 1 ) ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ π ) )
254 cospi ⊢ ( cos ‘ π ) = - 1
255 254 a1i ⊢ ( 𝑁 = 1 → ( cos ‘ π ) = - 1 )
256 243 253 255 3eqtrd ⊢ ( 𝑁 = 1 → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
257 256 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
258 2nn ⊢ 2 ∈ ℕ
259 258 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ∈ ℕ )
260 67 rehalfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℝ )
261 260 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
262 261 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
263 2div2e1 ⊢ ( 2 / 2 ) = 1
264 73 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ∈ ℝ )
265 67 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 𝑁 ∈ ℝ )
266 69 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ∈ ℝ+ )
267 neqne ⊢ ( ¬ 𝑁 = 1 → 𝑁 ≠ 1 )
268 nnne1ge2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → 2 ≤ 𝑁 )
269 1 267 268 syl2an ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 2 ≤ 𝑁 )
270 264 265 266 269 lediv1dd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 2 / 2 ) ≤ ( 𝑁 / 2 ) )
271 263 270 eqbrtrrid ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 1 ≤ ( 𝑁 / 2 ) )
272 260 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 𝑁 / 2 ) ∈ ℝ )
273 flge ⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ ( 𝑁 / 2 ) ↔ 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
274 272 244 273 sylancl ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 1 ≤ ( 𝑁 / 2 ) ↔ 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
275 271 274 mpbid ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
276 elnnz1 ⊢ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 1 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
277 262 275 276 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℕ )
278 259 277 nnmulcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ∈ ℕ )
279 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
280 278 279 eleqtrdi ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ∈ ( ℤ≥ ‘ 1 ) )
281 15 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → π ∈ ℂ )
282 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) → 𝑛 ∈ ℤ )
283 282 zcnd ⊢ ( 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) → 𝑛 ∈ ℂ )
284 283 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → 𝑛 ∈ ℂ )
285 281 284 mulcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → ( π · 𝑛 ) ∈ ℂ )
286 285 coscld ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) ∧ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) → ( cos ‘ ( π · 𝑛 ) ) ∈ ℂ )
287 oveq2 ⊢ ( 𝑛 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) → ( π · 𝑛 ) = ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
288 287 fveq2d ⊢ ( 𝑛 = ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) )
289 280 286 288 fsump1 ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) + ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) ) )
290 15 a1i ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → π ∈ ℂ )
291 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → 𝑛 ∈ ℤ )
292 291 zcnd ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → 𝑛 ∈ ℂ )
293 290 292 mulcomd ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → ( π · 𝑛 ) = ( 𝑛 · π ) )
294 293 fveq2d ⊢ ( 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) → ( cos ‘ ( π · 𝑛 ) ) = ( cos ‘ ( 𝑛 · π ) ) )
295 294 sumeq2i ⊢ Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( 𝑛 · π ) )
296 dirkertrigeqlem1 ⊢ ( ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℕ → Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )
297 277 296 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )
298 295 297 eqtrid ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) = 0 )
299 261 zcnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℂ )
300 50 299 mulcld ⊢ ( 𝜑 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ∈ ℂ )
301 107 300 109 adddid ⊢ ( 𝜑 → ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) = ( ( π · ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) + ( π · 1 ) ) )
302 107 50 299 mul13d ⊢ ( 𝜑 → ( π · ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) )
303 248 a1i ⊢ ( 𝜑 → ( π · 1 ) = π )
304 302 303 oveq12d ⊢ ( 𝜑 → ( ( π · ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) + ( π · 1 ) ) = ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) + π ) )
305 299 192 mulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ∈ ℂ )
306 305 107 addcomd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) + π ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
307 301 304 306 3eqtrd ⊢ ( 𝜑 → ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
308 307 fveq2d ⊢ ( 𝜑 → ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) = ( cos ‘ ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
309 cosper ⊢ ( ( π ∈ ℂ ∧ ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ) → ( cos ‘ ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
310 107 261 309 syl2anc ⊢ ( 𝜑 → ( cos ‘ ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
311 254 a1i ⊢ ( 𝜑 → ( cos ‘ π ) = - 1 )
312 308 310 311 3eqtrd ⊢ ( 𝜑 → ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) = - 1 )
313 312 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) = - 1 )
314 298 313 oveq12d ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) ) ( cos ‘ ( π · 𝑛 ) ) + ( cos ‘ ( π · ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ) ) = ( 0 + - 1 ) )
315 neg1cn ⊢ - 1 ∈ ℂ
316 315 addid2i ⊢ ( 0 + - 1 ) = - 1
317 316 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → ( 0 + - 1 ) = - 1 )
318 289 314 317 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 1 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
319 257 318 pm2.61dan ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
320 319 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
321 232 320 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) = - 1 )
322 321 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) = ( ( 1 / 2 ) + - 1 ) )
323 322 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( π · 𝑛 ) ) ) / π ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
324 168 172 eqtrd ⊢ ( 𝜑 → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
325 324 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) = ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
326 230 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 · π ) = ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) )
327 300 109 107 adddird ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) = ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + ( 1 · π ) ) )
328 107 mulid2d ⊢ ( 𝜑 → ( 1 · π ) = π )
329 328 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + ( 1 · π ) ) = ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + π ) )
330 300 107 mulcld ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ∈ ℂ )
331 330 107 addcomd ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) + π ) = ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) )
332 327 329 331 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) = ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) )
333 332 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) · π ) = ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) )
334 50 299 mulcomd ⊢ ( 𝜑 → ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · 2 ) )
335 334 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) = ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · 2 ) · π ) )
336 299 50 107 mulassd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · 2 ) · π ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) )
337 335 336 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) )
338 337 oveq2d ⊢ ( 𝜑 → ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
339 338 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( π + ( ( 2 · ( ⌊ ‘ ( 𝑁 / 2 ) ) ) · π ) ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
340 326 333 339 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( 𝑁 · π ) = ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
341 340 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
342 193 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ )
343 15 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → π ∈ ℂ )
344 305 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ∈ ℂ )
345 342 343 344 addassd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) = ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( π + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
346 341 345 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) = ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) )
347 346 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) = ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) )
348 347 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + ( 𝑁 · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
349 193 107 addcld ⊢ ( 𝜑 → ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ∈ ℂ )
350 sinper ⊢ ( ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ∈ ℂ ∧ ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ) → ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) )
351 349 261 350 syl2anc ⊢ ( 𝜑 → ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) )
352 sinppi ⊢ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) ∈ ℂ → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) = - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
353 193 352 syl ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) ) = - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
354 351 353 eqtrd ⊢ ( 𝜑 → ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) = - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) )
355 354 oveq1d ⊢ ( 𝜑 → ( ( sin ‘ ( ( ( ( 𝐾 + ( 1 / 2 ) ) · π ) + π ) + ( ( ⌊ ‘ ( 𝑁 / 2 ) ) · ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) )
356 195 oveq2d ⊢ ( 𝜑 → ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
357 194 194 215 divnegd ⊢ ( 𝜑 → - ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) )
358 218 negeqd ⊢ ( 𝜑 → - ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = - 1 )
359 357 358 eqtr3d ⊢ ( 𝜑 → ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) = - 1 )
360 359 oveq1d ⊢ ( 𝜑 → ( ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( - 1 / ( 2 · π ) ) )
361 194 negcld ⊢ ( 𝜑 → - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ∈ ℂ )
362 361 194 192 215 216 divdiv1d ⊢ ( 𝜑 → ( ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) ) / ( 2 · π ) ) = ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) )
363 86 90 negsubi ⊢ ( ( 1 / 2 ) + - 1 ) = ( ( 1 / 2 ) − 1 )
364 90 86 negsubdi2i ⊢ - ( 1 − ( 1 / 2 ) ) = ( ( 1 / 2 ) − 1 )
365 1mhlfehlf ⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
366 365 negeqi ⊢ - ( 1 − ( 1 / 2 ) ) = - ( 1 / 2 )
367 divneg ⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 1 / 2 ) = ( - 1 / 2 ) )
368 90 118 51 367 mp3an ⊢ - ( 1 / 2 ) = ( - 1 / 2 )
369 366 368 eqtri ⊢ - ( 1 − ( 1 / 2 ) ) = ( - 1 / 2 )
370 363 364 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 315 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 360 362 375 3eqtr3d ⊢ ( 𝜑 → ( - ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) / ( ( sin ‘ ( ( 𝐾 + ( 1 / 2 ) ) · π ) ) · ( 2 · π ) ) ) = ( ( ( 1 / 2 ) + - 1 ) / π ) )
377 355 356 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 325 348 378 3eqtrrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + - 1 ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
380 225 323 379 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 mod 2 ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
381 224 380 pm2.61dan ⊢ ( 𝜑 → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )