Metamath Proof Explorer

Theorem dirkercncflem4

Description: The Dirichlet Kernel is continuos at points that are not multiple of 2 π . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkercncflem4.d 
|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
dirkercncflem4.n 
|- ( ph -> N e. NN )
dirkercncflem4.y 
|- ( ph -> Y e. RR )
dirkercncflem4.ymod0 
|- ( ph -> ( Y mod ( 2 x. _pi ) ) =/= 0 )
dirkercncflem4.a 
|- A = ( |_ ` ( Y / ( 2 x. _pi ) ) )
dirkercncflem4.b 
|- B = ( A + 1 )
dirkercncflem4.c 
|- C = ( A x. ( 2 x. _pi ) )
dirkercncflem4.e 
|- E = ( B x. ( 2 x. _pi ) )
Assertion dirkercncflem4 
|- ( ph -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` Y ) )

Proof

Step Hyp Ref Expression
1 dirkercncflem4.d 
 |-  D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
2 dirkercncflem4.n 
 |-  ( ph -> N e. NN )
3 dirkercncflem4.y 
 |-  ( ph -> Y e. RR )
4 dirkercncflem4.ymod0 
 |-  ( ph -> ( Y mod ( 2 x. _pi ) ) =/= 0 )
5 dirkercncflem4.a 
 |-  A = ( |_ ` ( Y / ( 2 x. _pi ) ) )
6 dirkercncflem4.b 
 |-  B = ( A + 1 )
7 dirkercncflem4.c 
 |-  C = ( A x. ( 2 x. _pi ) )
8 dirkercncflem4.e 
 |-  E = ( B x. ( 2 x. _pi ) )
9 sincn 
 |-  sin e. ( CC -cn-> CC )
10 9 a1i 
 |-  ( ph -> sin e. ( CC -cn-> CC ) )
11 ioosscn 
 |-  ( C (,) E ) C_ CC
12 11 a1i 
 |-  ( ph -> ( C (,) E ) C_ CC )
13 2 nncnd 
 |-  ( ph -> N e. CC )
14 1cnd 
 |-  ( ph -> 1 e. CC )
15 14 halfcld 
 |-  ( ph -> ( 1 / 2 ) e. CC )
16 13 15 addcld 
 |-  ( ph -> ( N + ( 1 / 2 ) ) e. CC )
17 ssid 
 |-  CC C_ CC
18 17 a1i 
 |-  ( ph -> CC C_ CC )
19 12 16 18 constcncfg 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( N + ( 1 / 2 ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
20 12 18 idcncfg 
 |-  ( ph -> ( y e. ( C (,) E ) |-> y ) e. ( ( C (,) E ) -cn-> CC ) )
21 19 20 mulcncf 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) e. ( ( C (,) E ) -cn-> CC ) )
22 10 21 cncfmpt1f 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
23 2cnd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> 2 e. CC )
24 pirp 
 |-  _pi e. RR+
25 24 a1i 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> _pi e. RR+ )
26 25 rpcnd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> _pi e. CC )
27 23 26 mulcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( 2 x. _pi ) e. CC )
28 ioossre 
 |-  ( C (,) E ) C_ RR
29 28 a1i 
 |-  ( ph -> ( C (,) E ) C_ RR )
30 29 sselda 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> y e. RR )
31 30 recnd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> y e. CC )
32 31 halfcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y / 2 ) e. CC )
33 32 sincld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( sin ` ( y / 2 ) ) e. CC )
34 27 33 mulcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
35 2rp 
 |-  2 e. RR+
36 35 a1i 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> 2 e. RR+ )
37 36 rpne0d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> 2 =/= 0 )
38 25 rpne0d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> _pi =/= 0 )
39 23 26 37 38 mulne0d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( 2 x. _pi ) =/= 0 )
40 31 23 26 37 38 divdiv1d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( y / 2 ) / _pi ) = ( y / ( 2 x. _pi ) ) )
41 5 oveq1i 
 |-  ( A x. ( 2 x. _pi ) ) = ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) )
42 7 41 eqtri 
 |-  C = ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) )
43 42 oveq1i 
 |-  ( C / ( 2 x. _pi ) ) = ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) ) / ( 2 x. _pi ) )
44 2re 
 |-  2 e. RR
45 pire 
 |-  _pi e. RR
46 44 45 remulcli 
 |-  ( 2 x. _pi ) e. RR
47 46 a1i 
 |-  ( ph -> ( 2 x. _pi ) e. RR )
48 0re 
 |-  0 e. RR
49 2pos 
 |-  0 < 2
50 pipos 
 |-  0 < _pi
51 44 45 49 50 mulgt0ii 
 |-  0 < ( 2 x. _pi )
52 48 51 gtneii 
 |-  ( 2 x. _pi ) =/= 0
53 52 a1i 
 |-  ( ph -> ( 2 x. _pi ) =/= 0 )
54 3 47 53 redivcld 
 |-  ( ph -> ( Y / ( 2 x. _pi ) ) e. RR )
55 54 flcld 
 |-  ( ph -> ( |_ ` ( Y / ( 2 x. _pi ) ) ) e. ZZ )
56 55 zred 
 |-  ( ph -> ( |_ ` ( Y / ( 2 x. _pi ) ) ) e. RR )
57 56 recnd 
 |-  ( ph -> ( |_ ` ( Y / ( 2 x. _pi ) ) ) e. CC )
58 47 recnd 
 |-  ( ph -> ( 2 x. _pi ) e. CC )
59 57 58 53 divcan4d 
 |-  ( ph -> ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) = ( |_ ` ( Y / ( 2 x. _pi ) ) ) )
60 43 59 eqtrid 
 |-  ( ph -> ( C / ( 2 x. _pi ) ) = ( |_ ` ( Y / ( 2 x. _pi ) ) ) )
61 60 55 eqeltrd 
 |-  ( ph -> ( C / ( 2 x. _pi ) ) e. ZZ )
62 61 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( C / ( 2 x. _pi ) ) e. ZZ )
63 56 47 remulcld 
 |-  ( ph -> ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) ) e. RR )
64 42 63 eqeltrid 
 |-  ( ph -> C e. RR )
65 64 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> C e. RR )
66 36 25 rpmulcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( 2 x. _pi ) e. RR+ )
67 simpr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> y e. ( C (,) E ) )
68 64 rexrd 
 |-  ( ph -> C e. RR* )
69 68 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> C e. RR* )
70 5 eqcomi 
 |-  ( |_ ` ( Y / ( 2 x. _pi ) ) ) = A
71 70 oveq1i 
 |-  ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) = ( A + 1 )
72 71 6 eqtr4i 
 |-  ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) = B
73 72 oveq1i 
 |-  ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) ) = ( B x. ( 2 x. _pi ) )
74 73 8 eqtr4i 
 |-  ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) ) = E
75 74 a1i 
 |-  ( ph -> ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) ) = E )
76 1red 
 |-  ( ph -> 1 e. RR )
77 56 76 readdcld 
 |-  ( ph -> ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) e. RR )
78 77 47 remulcld 
 |-  ( ph -> ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) ) e. RR )
79 75 78 eqeltrrd 
 |-  ( ph -> E e. RR )
80 79 rexrd 
 |-  ( ph -> E e. RR* )
81 80 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> E e. RR* )
82 elioo2 
 |-  ( ( C e. RR* /\ E e. RR* ) -> ( y e. ( C (,) E ) <-> ( y e. RR /\ C < y /\ y < E ) ) )
83 69 81 82 syl2anc 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y e. ( C (,) E ) <-> ( y e. RR /\ C < y /\ y < E ) ) )
84 67 83 mpbid 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y e. RR /\ C < y /\ y < E ) )
85 84 simp2d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> C < y )
86 65 30 66 85 ltdiv1dd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( C / ( 2 x. _pi ) ) < ( y / ( 2 x. _pi ) ) )
87 79 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> E e. RR )
88 84 simp3d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> y < E )
89 30 87 66 88 ltdiv1dd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y / ( 2 x. _pi ) ) < ( E / ( 2 x. _pi ) ) )
90 7 a1i 
 |-  ( ph -> C = ( A x. ( 2 x. _pi ) ) )
91 90 oveq1d 
 |-  ( ph -> ( C / ( 2 x. _pi ) ) = ( ( A x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) )
92 91 oveq1d 
 |-  ( ph -> ( ( C / ( 2 x. _pi ) ) + 1 ) = ( ( ( A x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) + 1 ) )
93 5 57 eqeltrid 
 |-  ( ph -> A e. CC )
94 93 58 53 divcan4d 
 |-  ( ph -> ( ( A x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) = A )
95 94 oveq1d 
 |-  ( ph -> ( ( ( A x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) + 1 ) = ( A + 1 ) )
96 6 oveq1i 
 |-  ( B x. ( 2 x. _pi ) ) = ( ( A + 1 ) x. ( 2 x. _pi ) )
97 8 96 eqtri 
 |-  E = ( ( A + 1 ) x. ( 2 x. _pi ) )
98 97 a1i 
 |-  ( ph -> E = ( ( A + 1 ) x. ( 2 x. _pi ) ) )
99 98 oveq1d 
 |-  ( ph -> ( E / ( 2 x. _pi ) ) = ( ( ( A + 1 ) x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) )
100 93 14 addcld 
 |-  ( ph -> ( A + 1 ) e. CC )
101 100 58 53 divcan4d 
 |-  ( ph -> ( ( ( A + 1 ) x. ( 2 x. _pi ) ) / ( 2 x. _pi ) ) = ( A + 1 ) )
102 99 101 eqtr2d 
 |-  ( ph -> ( A + 1 ) = ( E / ( 2 x. _pi ) ) )
103 92 95 102 3eqtrrd 
 |-  ( ph -> ( E / ( 2 x. _pi ) ) = ( ( C / ( 2 x. _pi ) ) + 1 ) )
104 103 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( E / ( 2 x. _pi ) ) = ( ( C / ( 2 x. _pi ) ) + 1 ) )
105 89 104 breqtrd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y / ( 2 x. _pi ) ) < ( ( C / ( 2 x. _pi ) ) + 1 ) )
106 btwnnz 
 |-  ( ( ( C / ( 2 x. _pi ) ) e. ZZ /\ ( C / ( 2 x. _pi ) ) < ( y / ( 2 x. _pi ) ) /\ ( y / ( 2 x. _pi ) ) < ( ( C / ( 2 x. _pi ) ) + 1 ) ) -> -. ( y / ( 2 x. _pi ) ) e. ZZ )
107 62 86 105 106 syl3anc 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> -. ( y / ( 2 x. _pi ) ) e. ZZ )
108 40 107 eqneltrd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> -. ( ( y / 2 ) / _pi ) e. ZZ )
109 sineq0 
 |-  ( ( y / 2 ) e. CC -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / _pi ) e. ZZ ) )
110 32 109 syl 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / _pi ) e. ZZ ) )
111 108 110 mtbird 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> -. ( sin ` ( y / 2 ) ) = 0 )
112 111 neqned 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( sin ` ( y / 2 ) ) =/= 0 )
113 27 33 39 112 mulne0d 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) =/= 0 )
114 113 neneqd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> -. ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = 0 )
115 44 a1i 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> 2 e. RR )
116 45 a1i 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> _pi e. RR )
117 115 116 remulcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( 2 x. _pi ) e. RR )
118 30 rehalfcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y / 2 ) e. RR )
119 118 resincld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( sin ` ( y / 2 ) ) e. RR )
120 117 119 remulcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. RR )
121 elsng 
 |-  ( ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. RR -> ( ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. { 0 } <-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = 0 ) )
122 120 121 syl 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. { 0 } <-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = 0 ) )
123 114 122 mtbird 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> -. ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. { 0 } )
124 34 123 eldifd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. ( CC \ { 0 } ) )
125 eqidd 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
126 eqidd 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) = ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) )
127 oveq2 
 |-  ( x = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) -> ( 1 / x ) = ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
128 124 125 126 127 fmptco 
 |-  ( ph -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) o. ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( y e. ( C (,) E ) |-> ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
129 eqid 
 |-  ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
130 2cnd 
 |-  ( ph -> 2 e. CC )
131 12 130 18 constcncfg 
 |-  ( ph -> ( y e. ( C (,) E ) |-> 2 ) e. ( ( C (,) E ) -cn-> CC ) )
132 24 a1i 
 |-  ( ph -> _pi e. RR+ )
133 132 rpcnd 
 |-  ( ph -> _pi e. CC )
134 12 133 18 constcncfg 
 |-  ( ph -> ( y e. ( C (,) E ) |-> _pi ) e. ( ( C (,) E ) -cn-> CC ) )
135 131 134 mulcncf 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( 2 x. _pi ) ) e. ( ( C (,) E ) -cn-> CC ) )
136 31 23 37 divrecd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( y / 2 ) = ( y x. ( 1 / 2 ) ) )
137 136 mpteq2dva 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( y / 2 ) ) = ( y e. ( C (,) E ) |-> ( y x. ( 1 / 2 ) ) ) )
138 12 15 18 constcncfg 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( 1 / 2 ) ) e. ( ( C (,) E ) -cn-> CC ) )
139 20 138 mulcncf 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( y x. ( 1 / 2 ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
140 137 139 eqeltrd 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( y / 2 ) ) e. ( ( C (,) E ) -cn-> CC ) )
141 10 140 cncfmpt1f 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( sin ` ( y / 2 ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
142 135 141 mulcncf 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
143 ssid 
 |-  ( C (,) E ) C_ ( C (,) E )
144 143 a1i 
 |-  ( ph -> ( C (,) E ) C_ ( C (,) E ) )
145 difssd 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
146 129 142 144 145 124 cncfmptssg 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) e. ( ( C (,) E ) -cn-> ( CC \ { 0 } ) ) )
147 ax-1cn 
 |-  1 e. CC
148 eqid 
 |-  ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) = ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) )
149 148 cdivcncf 
 |-  ( 1 e. CC -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
150 147 149 mp1i 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
151 146 150 cncfco 
 |-  ( ph -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) o. ( y e. ( C (,) E ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
152 128 151 eqeltrrd 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
153 22 152 mulcncf 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) x. ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) e. ( ( C (,) E ) -cn-> CC ) )
154 1 dirkerval 
 |-  ( N e. NN -> ( D ` N ) = ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
155 2 154 syl 
 |-  ( ph -> ( D ` N ) = ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
156 155 reseq1d 
 |-  ( ph -> ( ( D ` N ) |` ( C (,) E ) ) = ( ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) |` ( C (,) E ) ) )
157 29 resmptd 
 |-  ( ph -> ( ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) |` ( C (,) E ) ) = ( y e. ( C (,) E ) |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
158 35 a1i 
 |-  ( ph -> 2 e. RR+ )
159 158 132 rpmulcld 
 |-  ( ph -> ( 2 x. _pi ) e. RR+ )
160 159 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( 2 x. _pi ) e. RR+ )
161 mod0 
 |-  ( ( y e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( y / ( 2 x. _pi ) ) e. ZZ ) )
162 30 160 161 syl2anc 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( y / ( 2 x. _pi ) ) e. ZZ ) )
163 107 162 mtbird 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> -. ( y mod ( 2 x. _pi ) ) = 0 )
164 163 iffalsed 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
165 13 adantr 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> N e. CC )
166 1cnd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> 1 e. CC )
167 166 halfcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( 1 / 2 ) e. CC )
168 165 167 addcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( N + ( 1 / 2 ) ) e. CC )
169 168 31 mulcld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
170 169 sincld 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
171 170 34 113 divrecd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) x. ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
172 164 171 eqtrd 
 |-  ( ( ph /\ y e. ( C (,) E ) ) -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) x. ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
173 172 mpteq2dva 
 |-  ( ph -> ( y e. ( C (,) E ) |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( y e. ( C (,) E ) |-> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) x. ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
174 156 157 173 3eqtrrd 
 |-  ( ph -> ( y e. ( C (,) E ) |-> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) x. ( 1 / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( ( D ` N ) |` ( C (,) E ) ) )
175 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
176 175 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
177 176 oveq1i 
 |-  ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( C (,) E ) )
178 175 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
179 reex 
 |-  RR e. _V
180 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( C (,) E ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( C (,) E ) ) = ( ( TopOpen ` CCfld ) |`t ( C (,) E ) ) )
181 178 28 179 180 mp3an 
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( C (,) E ) ) = ( ( TopOpen ` CCfld ) |`t ( C (,) E ) )
182 177 181 eqtri 
 |-  ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) = ( ( TopOpen ` CCfld ) |`t ( C (,) E ) )
183 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
184 183 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
185 178 184 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
186 185 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
187 175 182 186 cncfcn 
 |-  ( ( ( C (,) E ) C_ CC /\ CC C_ CC ) -> ( ( C (,) E ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) Cn ( TopOpen ` CCfld ) ) )
188 12 18 187 syl2anc 
 |-  ( ph -> ( ( C (,) E ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) Cn ( TopOpen ` CCfld ) ) )
189 153 174 188 3eltr3d 
 |-  ( ph -> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) Cn ( TopOpen ` CCfld ) ) )
190 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
191 190 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
192 resttopon 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( C (,) E ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) e. ( TopOn ` ( C (,) E ) ) )
193 191 29 192 syl2anc 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) e. ( TopOn ` ( C (,) E ) ) )
194 175 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
195 194 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
196 cncnp 
 |-  ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) e. ( TopOn ` ( C (,) E ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( ( D ` N ) |` ( C (,) E ) ) : ( C (,) E ) --> CC /\ A. y e. ( C (,) E ) ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
197 193 195 196 syl2anc 
 |-  ( ph -> ( ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( ( D ` N ) |` ( C (,) E ) ) : ( C (,) E ) --> CC /\ A. y e. ( C (,) E ) ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
198 189 197 mpbid 
 |-  ( ph -> ( ( ( D ` N ) |` ( C (,) E ) ) : ( C (,) E ) --> CC /\ A. y e. ( C (,) E ) ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
199 198 simprd 
 |-  ( ph -> A. y e. ( C (,) E ) ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
200 4 neneqd 
 |-  ( ph -> -. ( Y mod ( 2 x. _pi ) ) = 0 )
201 mod0 
 |-  ( ( Y e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( Y mod ( 2 x. _pi ) ) = 0 <-> ( Y / ( 2 x. _pi ) ) e. ZZ ) )
202 3 159 201 syl2anc 
 |-  ( ph -> ( ( Y mod ( 2 x. _pi ) ) = 0 <-> ( Y / ( 2 x. _pi ) ) e. ZZ ) )
203 200 202 mtbid 
 |-  ( ph -> -. ( Y / ( 2 x. _pi ) ) e. ZZ )
204 flltnz 
 |-  ( ( ( Y / ( 2 x. _pi ) ) e. RR /\ -. ( Y / ( 2 x. _pi ) ) e. ZZ ) -> ( |_ ` ( Y / ( 2 x. _pi ) ) ) < ( Y / ( 2 x. _pi ) ) )
205 54 203 204 syl2anc 
 |-  ( ph -> ( |_ ` ( Y / ( 2 x. _pi ) ) ) < ( Y / ( 2 x. _pi ) ) )
206 56 54 159 205 ltmul1dd 
 |-  ( ph -> ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) ) < ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) )
207 3 recnd 
 |-  ( ph -> Y e. CC )
208 207 58 53 divcan1d 
 |-  ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = Y )
209 206 208 breqtrd 
 |-  ( ph -> ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) ) < Y )
210 42 209 eqbrtrid 
 |-  ( ph -> C < Y )
211 fllelt 
 |-  ( ( Y / ( 2 x. _pi ) ) e. RR -> ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) <_ ( Y / ( 2 x. _pi ) ) /\ ( Y / ( 2 x. _pi ) ) < ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) ) )
212 54 211 syl 
 |-  ( ph -> ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) <_ ( Y / ( 2 x. _pi ) ) /\ ( Y / ( 2 x. _pi ) ) < ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) ) )
213 212 simprd 
 |-  ( ph -> ( Y / ( 2 x. _pi ) ) < ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) )
214 54 77 159 213 ltmul1dd 
 |-  ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) < ( ( ( |_ ` ( Y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) ) )
215 214 208 75 3brtr3d 
 |-  ( ph -> Y < E )
216 68 80 3 210 215 eliood 
 |-  ( ph -> Y e. ( C (,) E ) )
217 fveq2 
 |-  ( y = Y -> ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
218 217 eleq2d 
 |-  ( y = Y -> ( ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
219 218 rspccva 
 |-  ( ( A. y e. ( C (,) E ) ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` y ) /\ Y e. ( C (,) E ) ) -> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
220 199 216 219 syl2anc 
 |-  ( ph -> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
221 178 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
222 1 dirkerf 
 |-  ( N e. NN -> ( D ` N ) : RR --> RR )
223 2 222 syl 
 |-  ( ph -> ( D ` N ) : RR --> RR )
224 223 29 fssresd 
 |-  ( ph -> ( ( D ` N ) |` ( C (,) E ) ) : ( C (,) E ) --> RR )
225 ax-resscn 
 |-  RR C_ CC
226 225 a1i 
 |-  ( ph -> RR C_ CC )
227 retop 
 |-  ( topGen ` ran (,) ) e. Top
228 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
229 228 restuni 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( C (,) E ) C_ RR ) -> ( C (,) E ) = U. ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) )
230 227 28 229 mp2an 
 |-  ( C (,) E ) = U. ( ( topGen ` ran (,) ) |`t ( C (,) E ) )
231 230 183 cnprest2 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( D ` N ) |` ( C (,) E ) ) : ( C (,) E ) --> RR /\ RR C_ CC ) -> ( ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) <-> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` Y ) ) )
232 221 224 226 231 syl3anc 
 |-  ( ph -> ( ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) <-> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` Y ) ) )
233 220 232 mpbid 
 |-  ( ph -> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` Y ) )
234 176 eqcomi 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) )
235 234 a1i 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) ) )
236 235 oveq2d 
 |-  ( ph -> ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) = ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( topGen ` ran (,) ) ) )
237 236 fveq1d 
 |-  ( ph -> ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` Y ) = ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( topGen ` ran (,) ) ) ` Y ) )
238 233 237 eleqtrd 
 |-  ( ph -> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( topGen ` ran (,) ) ) ` Y ) )
239 227 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
240 iooretop 
 |-  ( C (,) E ) e. ( topGen ` ran (,) )
241 228 isopn3 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( C (,) E ) C_ RR ) -> ( ( C (,) E ) e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` ( C (,) E ) ) = ( C (,) E ) ) )
242 240 241 mpbii 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( C (,) E ) C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( C (,) E ) ) = ( C (,) E ) )
243 239 29 242 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( C (,) E ) ) = ( C (,) E ) )
244 243 eqcomd 
 |-  ( ph -> ( C (,) E ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( C (,) E ) ) )
245 216 244 eleqtrd 
 |-  ( ph -> Y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( C (,) E ) ) )
246 228 228 cnprest 
 |-  ( ( ( ( topGen ` ran (,) ) e. Top /\ ( C (,) E ) C_ RR ) /\ ( Y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( C (,) E ) ) /\ ( D ` N ) : RR --> RR ) ) -> ( ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` Y ) <-> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( topGen ` ran (,) ) ) ` Y ) ) )
247 239 29 245 223 246 syl22anc 
 |-  ( ph -> ( ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` Y ) <-> ( ( D ` N ) |` ( C (,) E ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( C (,) E ) ) CnP ( topGen ` ran (,) ) ) ` Y ) ) )
248 238 247 mpbird 
 |-  ( ph -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` Y ) )