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		tgioo4	\|- ( 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 ) )

Metamath Proof Explorer

Theorem dirkercncflem4

Proof