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

Metamath Proof Explorer

Theorem dirkercncflem2

Description: Lemma used to prove that the Dirichlet Kernel is continuous at Y points that are multiples of ( 2 x. _pi ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkercncflem2.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
dirkercncflem2.f ⊢ 𝐹 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
dirkercncflem2.g ⊢ 𝐺 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
dirkercncflem2.yne0 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
dirkercncflem2.h ⊢ 𝐻 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
dirkercncflem2.i ⊢ 𝐼 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
dirkercncflem2.l ⊢ 𝐿 = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) )
dirkercncflem2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dirkercncflem2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 (,) 𝐵 ) )
dirkercncflem2.ymod ⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) = 0 )
dirkercncflem2.11 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
Assertion dirkercncflem2 ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) limℂ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dirkercncflem2.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
2 dirkercncflem2.f ⊢ 𝐹 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
3 dirkercncflem2.g ⊢ 𝐺 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
4 dirkercncflem2.yne0 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
5 dirkercncflem2.h ⊢ 𝐻 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
6 dirkercncflem2.i ⊢ 𝐼 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
7 dirkercncflem2.l ⊢ 𝐿 = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) )
8 dirkercncflem2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 dirkercncflem2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 (,) 𝐵 ) )
10 dirkercncflem2.ymod ⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) = 0 )
11 dirkercncflem2.11 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
12 difss ⊢ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ( 𝐴 (,) 𝐵 )
13 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
14 12 13 sstri ⊢ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ
15 14 a1i ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑁 ∈ ℕ )
17 16 nnred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑁 ∈ ℝ )
18 halfre ⊢ ( 1 / 2 ) ∈ ℝ
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 1 / 2 ) ∈ ℝ )
20 17 19 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
21 15 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑦 ∈ ℝ )
22 20 21 remulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℝ )
23 22 resincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℝ )
24 23 2 fmptd ⊢ ( 𝜑 → 𝐹 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℝ )
25 2re ⊢ 2 ∈ ℝ
26 pire ⊢ π ∈ ℝ
27 25 26 remulcli ⊢ ( 2 · π ) ∈ ℝ
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 2 · π ) ∈ ℝ )
29 21 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 / 2 ) ∈ ℝ )
30 29 resincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℝ )
31 28 30 remulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℝ )
32 31 3 fmptd ⊢ ( 𝜑 → 𝐺 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℝ )
33 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
34 33 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
35 eqid ⊢ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } )
36 2 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
37 36 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
38 resmpt ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
39 14 38 ax-mp ⊢ ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
40 39 eqcomi ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
41 40 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
42 41 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
43 ax-resscn ⊢ ℝ ⊆ ℂ
44 43 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
45 8 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
46 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
47 46 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
48 45 47 addcld ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
50 44 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
51 49 50 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ )
52 51 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℂ )
53 eqid ⊢ ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
54 52 53 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) : ℝ ⟶ ℂ )
55 ssid ⊢ ℝ ⊆ ℝ
56 55 14 pm3.2i ⊢ ( ℝ ⊆ ℝ ∧ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ )
57 56 a1i ⊢ ( 𝜑 → ( ℝ ⊆ ℝ ∧ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ ) )
58 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
59 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
60 58 59 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
61 44 54 57 60 syl21anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
62 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
63 rehaus ⊢ ( topGen ‘ ran (,) ) ∈ Haus
64 9 elioored ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
65 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
66 65 sncld ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Haus ∧ 𝑌 ∈ ℝ ) → { 𝑌 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
67 63 64 66 sylancr ⊢ ( 𝜑 → { 𝑌 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
68 65 difopn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ∧ { 𝑌 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∈ ( topGen ‘ ran (,) ) )
69 33 67 68 sylancr ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∈ ( topGen ‘ ran (,) ) )
70 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
71 62 69 70 sylancr ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
72 71 reseq2d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
73 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
74 73 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
75 48 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
77 75 76 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ )
78 77 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℂ )
79 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
80 78 79 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) : ℂ ⟶ ℂ )
81 ssid ⊢ ℂ ⊆ ℂ
82 81 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
83 dvsinax ⊢ ( ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
84 48 83 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
85 84 dmeqd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = dom ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
86 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
87 77 coscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℂ )
88 75 87 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ∈ ℂ )
89 86 88 dmmptd ⊢ ( 𝜑 → dom ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ℂ )
90 85 89 eqtrd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ℂ )
91 43 90 sseqtrrid ⊢ ( 𝜑 → ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
92 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ) ) → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) )
93 74 80 82 91 92 syl22anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) )
94 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
95 43 94 mp1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
96 95 oveq2d ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ↾ ℝ ) ) = ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
97 84 reseq1d ⊢ ( 𝜑 → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) = ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) )
98 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
99 43 98 ax-mp ⊢ ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
100 97 99 eqtrdi ⊢ ( 𝜑 → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
101 93 96 100 3eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
102 101 reseq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
103 resmpt ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
104 14 103 mp1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
105 72 102 104 3eqtrd ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
106 42 61 105 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
107 5 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
108 107 eqcomd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) = 𝐻 )
109 37 106 108 3eqtrd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐻 )
110 109 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = dom 𝐻 )
111 21 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑦 ∈ ℂ )
112 111 88 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ∈ ℂ )
113 5 112 dmmptd ⊢ ( 𝜑 → dom 𝐻 = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
114 110 113 eqtr2d ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) = dom ( ℝ D 𝐹 ) )
115 eqimss ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) = dom ( ℝ D 𝐹 ) → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ dom ( ℝ D 𝐹 ) )
116 114 115 syl ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ dom ( ℝ D 𝐹 ) )
117 6 a1i ⊢ ( 𝜑 → 𝐼 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
118 resmpt ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
119 14 118 ax-mp ⊢ ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
120 119 eqcomi ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
121 120 oveq2i ⊢ ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
122 121 a1i ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
123 2cn ⊢ 2 ∈ ℂ
124 picn ⊢ π ∈ ℂ
125 123 124 mulcli ⊢ ( 2 · π ) ∈ ℂ
126 125 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 2 · π ) ∈ ℂ )
127 50 halfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 / 2 ) ∈ ℂ )
128 127 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
129 126 128 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ )
130 eqid ⊢ ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
131 129 130 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) : ℝ ⟶ ℂ )
132 58 59 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
133 44 131 57 132 syl21anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
134 71 reseq2d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
135 43 sseli ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
136 1cnd ⊢ ( 𝑦 ∈ ℂ → 1 ∈ ℂ )
137 2cnd ⊢ ( 𝑦 ∈ ℂ → 2 ∈ ℂ )
138 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
139 2ne0 ⊢ 2 ≠ 0
140 139 a1i ⊢ ( 𝑦 ∈ ℂ → 2 ≠ 0 )
141 136 137 138 140 div13d ⊢ ( 𝑦 ∈ ℂ → ( ( 1 / 2 ) · 𝑦 ) = ( ( 𝑦 / 2 ) · 1 ) )
142 halfcl ⊢ ( 𝑦 ∈ ℂ → ( 𝑦 / 2 ) ∈ ℂ )
143 142 mulridd ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 / 2 ) · 1 ) = ( 𝑦 / 2 ) )
144 141 143 eqtrd ⊢ ( 𝑦 ∈ ℂ → ( ( 1 / 2 ) · 𝑦 ) = ( 𝑦 / 2 ) )
145 144 fveq2d ⊢ ( 𝑦 ∈ ℂ → ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) = ( sin ‘ ( 𝑦 / 2 ) ) )
146 145 oveq2d ⊢ ( 𝑦 ∈ ℂ → ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
147 146 eqcomd ⊢ ( 𝑦 ∈ ℂ → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) )
148 135 147 syl ⊢ ( 𝑦 ∈ ℝ → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) )
149 148 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) )
150 149 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) )
151 150 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) )
152 125 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 2 · π ) ∈ ℂ )
153 46 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 1 / 2 ) ∈ ℂ )
154 153 76 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 1 / 2 ) · 𝑦 ) ∈ ℂ )
155 154 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ∈ ℂ )
156 152 155 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ∈ ℂ )
157 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) )
158 156 157 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) : ℂ ⟶ ℂ )
159 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
160 124 a1i ⊢ ( 𝜑 → π ∈ ℂ )
161 159 160 mulcld ⊢ ( 𝜑 → ( 2 · π ) ∈ ℂ )
162 dvasinbx ⊢ ( ( ( 2 · π ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( 2 · π ) · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) )
163 161 46 162 sylancl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( 2 · π ) · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) )
164 2cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 2 ∈ ℂ )
165 124 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → π ∈ ℂ )
166 164 165 153 mul32d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 2 · π ) · ( 1 / 2 ) ) = ( ( 2 · ( 1 / 2 ) ) · π ) )
167 139 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 2 ≠ 0 )
168 164 167 recidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 2 · ( 1 / 2 ) ) = 1 )
169 168 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 2 · ( 1 / 2 ) ) · π ) = ( 1 · π ) )
170 165 mullidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 1 · π ) = π )
171 166 169 170 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 2 · π ) · ( 1 / 2 ) ) = π )
172 144 fveq2d ⊢ ( 𝑦 ∈ ℂ → ( cos ‘ ( ( 1 / 2 ) · 𝑦 ) ) = ( cos ‘ ( 𝑦 / 2 ) ) )
173 172 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( ( 1 / 2 ) · 𝑦 ) ) = ( cos ‘ ( 𝑦 / 2 ) ) )
174 171 173 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( ( 2 · π ) · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) = ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
175 174 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( ( ( 2 · π ) · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
176 163 175 eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
177 176 dmeqd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = dom ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
178 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
179 76 halfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 / 2 ) ∈ ℂ )
180 179 coscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
181 165 180 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ )
182 178 181 dmmptd ⊢ ( 𝜑 → dom ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) = ℂ )
183 177 182 eqtrd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = ℂ )
184 43 183 sseqtrrid ⊢ ( 𝜑 → ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) )
185 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) ) ) → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) ↾ ℝ ) )
186 74 158 82 184 185 syl22anc ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) ↾ ℝ ) )
187 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) )
188 43 187 mp1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) )
189 188 oveq2d ⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ↾ ℝ ) ) = ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) )
190 176 reseq1d ⊢ ( 𝜑 → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) ↾ ℝ ) = ( ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ↾ ℝ ) )
191 186 189 190 3eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ↾ ℝ ) )
192 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
193 43 192 ax-mp ⊢ ( ( 𝑦 ∈ ℂ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
194 191 193 eqtrdi ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( ( 1 / 2 ) · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
195 151 194 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
196 195 reseq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( ( 𝑦 ∈ ℝ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
197 15 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
198 134 196 197 3eqtrd ⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
199 122 133 198 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
200 199 eqcomd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) = ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
201 3 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
202 201 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
203 202 eqcomd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ℝ D 𝐺 ) )
204 117 200 203 3eqtrrd ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = 𝐼 )
205 204 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = dom 𝐼 )
206 111 181 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ )
207 6 206 dmmptd ⊢ ( 𝜑 → dom 𝐼 = ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
208 205 207 eqtr2d ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) = dom ( ℝ D 𝐺 ) )
209 eqimss ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) = dom ( ℝ D 𝐺 ) → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ dom ( ℝ D 𝐺 ) )
210 208 209 syl ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ dom ( ℝ D 𝐺 ) )
211 111 77 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ )
212 211 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ )
213 eqid ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) )
214 213 fnmpt ⊢ ( ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) Fn ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
215 212 214 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) Fn ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
216 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
217 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
218 217 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ 𝑦 = 𝑤 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
219 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
220 45 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑁 ∈ ℂ )
221 1cnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 1 ∈ ℂ )
222 221 halfcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 1 / 2 ) ∈ ℂ )
223 220 222 addcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
224 eldifi ⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 𝑤 ∈ ( 𝐴 (,) 𝐵 ) )
225 224 elioored ⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 𝑤 ∈ ℝ )
226 225 recnd ⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 𝑤 ∈ ℂ )
227 226 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑤 ∈ ℂ )
228 223 227 mulcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ ℂ )
229 216 218 219 228 fvmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
230 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↔ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
231 230 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ↔ ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) )
232 oveq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 mod ( 2 · π ) ) = ( 𝑤 mod ( 2 · π ) ) )
233 232 neeq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 mod ( 2 · π ) ) ≠ 0 ↔ ( 𝑤 mod ( 2 · π ) ) ≠ 0 ) )
234 231 233 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 mod ( 2 · π ) ) ≠ 0 ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑤 mod ( 2 · π ) ) ≠ 0 ) ) )
235 eldifi ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
236 elioore ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → 𝑦 ∈ ℝ )
237 235 236 135 3syl ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 𝑦 ∈ ℂ )
238 2cnd ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 2 ∈ ℂ )
239 124 a1i ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → π ∈ ℂ )
240 139 a1i ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → 2 ≠ 0 )
241 0re ⊢ 0 ∈ ℝ
242 pipos ⊢ 0 < π
243 241 242 gtneii ⊢ π ≠ 0
244 243 a1i ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → π ≠ 0 )
245 237 238 239 240 244 divdiv1d ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( ( 𝑦 / 2 ) / π ) = ( 𝑦 / ( 2 · π ) ) )
246 245 eqcomd ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( 𝑦 / ( 2 · π ) ) = ( ( 𝑦 / 2 ) / π ) )
247 246 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 / ( 2 · π ) ) = ( ( 𝑦 / 2 ) / π ) )
248 4 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( sin ‘ ( 𝑦 / 2 ) ) = 0 )
249 111 halfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 / 2 ) ∈ ℂ )
250 sineq0 ⊢ ( ( 𝑦 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝑦 / 2 ) ) = 0 ↔ ( ( 𝑦 / 2 ) / π ) ∈ ℤ ) )
251 249 250 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( sin ‘ ( 𝑦 / 2 ) ) = 0 ↔ ( ( 𝑦 / 2 ) / π ) ∈ ℤ ) )
252 248 251 mtbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( ( 𝑦 / 2 ) / π ) ∈ ℤ )
253 247 252 eqneltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( 𝑦 / ( 2 · π ) ) ∈ ℤ )
254 2rp ⊢ 2 ∈ ℝ+
255 pirp ⊢ π ∈ ℝ+
256 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
257 254 255 256 mp2an ⊢ ( 2 · π ) ∈ ℝ+
258 mod0 ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑦 mod ( 2 · π ) ) = 0 ↔ ( 𝑦 / ( 2 · π ) ) ∈ ℤ ) )
259 21 257 258 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑦 mod ( 2 · π ) ) = 0 ↔ ( 𝑦 / ( 2 · π ) ) ∈ ℤ ) )
260 253 259 mtbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( 𝑦 mod ( 2 · π ) ) = 0 )
261 260 neqned ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 mod ( 2 · π ) ) ≠ 0 )
262 234 261 chvarvv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑤 mod ( 2 · π ) ) ≠ 0 )
263 262 neneqd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( 𝑤 mod ( 2 · π ) ) = 0 )
264 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → 𝜑 )
265 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) )
266 226 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → 𝑤 ∈ ℂ )
267 64 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
268 267 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → 𝑌 ∈ ℂ )
269 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
270 8 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
271 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
272 271 rehalfcld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
273 270 272 readdcld ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
274 8 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
275 254 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
276 275 rpreccld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ+ )
277 270 276 ltaddrpd ⊢ ( 𝜑 → 𝑁 < ( 𝑁 + ( 1 / 2 ) ) )
278 269 270 273 274 277 lttrd ⊢ ( 𝜑 → 0 < ( 𝑁 + ( 1 / 2 ) ) )
279 278 gt0ne0d ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ≠ 0 )
280 48 279 jca ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ ∧ ( 𝑁 + ( 1 / 2 ) ) ≠ 0 ) )
281 280 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → ( ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ ∧ ( 𝑁 + ( 1 / 2 ) ) ≠ 0 ) )
282 mulcan ⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ( ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ ∧ ( 𝑁 + ( 1 / 2 ) ) ≠ 0 ) ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ↔ 𝑤 = 𝑌 ) )
283 266 268 281 282 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ↔ 𝑤 = 𝑌 ) )
284 265 283 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → 𝑤 = 𝑌 )
285 oveq1 ⊢ ( 𝑤 = 𝑌 → ( 𝑤 mod ( 2 · π ) ) = ( 𝑌 mod ( 2 · π ) ) )
286 285 10 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑌 ) → ( 𝑤 mod ( 2 · π ) ) = 0 )
287 264 284 286 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) → ( 𝑤 mod ( 2 · π ) ) = 0 )
288 263 287 mtand ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) )
289 48 267 mulcld ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ∈ ℂ )
290 289 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ∈ ℂ )
291 elsn2g ⊢ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ∈ ℂ → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ↔ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) )
292 290 291 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ↔ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) )
293 288 292 mtbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } )
294 228 293 eldifd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ ( ℂ ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
295 229 294 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ∈ ( ℂ ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
296 sinf ⊢ sin : ℂ ⟶ ℂ
297 296 fdmi ⊢ dom sin = ℂ
298 297 eqcomi ⊢ ℂ = dom sin
299 298 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ℂ = dom sin )
300 299 difeq1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ℂ ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) = ( dom sin ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
301 295 300 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ∈ ( dom sin ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
302 301 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ∈ ( dom sin ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
303 fnfvrnss ⊢ ( ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) Fn ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ∀ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ∈ ( dom sin ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) ) → ran ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ⊆ ( dom sin ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
304 215 302 303 syl2anc ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ⊆ ( dom sin ∖ { ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) } ) )
305 uncom ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
306 305 a1i ⊢ ( 𝜑 → ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
307 9 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ ( 𝐴 (,) 𝐵 ) )
308 undif ⊢ ( { 𝑌 } ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝐴 (,) 𝐵 ) )
309 307 308 sylib ⊢ ( 𝜑 → ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝐴 (,) 𝐵 ) )
310 306 309 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( 𝐴 (,) 𝐵 ) )
311 310 mpteq1d ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) )
312 iftrue ⊢ ( 𝑤 = 𝑌 → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) )
313 oveq2 ⊢ ( 𝑤 = 𝑌 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) )
314 312 313 eqtr4d ⊢ ( 𝑤 = 𝑌 → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
315 314 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
316 iffalse ⊢ ( ¬ 𝑤 = 𝑌 → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) )
317 316 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) )
318 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
319 oveq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
320 319 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
321 simpl ⊢ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ∧ ¬ 𝑤 = 𝑌 ) → 𝑤 ∈ ( 𝐴 (,) 𝐵 ) )
322 id ⊢ ( ¬ 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌 )
323 velsn ⊢ ( 𝑤 ∈ { 𝑌 } ↔ 𝑤 = 𝑌 )
324 322 323 sylnibr ⊢ ( ¬ 𝑤 = 𝑌 → ¬ 𝑤 ∈ { 𝑌 } )
325 324 adantl ⊢ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ∧ ¬ 𝑤 = 𝑌 ) → ¬ 𝑤 ∈ { 𝑌 } )
326 321 325 eldifd ⊢ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ∧ ¬ 𝑤 = 𝑌 ) → 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
327 326 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
328 48 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
329 elioore ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → 𝑤 ∈ ℝ )
330 329 recnd ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → 𝑤 ∈ ℂ )
331 330 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑤 ∈ ℂ )
332 328 331 mulcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ ℂ )
333 332 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ∈ ℂ )
334 318 320 327 333 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
335 317 334 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
336 315 335 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
337 336 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
338 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
339 resmpt ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ → ( ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
340 338 339 ax-mp ⊢ ( ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
341 eqid ⊢ ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) = ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
342 341 mulc1cncf ⊢ ( ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ℂ –cn→ ℂ ) )
343 48 342 syl ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ℂ –cn→ ℂ ) )
344 58 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
345 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
346 345 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
347 344 346 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
348 347 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
349 58 348 348 cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
350 81 82 349 sylancr ⊢ ( 𝜑 → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
351 343 350 eleqtrd ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
352 13 44 sstrid ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
353 345 cnrest ⊢ ( ( ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
354 351 352 353 syl2anc ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℂ ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
355 340 354 eqeltrrid ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
356 58 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
357 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
358 356 352 357 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
359 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
360 358 356 359 sylancl ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
361 355 360 mpbid ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
362 361 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
363 fveq2 ⊢ ( 𝑦 = 𝑌 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
364 363 eleq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
365 364 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ∧ 𝑌 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
366 362 9 365 syl2anc ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
367 337 366 eqeltrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
368 310 eqcomd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) = ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) )
369 368 oveq2d ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) )
370 369 oveq1d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) )
371 370 fveq1d ⊢ ( 𝜑 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
372 367 371 eleqtrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
373 311 372 eqeltrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
374 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) )
375 eqid ⊢ ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) )
376 211 213 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
377 15 43 sstrdi ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℂ )
378 374 58 375 376 377 267 ellimc ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) limℂ 𝑌 ) ↔ ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
379 373 378 mpbird ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) limℂ 𝑌 ) )
380 139 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
381 243 a1i ⊢ ( 𝜑 → π ≠ 0 )
382 159 160 380 381 mulne0d ⊢ ( 𝜑 → ( 2 · π ) ≠ 0 )
383 267 161 382 divcan1d ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) = 𝑌 )
384 383 eqcomd ⊢ ( 𝜑 → 𝑌 = ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) )
385 384 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) ) )
386 385 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) ) ) )
387 267 161 382 divcld ⊢ ( 𝜑 → ( 𝑌 / ( 2 · π ) ) ∈ ℂ )
388 48 387 161 mul12d ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) ) = ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) ) )
389 48 159 160 mulassd ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) · π ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) )
390 389 eqcomd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) · π ) )
391 390 oveq2d ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) ) = ( ( 𝑌 / ( 2 · π ) ) · ( ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) · π ) ) )
392 45 47 159 adddird ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) = ( ( 𝑁 · 2 ) + ( ( 1 / 2 ) · 2 ) ) )
393 159 380 recid2d ⊢ ( 𝜑 → ( ( 1 / 2 ) · 2 ) = 1 )
394 393 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 · 2 ) + ( ( 1 / 2 ) · 2 ) ) = ( ( 𝑁 · 2 ) + 1 ) )
395 392 394 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) = ( ( 𝑁 · 2 ) + 1 ) )
396 395 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) · π ) = ( ( ( 𝑁 · 2 ) + 1 ) · π ) )
397 396 oveq2d ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( ( ( 𝑁 + ( 1 / 2 ) ) · 2 ) · π ) ) = ( ( 𝑌 / ( 2 · π ) ) · ( ( ( 𝑁 · 2 ) + 1 ) · π ) ) )
398 388 391 397 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) ) = ( ( 𝑌 / ( 2 · π ) ) · ( ( ( 𝑁 · 2 ) + 1 ) · π ) ) )
399 45 159 mulcld ⊢ ( 𝜑 → ( 𝑁 · 2 ) ∈ ℂ )
400 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
401 399 400 addcld ⊢ ( 𝜑 → ( ( 𝑁 · 2 ) + 1 ) ∈ ℂ )
402 387 401 160 mulassd ⊢ ( 𝜑 → ( ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) · π ) = ( ( 𝑌 / ( 2 · π ) ) · ( ( ( 𝑁 · 2 ) + 1 ) · π ) ) )
403 398 402 eqtr4d ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) ) = ( ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) · π ) )
404 403 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) · π ) ) )
405 mod0 ⊢ ( ( 𝑌 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑌 mod ( 2 · π ) ) = 0 ↔ ( 𝑌 / ( 2 · π ) ) ∈ ℤ ) )
406 64 257 405 sylancl ⊢ ( 𝜑 → ( ( 𝑌 mod ( 2 · π ) ) = 0 ↔ ( 𝑌 / ( 2 · π ) ) ∈ ℤ ) )
407 10 406 mpbid ⊢ ( 𝜑 → ( 𝑌 / ( 2 · π ) ) ∈ ℤ )
408 8 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
409 2z ⊢ 2 ∈ ℤ
410 409 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
411 408 410 zmulcld ⊢ ( 𝜑 → ( 𝑁 · 2 ) ∈ ℤ )
412 411 peano2zd ⊢ ( 𝜑 → ( ( 𝑁 · 2 ) + 1 ) ∈ ℤ )
413 407 412 zmulcld ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) ∈ ℤ )
414 sinkpi ⊢ ( ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) ∈ ℤ → ( sin ‘ ( ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) · π ) ) = 0 )
415 413 414 syl ⊢ ( 𝜑 → ( sin ‘ ( ( ( 𝑌 / ( 2 · π ) ) · ( ( 𝑁 · 2 ) + 1 ) ) · π ) ) = 0 )
416 386 404 415 3eqtrd ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) = 0 )
417 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
418 417 a1i ⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
419 418 289 cnlimci ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ∈ ( sin limℂ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) )
420 416 419 eqeltrrd ⊢ ( 𝜑 → 0 ∈ ( sin limℂ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) )
421 304 379 420 limccog ⊢ ( 𝜑 → 0 ∈ ( ( sin ∘ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) limℂ 𝑌 ) )
422 2 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝐹 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
423 218 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ 𝑦 = 𝑤 ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
424 228 sincld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ℂ )
425 422 423 219 424 fvmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐹 ‘ 𝑤 ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
426 229 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
427 425 426 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐹 ‘ 𝑤 ) = ( sin ‘ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) )
428 427 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( 𝐹 ‘ 𝑤 ) ) = ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) )
429 24 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( 𝐹 ‘ 𝑤 ) ) )
430 fcompt ⊢ ( ( sin : ℂ ⟶ ℂ ∧ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ ) → ( sin ∘ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) )
431 296 376 430 sylancr ⊢ ( 𝜑 → ( sin ∘ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) )
432 428 429 431 3eqtr4rd ⊢ ( 𝜑 → ( sin ∘ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = 𝐹 )
433 432 oveq1d ⊢ ( 𝜑 → ( ( sin ∘ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) limℂ 𝑌 ) = ( 𝐹 limℂ 𝑌 ) )
434 421 433 eleqtrd ⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝑌 ) )
435 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → 𝑤 = 𝑌 )
436 435 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) = 0 )
437 267 159 161 380 382 divdiv32d ⊢ ( 𝜑 → ( ( 𝑌 / 2 ) / ( 2 · π ) ) = ( ( 𝑌 / ( 2 · π ) ) / 2 ) )
438 437 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 / 2 ) / ( 2 · π ) ) · ( 2 · π ) ) = ( ( ( 𝑌 / ( 2 · π ) ) / 2 ) · ( 2 · π ) ) )
439 267 halfcld ⊢ ( 𝜑 → ( 𝑌 / 2 ) ∈ ℂ )
440 439 161 382 divcan1d ⊢ ( 𝜑 → ( ( ( 𝑌 / 2 ) / ( 2 · π ) ) · ( 2 · π ) ) = ( 𝑌 / 2 ) )
441 387 159 161 380 div32d ⊢ ( 𝜑 → ( ( ( 𝑌 / ( 2 · π ) ) / 2 ) · ( 2 · π ) ) = ( ( 𝑌 / ( 2 · π ) ) · ( ( 2 · π ) / 2 ) ) )
442 160 159 380 divcan3d ⊢ ( 𝜑 → ( ( 2 · π ) / 2 ) = π )
443 442 oveq2d ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( ( 2 · π ) / 2 ) ) = ( ( 𝑌 / ( 2 · π ) ) · π ) )
444 441 443 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 / ( 2 · π ) ) / 2 ) · ( 2 · π ) ) = ( ( 𝑌 / ( 2 · π ) ) · π ) )
445 438 440 444 3eqtr3d ⊢ ( 𝜑 → ( 𝑌 / 2 ) = ( ( 𝑌 / ( 2 · π ) ) · π ) )
446 445 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( 𝑌 / 2 ) ) = ( sin ‘ ( ( 𝑌 / ( 2 · π ) ) · π ) ) )
447 sinkpi ⊢ ( ( 𝑌 / ( 2 · π ) ) ∈ ℤ → ( sin ‘ ( ( 𝑌 / ( 2 · π ) ) · π ) ) = 0 )
448 407 447 syl ⊢ ( 𝜑 → ( sin ‘ ( ( 𝑌 / ( 2 · π ) ) · π ) ) = 0 )
449 446 448 eqtrd ⊢ ( 𝜑 → ( sin ‘ ( 𝑌 / 2 ) ) = 0 )
450 449 oveq2d ⊢ ( 𝜑 → ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) = ( ( 2 · π ) · 0 ) )
451 161 mul01d ⊢ ( 𝜑 → ( ( 2 · π ) · 0 ) = 0 )
452 450 451 eqtrd ⊢ ( 𝜑 → ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) = 0 )
453 452 eqcomd ⊢ ( 𝜑 → 0 = ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) )
454 453 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → 0 = ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) )
455 fvoveq1 ⊢ ( 𝑤 = 𝑌 → ( sin ‘ ( 𝑤 / 2 ) ) = ( sin ‘ ( 𝑌 / 2 ) ) )
456 455 oveq2d ⊢ ( 𝑤 = 𝑌 → ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) )
457 456 eqcomd ⊢ ( 𝑤 = 𝑌 → ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
458 457 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
459 436 454 458 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
460 iffalse ⊢ ( ¬ 𝑤 = 𝑌 → if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) )
461 460 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) )
462 fvoveq1 ⊢ ( 𝑦 = 𝑤 → ( sin ‘ ( 𝑦 / 2 ) ) = ( sin ‘ ( 𝑤 / 2 ) ) )
463 462 oveq2d ⊢ ( 𝑦 = 𝑤 → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
464 125 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · π ) ∈ ℂ )
465 331 halfcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑤 / 2 ) ∈ ℂ )
466 465 sincld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑤 / 2 ) ) ∈ ℂ )
467 464 466 mulcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ∈ ℂ )
468 467 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ∈ ℂ )
469 3 463 327 468 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝐺 ‘ 𝑤 ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
470 461 469 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
471 459 470 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
472 471 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) )
473 eqid ⊢ ( 𝑤 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) = ( 𝑤 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
474 82 161 82 constcncfg ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( 2 · π ) ) ∈ ( ℂ –cn→ ℂ ) )
475 id ⊢ ( 𝑤 ∈ ℂ → 𝑤 ∈ ℂ )
476 2cnd ⊢ ( 𝑤 ∈ ℂ → 2 ∈ ℂ )
477 139 a1i ⊢ ( 𝑤 ∈ ℂ → 2 ≠ 0 )
478 475 476 477 divrec2d ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 / 2 ) = ( ( 1 / 2 ) · 𝑤 ) )
479 478 mpteq2ia ⊢ ( 𝑤 ∈ ℂ ↦ ( 𝑤 / 2 ) ) = ( 𝑤 ∈ ℂ ↦ ( ( 1 / 2 ) · 𝑤 ) )
480 eqid ⊢ ( 𝑤 ∈ ℂ ↦ ( ( 1 / 2 ) · 𝑤 ) ) = ( 𝑤 ∈ ℂ ↦ ( ( 1 / 2 ) · 𝑤 ) )
481 480 mulc1cncf ⊢ ( ( 1 / 2 ) ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( ( 1 / 2 ) · 𝑤 ) ) ∈ ( ℂ –cn→ ℂ ) )
482 46 481 ax-mp ⊢ ( 𝑤 ∈ ℂ ↦ ( ( 1 / 2 ) · 𝑤 ) ) ∈ ( ℂ –cn→ ℂ )
483 479 482 eqeltri ⊢ ( 𝑤 ∈ ℂ ↦ ( 𝑤 / 2 ) ) ∈ ( ℂ –cn→ ℂ )
484 483 a1i ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( 𝑤 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
485 418 484 cncfmpt1f ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( 𝑤 / 2 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
486 474 485 mulcncf ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
487 473 486 352 82 467 cncfmptssg ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
488 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
489 58 488 348 cncfcn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
490 352 81 489 sylancl ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
491 487 490 eleqtrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
492 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
493 358 356 492 sylancl ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
494 491 493 mpbid ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
495 494 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
496 363 eleq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
497 496 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ∧ 𝑌 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
498 495 9 497 syl2anc ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
499 472 498 eqeltrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
500 310 mpteq1d ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) )
501 369 eqcomd ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
502 501 oveq1d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) )
503 502 fveq1d ⊢ ( 𝜑 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
504 499 500 503 3eltr4d ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
505 eqid ⊢ ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) )
506 21 129 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ )
507 506 3 fmptd ⊢ ( 𝜑 → 𝐺 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
508 374 58 505 507 377 267 ellimc ⊢ ( 𝜑 → ( 0 ∈ ( 𝐺 limℂ 𝑌 ) ↔ ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , 0 , ( 𝐺 ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
509 504 508 mpbird ⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝑌 ) )
510 260 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝑦 mod ( 2 · π ) ) = 0 )
511 507 ffund ⊢ ( 𝜑 → Fun 𝐺 )
512 fvelima ⊢ ( ( Fun 𝐺 ∧ 0 ∈ ( 𝐺 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐺 ‘ 𝑦 ) = 0 )
513 511 512 sylan ⊢ ( ( 𝜑 ∧ 0 ∈ ( 𝐺 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐺 ‘ 𝑦 ) = 0 )
514 2cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 2 ∈ ℂ )
515 124 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → π ∈ ℂ )
516 139 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 2 ≠ 0 )
517 243 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → π ≠ 0 )
518 111 514 515 516 517 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝑦 / 2 ) / π ) = ( 𝑦 / ( 2 · π ) ) )
519 518 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝑦 / ( 2 · π ) ) = ( ( 𝑦 / 2 ) / π ) )
520 519 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝑦 / ( 2 · π ) ) = ( ( 𝑦 / 2 ) / π ) )
521 2cnd ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → 2 ∈ ℂ )
522 124 a1i ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → π ∈ ℂ )
523 521 522 mulcld ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 2 · π ) ∈ ℂ )
524 237 adantr ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → 𝑦 ∈ ℂ )
525 524 halfcld ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝑦 / 2 ) ∈ ℂ )
526 525 sincld ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
527 523 526 mulcld ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ )
528 3 fvmpt2 ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ ) → ( 𝐺 ‘ 𝑦 ) = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
529 527 528 syldan ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝐺 ‘ 𝑦 ) = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
530 529 eqcomd ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( 𝐺 ‘ 𝑦 ) )
531 simpr ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝐺 ‘ 𝑦 ) = 0 )
532 530 531 eqtrd ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = 0 )
533 125 a1i ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( 2 · π ) ∈ ℂ )
534 237 halfcld ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( 𝑦 / 2 ) ∈ ℂ )
535 534 sincld ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
536 533 535 mul0ord ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = 0 ↔ ( ( 2 · π ) = 0 ∨ ( sin ‘ ( 𝑦 / 2 ) ) = 0 ) ) )
537 536 adantr ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = 0 ↔ ( ( 2 · π ) = 0 ∨ ( sin ‘ ( 𝑦 / 2 ) ) = 0 ) ) )
538 532 537 mpbid ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( 2 · π ) = 0 ∨ ( sin ‘ ( 𝑦 / 2 ) ) = 0 ) )
539 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
540 124 243 pm3.2i ⊢ ( π ∈ ℂ ∧ π ≠ 0 )
541 mulne0 ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( π ∈ ℂ ∧ π ≠ 0 ) ) → ( 2 · π ) ≠ 0 )
542 539 540 541 mp2an ⊢ ( 2 · π ) ≠ 0
543 542 neii ⊢ ¬ ( 2 · π ) = 0
544 pm2.53 ⊢ ( ( ( 2 · π ) = 0 ∨ ( sin ‘ ( 𝑦 / 2 ) ) = 0 ) → ( ¬ ( 2 · π ) = 0 → ( sin ‘ ( 𝑦 / 2 ) ) = 0 ) )
545 538 543 544 mpisyl ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( sin ‘ ( 𝑦 / 2 ) ) = 0 )
546 545 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( sin ‘ ( 𝑦 / 2 ) ) = 0 )
547 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → 𝑦 ∈ ℂ )
548 547 halfcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝑦 / 2 ) ∈ ℂ )
549 548 250 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( sin ‘ ( 𝑦 / 2 ) ) = 0 ↔ ( ( 𝑦 / 2 ) / π ) ∈ ℤ ) )
550 546 549 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( 𝑦 / 2 ) / π ) ∈ ℤ )
551 520 550 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝑦 / ( 2 · π ) ) ∈ ℤ )
552 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → 𝑦 ∈ ℝ )
553 552 257 258 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( ( 𝑦 mod ( 2 · π ) ) = 0 ↔ ( 𝑦 / ( 2 · π ) ) ∈ ℤ ) )
554 551 553 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ∧ ( 𝐺 ‘ 𝑦 ) = 0 ) → ( 𝑦 mod ( 2 · π ) ) = 0 )
555 554 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝐺 ‘ 𝑦 ) = 0 → ( 𝑦 mod ( 2 · π ) ) = 0 ) )
556 555 reximdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐺 ‘ 𝑦 ) = 0 → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝑦 mod ( 2 · π ) ) = 0 ) )
557 556 adantr ⊢ ( ( 𝜑 ∧ 0 ∈ ( 𝐺 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) → ( ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐺 ‘ 𝑦 ) = 0 → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝑦 mod ( 2 · π ) ) = 0 ) )
558 513 557 mpd ⊢ ( ( 𝜑 ∧ 0 ∈ ( 𝐺 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝑦 mod ( 2 · π ) ) = 0 )
559 510 558 mtand ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐺 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
560 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
561 6 fvmpt2 ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ ) → ( 𝐼 ‘ 𝑦 ) = ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
562 560 206 561 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐼 ‘ 𝑦 ) = ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
563 534 coscld ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) → ( cos ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
564 563 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
565 515 564 517 11 mulne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ≠ 0 )
566 562 565 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐼 ‘ 𝑦 ) ≠ 0 )
567 566 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ¬ ( 𝐼 ‘ 𝑦 ) = 0 )
568 567 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐼 ‘ 𝑦 ) = 0 )
569 206 6 fmptd ⊢ ( 𝜑 → 𝐼 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
570 569 ffund ⊢ ( 𝜑 → Fun 𝐼 )
571 fvelima ⊢ ( ( Fun 𝐼 ∧ 0 ∈ ( 𝐼 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐼 ‘ 𝑦 ) = 0 )
572 570 571 sylan ⊢ ( ( 𝜑 ∧ 0 ∈ ( 𝐼 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( 𝐼 ‘ 𝑦 ) = 0 )
573 568 572 mtand ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐼 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
574 204 imaeq1d ⊢ ( 𝜑 → ( ( ℝ D 𝐺 ) “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝐼 “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
575 573 574 neleqtrrd ⊢ ( 𝜑 → ¬ 0 ∈ ( ( ℝ D 𝐺 ) “ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
576 1 dirkerval2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) = if ( ( 𝑌 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) ) ) )
577 8 64 576 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) = if ( ( 𝑌 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) ) ) )
578 10 iftrued ⊢ ( 𝜑 → if ( ( 𝑌 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
579 7 a1i ⊢ ( 𝜑 → 𝐿 = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) ) )
580 iftrue ⊢ ( 𝑤 = 𝑌 → if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
581 580 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
582 159 45 mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
583 582 400 addcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
584 583 159 160 380 381 divdiv1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
585 584 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
586 582 400 159 380 divdird ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) )
587 45 159 380 divcan3d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
588 587 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) = ( 𝑁 + ( 1 / 2 ) ) )
589 586 588 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( 𝑁 + ( 1 / 2 ) ) )
590 589 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) = ( ( 𝑁 + ( 1 / 2 ) ) / π ) )
591 585 590 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( 𝑁 + ( 1 / 2 ) ) / π ) )
592 591 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( 𝑁 + ( 1 / 2 ) ) / π ) )
593 313 fveq2d ⊢ ( 𝑤 = 𝑌 → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) = ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) )
594 593 oveq2d ⊢ ( 𝑤 = 𝑌 → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) )
595 fvoveq1 ⊢ ( 𝑤 = 𝑌 → ( cos ‘ ( 𝑤 / 2 ) ) = ( cos ‘ ( 𝑌 / 2 ) ) )
596 595 oveq2d ⊢ ( 𝑤 = 𝑌 → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) = ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) )
597 594 596 oveq12d ⊢ ( 𝑤 = 𝑌 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) )
598 597 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) )
599 45 47 267 adddird ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) = ( ( 𝑁 · 𝑌 ) + ( ( 1 / 2 ) · 𝑌 ) ) )
600 400 159 267 380 div32d ⊢ ( 𝜑 → ( ( 1 / 2 ) · 𝑌 ) = ( 1 · ( 𝑌 / 2 ) ) )
601 439 mullidd ⊢ ( 𝜑 → ( 1 · ( 𝑌 / 2 ) ) = ( 𝑌 / 2 ) )
602 600 601 eqtrd ⊢ ( 𝜑 → ( ( 1 / 2 ) · 𝑌 ) = ( 𝑌 / 2 ) )
603 602 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 · 𝑌 ) + ( ( 1 / 2 ) · 𝑌 ) ) = ( ( 𝑁 · 𝑌 ) + ( 𝑌 / 2 ) ) )
604 45 267 mulcld ⊢ ( 𝜑 → ( 𝑁 · 𝑌 ) ∈ ℂ )
605 604 439 addcomd ⊢ ( 𝜑 → ( ( 𝑁 · 𝑌 ) + ( 𝑌 / 2 ) ) = ( ( 𝑌 / 2 ) + ( 𝑁 · 𝑌 ) ) )
606 599 603 605 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) = ( ( 𝑌 / 2 ) + ( 𝑁 · 𝑌 ) ) )
607 606 fveq2d ⊢ ( 𝜑 → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) = ( cos ‘ ( ( 𝑌 / 2 ) + ( 𝑁 · 𝑌 ) ) ) )
608 604 161 382 divcan1d ⊢ ( 𝜑 → ( ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) · ( 2 · π ) ) = ( 𝑁 · 𝑌 ) )
609 608 eqcomd ⊢ ( 𝜑 → ( 𝑁 · 𝑌 ) = ( ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) · ( 2 · π ) ) )
610 609 oveq2d ⊢ ( 𝜑 → ( ( 𝑌 / 2 ) + ( 𝑁 · 𝑌 ) ) = ( ( 𝑌 / 2 ) + ( ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) · ( 2 · π ) ) ) )
611 610 fveq2d ⊢ ( 𝜑 → ( cos ‘ ( ( 𝑌 / 2 ) + ( 𝑁 · 𝑌 ) ) ) = ( cos ‘ ( ( 𝑌 / 2 ) + ( ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) · ( 2 · π ) ) ) ) )
612 45 267 161 382 divassd ⊢ ( 𝜑 → ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) = ( 𝑁 · ( 𝑌 / ( 2 · π ) ) ) )
613 408 407 zmulcld ⊢ ( 𝜑 → ( 𝑁 · ( 𝑌 / ( 2 · π ) ) ) ∈ ℤ )
614 612 613 eqeltrd ⊢ ( 𝜑 → ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) ∈ ℤ )
615 cosper ⊢ ( ( ( 𝑌 / 2 ) ∈ ℂ ∧ ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) ∈ ℤ ) → ( cos ‘ ( ( 𝑌 / 2 ) + ( ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) · ( 2 · π ) ) ) ) = ( cos ‘ ( 𝑌 / 2 ) ) )
616 439 614 615 syl2anc ⊢ ( 𝜑 → ( cos ‘ ( ( 𝑌 / 2 ) + ( ( ( 𝑁 · 𝑌 ) / ( 2 · π ) ) · ( 2 · π ) ) ) ) = ( cos ‘ ( 𝑌 / 2 ) ) )
617 607 611 616 3eqtrd ⊢ ( 𝜑 → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) = ( cos ‘ ( 𝑌 / 2 ) ) )
618 617 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( 𝑌 / 2 ) ) ) )
619 618 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( 𝑌 / 2 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) )
620 439 coscld ⊢ ( 𝜑 → ( cos ‘ ( 𝑌 / 2 ) ) ∈ ℂ )
621 267 159 160 380 381 divdiv1d ⊢ ( 𝜑 → ( ( 𝑌 / 2 ) / π ) = ( 𝑌 / ( 2 · π ) ) )
622 621 407 eqeltrd ⊢ ( 𝜑 → ( ( 𝑌 / 2 ) / π ) ∈ ℤ )
623 622 zred ⊢ ( 𝜑 → ( ( 𝑌 / 2 ) / π ) ∈ ℝ )
624 623 276 ltaddrpd ⊢ ( 𝜑 → ( ( 𝑌 / 2 ) / π ) < ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) )
625 halflt1 ⊢ ( 1 / 2 ) < 1
626 625 a1i ⊢ ( 𝜑 → ( 1 / 2 ) < 1 )
627 272 271 623 626 ltadd2dd ⊢ ( 𝜑 → ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) < ( ( ( 𝑌 / 2 ) / π ) + 1 ) )
628 btwnnz ⊢ ( ( ( ( 𝑌 / 2 ) / π ) ∈ ℤ ∧ ( ( 𝑌 / 2 ) / π ) < ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) ∧ ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) < ( ( ( 𝑌 / 2 ) / π ) + 1 ) ) → ¬ ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) ∈ ℤ )
629 622 624 627 628 syl3anc ⊢ ( 𝜑 → ¬ ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) ∈ ℤ )
630 coseq0 ⊢ ( ( 𝑌 / 2 ) ∈ ℂ → ( ( cos ‘ ( 𝑌 / 2 ) ) = 0 ↔ ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) ∈ ℤ ) )
631 439 630 syl ⊢ ( 𝜑 → ( ( cos ‘ ( 𝑌 / 2 ) ) = 0 ↔ ( ( ( 𝑌 / 2 ) / π ) + ( 1 / 2 ) ) ∈ ℤ ) )
632 629 631 mtbird ⊢ ( 𝜑 → ¬ ( cos ‘ ( 𝑌 / 2 ) ) = 0 )
633 632 neqned ⊢ ( 𝜑 → ( cos ‘ ( 𝑌 / 2 ) ) ≠ 0 )
634 48 160 620 381 633 divcan5rd ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( 𝑌 / 2 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) / π ) )
635 619 634 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) / π ) )
636 635 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) ) / ( π · ( cos ‘ ( 𝑌 / 2 ) ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) / π ) )
637 598 636 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( ( 𝑁 + ( 1 / 2 ) ) / π ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) )
638 581 592 637 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) )
639 iffalse ⊢ ( ¬ 𝑤 = 𝑌 → if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) = ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) )
640 639 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) = ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) )
641 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) )
642 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑤 ) )
643 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐼 ‘ 𝑦 ) = ( 𝐼 ‘ 𝑤 ) )
644 642 643 oveq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) = ( ( 𝐻 ‘ 𝑤 ) / ( 𝐼 ‘ 𝑤 ) ) )
645 644 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) = ( ( 𝐻 ‘ 𝑤 ) / ( 𝐼 ‘ 𝑤 ) ) )
646 112 5 fmptd ⊢ ( 𝜑 → 𝐻 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
647 646 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → 𝐻 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
648 647 327 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝐻 ‘ 𝑤 ) ∈ ℂ )
649 569 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → 𝐼 : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
650 649 327 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝐼 ‘ 𝑤 ) ∈ ℂ )
651 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → 𝐼 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
652 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
653 652 fvoveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → ( cos ‘ ( 𝑦 / 2 ) ) = ( cos ‘ ( 𝑤 / 2 ) ) )
654 653 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) = ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) )
655 124 a1i ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → π ∈ ℂ )
656 330 halfcld ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑤 / 2 ) ∈ ℂ )
657 656 coscld ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( 𝑤 / 2 ) ) ∈ ℂ )
658 655 657 mulcld ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ ℂ )
659 658 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ ℂ )
660 651 654 327 659 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝐼 ‘ 𝑤 ) = ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) )
661 540 a1i ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( π ∈ ℂ ∧ π ≠ 0 ) )
662 657 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( cos ‘ ( 𝑤 / 2 ) ) ∈ ℂ )
663 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → 𝜑 )
664 fvoveq1 ⊢ ( 𝑦 = 𝑤 → ( cos ‘ ( 𝑦 / 2 ) ) = ( cos ‘ ( 𝑤 / 2 ) ) )
665 664 neeq1d ⊢ ( 𝑦 = 𝑤 → ( ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ↔ ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 ) )
666 231 665 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 ) ) )
667 666 11 chvarvv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 )
668 663 327 667 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 )
669 mulne0 ⊢ ( ( ( π ∈ ℂ ∧ π ≠ 0 ) ∧ ( ( cos ‘ ( 𝑤 / 2 ) ) ∈ ℂ ∧ ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 ) ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ≠ 0 )
670 661 662 668 669 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ≠ 0 )
671 660 670 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝐼 ‘ 𝑤 ) ≠ 0 )
672 648 650 671 divcld ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 𝐻 ‘ 𝑤 ) / ( 𝐼 ‘ 𝑤 ) ) ∈ ℂ )
673 641 645 327 672 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) = ( ( 𝐻 ‘ 𝑤 ) / ( 𝐼 ‘ 𝑤 ) ) )
674 5 a1i ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → 𝐻 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ) )
675 320 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
676 675 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) ∧ 𝑦 = 𝑤 ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) )
677 332 coscld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ∈ ℂ )
678 328 677 mulcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) ∈ ℂ )
679 678 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) ∈ ℂ )
680 674 676 327 679 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( 𝐻 ‘ 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) )
681 680 660 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( 𝐻 ‘ 𝑤 ) / ( 𝐼 ‘ 𝑤 ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) )
682 640 673 681 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑤 = 𝑌 ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) )
683 638 682 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) )
684 683 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) )
685 579 684 eqtr2d ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) = 𝐿 )
686 352 48 82 constcncfg ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑁 + ( 1 / 2 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
687 cosf ⊢ cos : ℂ ⟶ ℂ
688 236 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ )
689 eqid ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) )
690 688 689 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
691 fcompt ⊢ ( ( cos : ℂ ⟶ ℂ ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) → ( cos ∘ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) )
692 687 690 691 sylancr ⊢ ( 𝜑 → ( cos ∘ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) )
693 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
694 319 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑦 = 𝑤 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
695 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑤 ∈ ( 𝐴 (,) 𝐵 ) )
696 693 694 695 332 fvmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) )
697 696 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) = ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) )
698 697 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) )
699 692 698 eqtr2d ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) = ( cos ∘ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
700 352 48 82 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑁 + ( 1 / 2 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
701 352 82 idcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑦 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
702 700 701 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
703 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
704 703 a1i ⊢ ( 𝜑 → cos ∈ ( ℂ –cn→ ℂ ) )
705 702 704 cncfco ⊢ ( 𝜑 → ( cos ∘ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
706 699 705 eqeltrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
707 686 706 mulcncf ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
708 eqid ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) )
709 352 160 82 constcncfg ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ π ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
710 2cnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
711 139 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
712 331 710 711 divrecd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑤 / 2 ) = ( 𝑤 · ( 1 / 2 ) ) )
713 712 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑤 / 2 ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑤 · ( 1 / 2 ) ) ) )
714 eqid ⊢ ( 𝑤 ∈ ℂ ↦ ( 𝑤 · ( 1 / 2 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( 𝑤 · ( 1 / 2 ) ) )
715 cncfmptid ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ ( ℂ –cn→ ℂ ) )
716 81 81 715 mp2an ⊢ ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ ( ℂ –cn→ ℂ )
717 716 a1i ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ ( ℂ –cn→ ℂ ) )
718 81 a1i ⊢ ( ( 1 / 2 ) ∈ ℂ → ℂ ⊆ ℂ )
719 id ⊢ ( ( 1 / 2 ) ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
720 718 719 718 constcncfg ⊢ ( ( 1 / 2 ) ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( 1 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
721 46 720 mp1i ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( 1 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
722 717 721 mulcncf ⊢ ( 𝜑 → ( 𝑤 ∈ ℂ ↦ ( 𝑤 · ( 1 / 2 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
723 712 465 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑤 · ( 1 / 2 ) ) ∈ ℂ )
724 714 722 352 82 723 cncfmptssg ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑤 · ( 1 / 2 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
725 713 724 eqeltrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑤 / 2 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
726 704 725 cncfmpt1f ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
727 709 726 mulcncf ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
728 ssid ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 )
729 728 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
730 difssd ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
731 658 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ ℂ )
732 124 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → π ∈ ℂ )
733 657 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑤 / 2 ) ) ∈ ℂ )
734 243 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → π ≠ 0 )
735 595 adantl ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑌 ) → ( cos ‘ ( 𝑤 / 2 ) ) = ( cos ‘ ( 𝑌 / 2 ) ) )
736 633 adantr ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑌 ) → ( cos ‘ ( 𝑌 / 2 ) ) ≠ 0 )
737 735 736 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑌 ) → ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 )
738 737 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑤 = 𝑌 ) → ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 )
739 738 668 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑤 / 2 ) ) ≠ 0 )
740 732 733 734 739 mulne0d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ≠ 0 )
741 740 neneqd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) = 0 )
742 elsng ⊢ ( ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ ℂ → ( ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ { 0 } ↔ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) = 0 ) )
743 731 742 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ { 0 } ↔ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) = 0 ) )
744 741 743 mtbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ { 0 } )
745 731 744 eldifd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
746 708 727 729 730 745 cncfmptssg ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ( ℂ ∖ { 0 } ) ) )
747 707 746 divcncf ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
748 747 490 eleqtrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
749 579 748 eqeltrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
750 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐿 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐿 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
751 358 356 750 sylancl ⊢ ( 𝜑 → ( 𝐿 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐿 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
752 749 751 mpbid ⊢ ( 𝜑 → ( 𝐿 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
753 752 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
754 363 eleq2d ⊢ ( 𝑦 = 𝑌 → ( 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
755 754 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ∧ 𝑌 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
756 753 9 755 syl2anc ⊢ ( 𝜑 → 𝐿 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
757 685 756 eqeltrd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
758 310 mpteq1d ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) )
759 757 758 503 3eltr4d ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
760 eqid ⊢ ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) )
761 5 fvmpt2 ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ∈ ℂ ) → ( 𝐻 ‘ 𝑦 ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
762 560 112 761 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐻 ‘ 𝑦 ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
763 762 562 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) / ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) )
764 112 206 565 divcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) / ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) ) ∈ ℂ )
765 763 764 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ∈ ℂ )
766 eqid ⊢ ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) )
767 765 766 fmptd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) : ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⟶ ℂ )
768 374 58 760 767 377 267 ellimc ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) limℂ 𝑌 ) ↔ ( 𝑤 ∈ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ↦ if ( 𝑤 = 𝑌 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) ‘ 𝑤 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
769 759 768 mpbird ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) limℂ 𝑌 ) )
770 109 eqcomd ⊢ ( 𝜑 → 𝐻 = ( ℝ D 𝐹 ) )
771 770 fveq1d ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
772 204 eqcomd ⊢ ( 𝜑 → 𝐼 = ( ℝ D 𝐺 ) )
773 772 fveq1d ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑦 ) = ( ( ℝ D 𝐺 ) ‘ 𝑦 ) )
774 771 773 oveq12d ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) )
775 774 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) )
776 775 oveq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐻 ‘ 𝑦 ) / ( 𝐼 ‘ 𝑦 ) ) ) limℂ 𝑌 ) = ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) limℂ 𝑌 ) )
777 769 776 eleqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) limℂ 𝑌 ) )
778 578 777 eqeltrd ⊢ ( 𝜑 → if ( ( 𝑌 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑌 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑌 / 2 ) ) ) ) ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) limℂ 𝑌 ) )
779 577 778 eqeltrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) limℂ 𝑌 ) )
780 15 24 32 34 9 35 116 210 434 509 559 575 779 lhop ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ) limℂ 𝑌 ) )
781 1 dirkerval ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
782 8 781 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
783 782 reseq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
784 15 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
785 260 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
786 23 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℂ )
787 2 fvmpt2 ⊢ ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∧ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℂ ) → ( 𝐹 ‘ 𝑦 ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
788 560 786 787 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐹 ‘ 𝑦 ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
789 560 506 528 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( 𝐺 ‘ 𝑦 ) = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
790 788 789 oveq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
791 785 790 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) )
792 791 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ) )
793 783 784 792 3eqtrrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) )
794 793 oveq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝐹 ‘ 𝑦 ) / ( 𝐺 ‘ 𝑦 ) ) ) limℂ 𝑌 ) = ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) limℂ 𝑌 ) )
795 780 794 eleqtrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) limℂ 𝑌 ) )