Theorem fouriersw

Description: Fourier series convergence, for the square wave function. Where F is discontinuous, the series converges to 0 , the average value of the left and the right limits. Notice that F is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fouriersw.t	|- T = ( 2 x. _pi )
	fouriersw.f	|- F = ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
	fouriersw.x	|- X e. RR
	fouriersw.z	|- S = ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) )
	fouriersw.y	|- Y = if ( ( X mod _pi ) = 0 , 0 , ( F ` X ) )
Assertion	fouriersw	|- ( ( ( 4 / _pi ) x. sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = Y /\ seq 1 ( + , S ) ~~> ( ( _pi / 4 ) x. Y ) )

Proof

Step	Hyp	Ref	Expression
1		fouriersw.t	|- T = ( 2 x. _pi )
2		fouriersw.f	|- F = ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
3		fouriersw.x	|- X e. RR
4		fouriersw.z	|- S = ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) )
5		fouriersw.y	|- Y = if ( ( X mod _pi ) = 0 , 0 , ( F ` X ) )
6		nnuz	|- NN = ( ZZ>= ` 1 )
7		1zzd	|- ( T. -> 1 e. ZZ )
8		eqidd	|- ( k e. NN -> ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) = ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) )
9		oveq2	|- ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
10	9	oveq1d	|- ( n = k -> ( ( 2 x. n ) - 1 ) = ( ( 2 x. k ) - 1 ) )
11	10	oveq1d	|- ( n = k -> ( ( ( 2 x. n ) - 1 ) x. X ) = ( ( ( 2 x. k ) - 1 ) x. X ) )
12	11	fveq2d	|- ( n = k -> ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) = ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) )
13	12 10	oveq12d	|- ( n = k -> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) = ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
14	13	adantl	|- ( ( k e. NN /\ n = k ) -> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) = ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
15		id	|- ( k e. NN -> k e. NN )
16		ovex	|- ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) e. _V
17	16	a1i	|- ( k e. NN -> ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) e. _V )
18	8 14 15 17	fvmptd	|- ( k e. NN -> ( ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ` k ) = ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
19	18	adantl	|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ` k ) = ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
20		2z	|- 2 e. ZZ
21	20	a1i	|- ( k e. NN -> 2 e. ZZ )
22		nnz	|- ( k e. NN -> k e. ZZ )
23	21 22	zmulcld	|- ( k e. NN -> ( 2 x. k ) e. ZZ )
24		1zzd	|- ( k e. NN -> 1 e. ZZ )
25	23 24	zsubcld	|- ( k e. NN -> ( ( 2 x. k ) - 1 ) e. ZZ )
26	25	zcnd	|- ( k e. NN -> ( ( 2 x. k ) - 1 ) e. CC )
27	3	recni	|- X e. CC
28	27	a1i	|- ( k e. NN -> X e. CC )
29	26 28	mulcld	|- ( k e. NN -> ( ( ( 2 x. k ) - 1 ) x. X ) e. CC )
30	29	sincld	|- ( k e. NN -> ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) e. CC )
31		0red	|- ( k e. NN -> 0 e. RR )
32		2re	|- 2 e. RR
33	32	a1i	|- ( k e. NN -> 2 e. RR )
34		1red	|- ( k e. NN -> 1 e. RR )
35	33 34	remulcld	|- ( k e. NN -> ( 2 x. 1 ) e. RR )
36	35 34	resubcld	|- ( k e. NN -> ( ( 2 x. 1 ) - 1 ) e. RR )
37	25	zred	|- ( k e. NN -> ( ( 2 x. k ) - 1 ) e. RR )
38		0lt1	|- 0 < 1
39		2t1e2	|- ( 2 x. 1 ) = 2
40	39	oveq1i	|- ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 )
41		2m1e1	|- ( 2 - 1 ) = 1
42	40 41	eqtr2i	|- 1 = ( ( 2 x. 1 ) - 1 )
43	38 42	breqtri	|- 0 < ( ( 2 x. 1 ) - 1 )
44	43	a1i	|- ( k e. NN -> 0 < ( ( 2 x. 1 ) - 1 ) )
45	23	zred	|- ( k e. NN -> ( 2 x. k ) e. RR )
46		nnre	|- ( k e. NN -> k e. RR )
47		0le2	|- 0 <_ 2
48	47	a1i	|- ( k e. NN -> 0 <_ 2 )
49		nnge1	|- ( k e. NN -> 1 <_ k )
50	34 46 33 48 49	lemul2ad	|- ( k e. NN -> ( 2 x. 1 ) <_ ( 2 x. k ) )
51	35 45 34 50	lesub1dd	|- ( k e. NN -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. k ) - 1 ) )
52	31 36 37 44 51	ltletrd	|- ( k e. NN -> 0 < ( ( 2 x. k ) - 1 ) )
53	31 52	gtned	|- ( k e. NN -> ( ( 2 x. k ) - 1 ) =/= 0 )
54	30 26 53	divcld	|- ( k e. NN -> ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) e. CC )
55	54	adantl	|- ( ( T. /\ k e. NN ) -> ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) e. CC )
56		picn	|- _pi e. CC
57	56	a1i	|- ( T. -> _pi e. CC )
58		4cn	|- 4 e. CC
59	58	a1i	|- ( T. -> 4 e. CC )
60		4ne0	|- 4 =/= 0
61	60	a1i	|- ( T. -> 4 =/= 0 )
62	57 59 61	divcld	|- ( T. -> ( _pi / 4 ) e. CC )
63		eqid	|- ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) = ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
64		0cnd	|- ( n e. NN -> 0 e. CC )
65	58	a1i	|- ( n e. NN -> 4 e. CC )
66		nncn	|- ( n e. NN -> n e. CC )
67		mulcl	|- ( ( n e. CC /\ _pi e. CC ) -> ( n x. _pi ) e. CC )
68	66 56 67	sylancl	|- ( n e. NN -> ( n x. _pi ) e. CC )
69	56	a1i	|- ( n e. NN -> _pi e. CC )
70		nnne0	|- ( n e. NN -> n =/= 0 )
71		0re	|- 0 e. RR
72		pipos	|- 0 < _pi
73	71 72	gtneii	|- _pi =/= 0
74	73	a1i	|- ( n e. NN -> _pi =/= 0 )
75	66 69 70 74	mulne0d	|- ( n e. NN -> ( n x. _pi ) =/= 0 )
76	65 68 75	divcld	|- ( n e. NN -> ( 4 / ( n x. _pi ) ) e. CC )
77	27	a1i	|- ( n e. NN -> X e. CC )
78	66 77	mulcld	|- ( n e. NN -> ( n x. X ) e. CC )
79	78	sincld	|- ( n e. NN -> ( sin ` ( n x. X ) ) e. CC )
80	76 79	mulcld	|- ( n e. NN -> ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) e. CC )
81	64 80	ifcld	|- ( n e. NN -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) e. CC )
82	63 81	fmpti	|- ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) : NN --> CC
83	82	a1i	|- ( T. -> ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) : NN --> CC )
84		eqidd	|- ( k e. NN -> ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) = ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) )
85		breq2	|- ( n = k -> ( 2 || n <-> 2 || k ) )
86		oveq1	|- ( n = k -> ( n x. _pi ) = ( k x. _pi ) )
87	86	oveq2d	|- ( n = k -> ( 4 / ( n x. _pi ) ) = ( 4 / ( k x. _pi ) ) )
88		oveq1	|- ( n = k -> ( n x. X ) = ( k x. X ) )
89	88	fveq2d	|- ( n = k -> ( sin ` ( n x. X ) ) = ( sin ` ( k x. X ) ) )
90	87 89	oveq12d	|- ( n = k -> ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) = ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) )
91	85 90	ifbieq2d	|- ( n = k -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) )
92	91	adantl	|- ( ( k e. NN /\ n = k ) -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) )
93		c0ex	|- 0 e. _V
94		ovex	|- ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) e. _V
95	93 94	ifex	|- if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) e. _V
96	95	a1i	|- ( k e. NN -> if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) e. _V )
97	84 92 15 96	fvmptd	|- ( k e. NN -> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` k ) = if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) )
98	97	adantr	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` k ) = if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) )
99		simpr	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> ( k / 2 ) e. NN )
100		simpl	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> k e. NN )
101		2nn	|- 2 e. NN
102		nndivdvds	|- ( ( k e. NN /\ 2 e. NN ) -> ( 2 || k <-> ( k / 2 ) e. NN ) )
103	100 101 102	sylancl	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> ( 2 || k <-> ( k / 2 ) e. NN ) )
104	99 103	mpbird	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> 2 || k )
105	104	iftrued	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> if ( 2 || k , 0 , ( ( 4 / ( k x. _pi ) ) x. ( sin ` ( k x. X ) ) ) ) = 0 )
106	98 105	eqtrd	|- ( ( k e. NN /\ ( k / 2 ) e. NN ) -> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` k ) = 0 )
107	106	3adant1	|- ( ( T. /\ k e. NN /\ ( k / 2 ) e. NN ) -> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` k ) = 0 )
108		1re	|- 1 e. RR
109	108	renegcli	|- -u 1 e. RR
110	108 109	ifcli	|- if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR
111	110	a1i	|- ( x e. RR -> if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR )
112	2 111	fmpti	|- F : RR --> RR
113		oveq1	|- ( x = y -> ( x mod T ) = ( y mod T ) )
114	113	breq1d	|- ( x = y -> ( ( x mod T ) < _pi <-> ( y mod T ) < _pi ) )
115	114	ifbid	|- ( x = y -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = if ( ( y mod T ) < _pi , 1 , -u 1 ) )
116	115	cbvmptv	|- ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) = ( y e. RR |-> if ( ( y mod T ) < _pi , 1 , -u 1 ) )
117	2 116	eqtri	|- F = ( y e. RR |-> if ( ( y mod T ) < _pi , 1 , -u 1 ) )
118	117	a1i	|- ( x e. RR -> F = ( y e. RR |-> if ( ( y mod T ) < _pi , 1 , -u 1 ) ) )
119		oveq1	|- ( y = ( x + T ) -> ( y mod T ) = ( ( x + T ) mod T ) )
120		pire	|- _pi e. RR
121	32 120	remulcli	|- ( 2 x. _pi ) e. RR
122	1 121	eqeltri	|- T e. RR
123	122	recni	|- T e. CC
124	123	mulid2i	|- ( 1 x. T ) = T
125	124	eqcomi	|- T = ( 1 x. T )
126	125	oveq2i	|- ( x + T ) = ( x + ( 1 x. T ) )
127	126	oveq1i	|- ( ( x + T ) mod T ) = ( ( x + ( 1 x. T ) ) mod T )
128	119 127	eqtrdi	|- ( y = ( x + T ) -> ( y mod T ) = ( ( x + ( 1 x. T ) ) mod T ) )
129	128	adantl	|- ( ( x e. RR /\ y = ( x + T ) ) -> ( y mod T ) = ( ( x + ( 1 x. T ) ) mod T ) )
130		simpl	|- ( ( x e. RR /\ y = ( x + T ) ) -> x e. RR )
131		2pos	|- 0 < 2
132	32 120 131 72	mulgt0ii	|- 0 < ( 2 x. _pi )
133	1	eqcomi	|- ( 2 x. _pi ) = T
134	132 133	breqtri	|- 0 < T
135	122 134	elrpii	|- T e. RR+
136	135	a1i	|- ( ( x e. RR /\ y = ( x + T ) ) -> T e. RR+ )
137		1zzd	|- ( ( x e. RR /\ y = ( x + T ) ) -> 1 e. ZZ )
138		modcyc	|- ( ( x e. RR /\ T e. RR+ /\ 1 e. ZZ ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
139	130 136 137 138	syl3anc	|- ( ( x e. RR /\ y = ( x + T ) ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
140	129 139	eqtrd	|- ( ( x e. RR /\ y = ( x + T ) ) -> ( y mod T ) = ( x mod T ) )
141	140	breq1d	|- ( ( x e. RR /\ y = ( x + T ) ) -> ( ( y mod T ) < _pi <-> ( x mod T ) < _pi ) )
142	141	ifbid	|- ( ( x e. RR /\ y = ( x + T ) ) -> if ( ( y mod T ) < _pi , 1 , -u 1 ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
143		id	|- ( x e. RR -> x e. RR )
144	122	a1i	|- ( x e. RR -> T e. RR )
145	143 144	readdcld	|- ( x e. RR -> ( x + T ) e. RR )
146	118 142 145 111	fvmptd	|- ( x e. RR -> ( F ` ( x + T ) ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
147	2	fvmpt2	|- ( ( x e. RR /\ if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
148	110 147	mpan2	|- ( x e. RR -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
149	146 148	eqtr4d	|- ( x e. RR -> ( F ` ( x + T ) ) = ( F ` x ) )
150		eqid	|- ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
151		snfi	|- { 0 } e. Fin
152		eldifi	|- ( x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x e. ( -u _pi (,) _pi ) )
153		0xr	|- 0 e. RR*
154	153	a1i	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> 0 e. RR* )
155	120	rexri	|- _pi e. RR*
156	155	a1i	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> _pi e. RR* )
157		elioore	|- ( x e. ( -u _pi (,) _pi ) -> x e. RR )
158	157	adantr	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> x e. RR )
159		simpr	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> 0 < x )
160	120	renegcli	|- -u _pi e. RR
161	160	rexri	|- -u _pi e. RR*
162		iooltub	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ x e. ( -u _pi (,) _pi ) ) -> x < _pi )
163	161 155 162	mp3an12	|- ( x e. ( -u _pi (,) _pi ) -> x < _pi )
164	163	adantr	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> x < _pi )
165	154 156 158 159 164	eliood	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> x e. ( 0 (,) _pi ) )
166		negpilt0	|- -u _pi < 0
167	160 71 166	ltleii	|- -u _pi <_ 0
168		iooss1	|- ( ( -u _pi e. RR* /\ -u _pi <_ 0 ) -> ( 0 (,) _pi ) C_ ( -u _pi (,) _pi ) )
169	161 167 168	mp2an	|- ( 0 (,) _pi ) C_ ( -u _pi (,) _pi )
170	169	sseli	|- ( x e. ( 0 (,) _pi ) -> x e. ( -u _pi (,) _pi ) )
171	2	reseq1i	|- ( F |` ( 0 (,) _pi ) ) = ( ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) |` ( 0 (,) _pi ) )
172		ioossre	|- ( 0 (,) _pi ) C_ RR
173		resmpt	|- ( ( 0 (,) _pi ) C_ RR -> ( ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) |` ( 0 (,) _pi ) ) = ( x e. ( 0 (,) _pi ) |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) )
174	172 173	ax-mp	|- ( ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) |` ( 0 (,) _pi ) ) = ( x e. ( 0 (,) _pi ) |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
175		elioore	|- ( x e. ( 0 (,) _pi ) -> x e. RR )
176	135	a1i	|- ( x e. ( 0 (,) _pi ) -> T e. RR+ )
177		0red	|- ( x e. ( 0 (,) _pi ) -> 0 e. RR )
178		ioogtlb	|- ( ( 0 e. RR* /\ _pi e. RR* /\ x e. ( 0 (,) _pi ) ) -> 0 < x )
179	153 155 178	mp3an12	|- ( x e. ( 0 (,) _pi ) -> 0 < x )
180	177 175 179	ltled	|- ( x e. ( 0 (,) _pi ) -> 0 <_ x )
181	120	a1i	|- ( x e. ( 0 (,) _pi ) -> _pi e. RR )
182	122	a1i	|- ( x e. ( 0 (,) _pi ) -> T e. RR )
183	170 163	syl	|- ( x e. ( 0 (,) _pi ) -> x < _pi )
184		pirp	|- _pi e. RR+
185		2timesgt	|- ( _pi e. RR+ -> _pi < ( 2 x. _pi ) )
186	184 185	ax-mp	|- _pi < ( 2 x. _pi )
187	186 133	breqtri	|- _pi < T
188	187	a1i	|- ( x e. ( 0 (,) _pi ) -> _pi < T )
189	175 181 182 183 188	lttrd	|- ( x e. ( 0 (,) _pi ) -> x < T )
190		modid	|- ( ( ( x e. RR /\ T e. RR+ ) /\ ( 0 <_ x /\ x < T ) ) -> ( x mod T ) = x )
191	175 176 180 189 190	syl22anc	|- ( x e. ( 0 (,) _pi ) -> ( x mod T ) = x )
192	191 183	eqbrtrd	|- ( x e. ( 0 (,) _pi ) -> ( x mod T ) < _pi )
193	192	iftrued	|- ( x e. ( 0 (,) _pi ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
194	193	mpteq2ia	|- ( x e. ( 0 (,) _pi ) |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) = ( x e. ( 0 (,) _pi ) |-> 1 )
195	171 174 194	3eqtrri	|- ( x e. ( 0 (,) _pi ) |-> 1 ) = ( F |` ( 0 (,) _pi ) )
196	195	oveq2i	|- ( RR _D ( x e. ( 0 (,) _pi ) |-> 1 ) ) = ( RR _D ( F |` ( 0 (,) _pi ) ) )
197		reelprrecn	|- RR e. { RR , CC }
198	197	a1i	|- ( T. -> RR e. { RR , CC } )
199		iooretop	|- ( 0 (,) _pi ) e. ( topGen ` ran (,) )
200		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
201	200	tgioo2	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
202	199 201	eleqtri	|- ( 0 (,) _pi ) e. ( ( TopOpen ` CCfld ) |`t RR )
203	202	a1i	|- ( T. -> ( 0 (,) _pi ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
204		1cnd	|- ( T. -> 1 e. CC )
205	198 203 204	dvmptconst	|- ( T. -> ( RR _D ( x e. ( 0 (,) _pi ) |-> 1 ) ) = ( x e. ( 0 (,) _pi ) |-> 0 ) )
206	205	mptru	|- ( RR _D ( x e. ( 0 (,) _pi ) |-> 1 ) ) = ( x e. ( 0 (,) _pi ) |-> 0 )
207		ssid	|- RR C_ RR
208		ax-resscn	|- RR C_ CC
209		fss	|- ( ( F : RR --> RR /\ RR C_ CC ) -> F : RR --> CC )
210	112 208 209	mp2an	|- F : RR --> CC
211		dvresioo	|- ( ( RR C_ RR /\ F : RR --> CC ) -> ( RR _D ( F |` ( 0 (,) _pi ) ) ) = ( ( RR _D F ) |` ( 0 (,) _pi ) ) )
212	207 210 211	mp2an	|- ( RR _D ( F |` ( 0 (,) _pi ) ) ) = ( ( RR _D F ) |` ( 0 (,) _pi ) )
213	196 206 212	3eqtr3i	|- ( x e. ( 0 (,) _pi ) |-> 0 ) = ( ( RR _D F ) |` ( 0 (,) _pi ) )
214	213	dmeqi	|- dom ( x e. ( 0 (,) _pi ) |-> 0 ) = dom ( ( RR _D F ) |` ( 0 (,) _pi ) )
215		eqid	|- ( x e. ( 0 (,) _pi ) |-> 0 ) = ( x e. ( 0 (,) _pi ) |-> 0 )
216	93 215	dmmpti	|- dom ( x e. ( 0 (,) _pi ) |-> 0 ) = ( 0 (,) _pi )
217	214 216	eqtr3i	|- dom ( ( RR _D F ) |` ( 0 (,) _pi ) ) = ( 0 (,) _pi )
218		ssdmres	|- ( ( 0 (,) _pi ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( 0 (,) _pi ) ) = ( 0 (,) _pi ) )
219	217 218	mpbir	|- ( 0 (,) _pi ) C_ dom ( RR _D F )
220	219	sseli	|- ( x e. ( 0 (,) _pi ) -> x e. dom ( RR _D F ) )
221	170 220	elind	|- ( x e. ( 0 (,) _pi ) -> x e. ( ( -u _pi (,) _pi ) i^i dom ( RR _D F ) ) )
222		dmres	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) = ( ( -u _pi (,) _pi ) i^i dom ( RR _D F ) )
223	221 222	eleqtrrdi	|- ( x e. ( 0 (,) _pi ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
224	165 223	syl	|- ( ( x e. ( -u _pi (,) _pi ) /\ 0 < x ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
225	224	adantlr	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ 0 < x ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
226	161	a1i	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> -u _pi e. RR* )
227	153	a1i	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> 0 e. RR* )
228	157	ad2antrr	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> x e. RR )
229		ioogtlb	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ x e. ( -u _pi (,) _pi ) ) -> -u _pi < x )
230	161 155 229	mp3an12	|- ( x e. ( -u _pi (,) _pi ) -> -u _pi < x )
231	230	ad2antrr	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> -u _pi < x )
232		0red	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> 0 e. RR )
233		neqne	|- ( -. x = 0 -> x =/= 0 )
234	233	ad2antlr	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> x =/= 0 )
235		simpr	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> -. 0 < x )
236	228 232 234 235	lttri5d	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> x < 0 )
237	226 227 228 231 236	eliood	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> x e. ( -u _pi (,) 0 ) )
238	71 120 72	ltleii	|- 0 <_ _pi
239		iooss2	|- ( ( _pi e. RR* /\ 0 <_ _pi ) -> ( -u _pi (,) 0 ) C_ ( -u _pi (,) _pi ) )
240	155 238 239	mp2an	|- ( -u _pi (,) 0 ) C_ ( -u _pi (,) _pi )
241	240	sseli	|- ( x e. ( -u _pi (,) 0 ) -> x e. ( -u _pi (,) _pi ) )
242	2	reseq1i	|- ( F |` ( -u _pi (,) 0 ) ) = ( ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) |` ( -u _pi (,) 0 ) )
243		ioossre	|- ( -u _pi (,) 0 ) C_ RR
244		resmpt	|- ( ( -u _pi (,) 0 ) C_ RR -> ( ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) |` ( -u _pi (,) 0 ) ) = ( x e. ( -u _pi (,) 0 ) |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) )
245	243 244	ax-mp	|- ( ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) |` ( -u _pi (,) 0 ) ) = ( x e. ( -u _pi (,) 0 ) |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
246	120	a1i	|- ( x e. ( -u _pi (,) 0 ) -> _pi e. RR )
247		elioore	|- ( x e. ( -u _pi (,) 0 ) -> x e. RR )
248	135	a1i	|- ( x e. ( -u _pi (,) 0 ) -> T e. RR+ )
249	247 248	modcld	|- ( x e. ( -u _pi (,) 0 ) -> ( x mod T ) e. RR )
250	247 145	syl	|- ( x e. ( -u _pi (,) 0 ) -> ( x + T ) e. RR )
251	56	2timesi	|- ( 2 x. _pi ) = ( _pi + _pi )
252	1 251	eqtri	|- T = ( _pi + _pi )
253	252	oveq2i	|- ( -u _pi + T ) = ( -u _pi + ( _pi + _pi ) )
254		negpicn	|- -u _pi e. CC
255	254 56 56	addassi	|- ( ( -u _pi + _pi ) + _pi ) = ( -u _pi + ( _pi + _pi ) )
256	255	eqcomi	|- ( -u _pi + ( _pi + _pi ) ) = ( ( -u _pi + _pi ) + _pi )
257	56	negidi	|- ( _pi + -u _pi ) = 0
258	56 254 257	addcomli	|- ( -u _pi + _pi ) = 0
259	258	oveq1i	|- ( ( -u _pi + _pi ) + _pi ) = ( 0 + _pi )
260	56	addid2i	|- ( 0 + _pi ) = _pi
261	259 260	eqtri	|- ( ( -u _pi + _pi ) + _pi ) = _pi
262	253 256 261	3eqtrri	|- _pi = ( -u _pi + T )
263	262	a1i	|- ( x e. ( -u _pi (,) 0 ) -> _pi = ( -u _pi + T ) )
264	160	a1i	|- ( x e. ( -u _pi (,) 0 ) -> -u _pi e. RR )
265	122	a1i	|- ( x e. ( -u _pi (,) 0 ) -> T e. RR )
266	241 230	syl	|- ( x e. ( -u _pi (,) 0 ) -> -u _pi < x )
267	264 247 265 266	ltadd1dd	|- ( x e. ( -u _pi (,) 0 ) -> ( -u _pi + T ) < ( x + T ) )
268	263 267	eqbrtrd	|- ( x e. ( -u _pi (,) 0 ) -> _pi < ( x + T ) )
269	246 250 268	ltled	|- ( x e. ( -u _pi (,) 0 ) -> _pi <_ ( x + T ) )
270		0red	|- ( x e. ( -u _pi (,) 0 ) -> 0 e. RR )
271	160 122	readdcli	|- ( -u _pi + T ) e. RR
272	271	a1i	|- ( x e. ( -u _pi (,) 0 ) -> ( -u _pi + T ) e. RR )
273	72	a1i	|- ( x e. ( -u _pi (,) 0 ) -> 0 < _pi )
274	273 262	breqtrdi	|- ( x e. ( -u _pi (,) 0 ) -> 0 < ( -u _pi + T ) )
275	270 272 250 274 267	lttrd	|- ( x e. ( -u _pi (,) 0 ) -> 0 < ( x + T ) )
276	270 250 275	ltled	|- ( x e. ( -u _pi (,) 0 ) -> 0 <_ ( x + T ) )
277	247	recnd	|- ( x e. ( -u _pi (,) 0 ) -> x e. CC )
278	123	a1i	|- ( x e. ( -u _pi (,) 0 ) -> T e. CC )
279	277 278	addcomd	|- ( x e. ( -u _pi (,) 0 ) -> ( x + T ) = ( T + x ) )
280		iooltub	|- ( ( -u _pi e. RR* /\ 0 e. RR* /\ x e. ( -u _pi (,) 0 ) ) -> x < 0 )
281	161 153 280	mp3an12	|- ( x e. ( -u _pi (,) 0 ) -> x < 0 )
282		ltaddneg	|- ( ( x e. RR /\ T e. RR ) -> ( x < 0 <-> ( T + x ) < T ) )
283	247 122 282	sylancl	|- ( x e. ( -u _pi (,) 0 ) -> ( x < 0 <-> ( T + x ) < T ) )
284	281 283	mpbid	|- ( x e. ( -u _pi (,) 0 ) -> ( T + x ) < T )
285	279 284	eqbrtrd	|- ( x e. ( -u _pi (,) 0 ) -> ( x + T ) < T )
286	276 285	jca	|- ( x e. ( -u _pi (,) 0 ) -> ( 0 <_ ( x + T ) /\ ( x + T ) < T ) )
287		modid2	|- ( ( ( x + T ) e. RR /\ T e. RR+ ) -> ( ( ( x + T ) mod T ) = ( x + T ) <-> ( 0 <_ ( x + T ) /\ ( x + T ) < T ) ) )
288	250 135 287	sylancl	|- ( x e. ( -u _pi (,) 0 ) -> ( ( ( x + T ) mod T ) = ( x + T ) <-> ( 0 <_ ( x + T ) /\ ( x + T ) < T ) ) )
289	286 288	mpbird	|- ( x e. ( -u _pi (,) 0 ) -> ( ( x + T ) mod T ) = ( x + T ) )
290	127	a1i	|- ( x e. RR -> ( ( x + T ) mod T ) = ( ( x + ( 1 x. T ) ) mod T ) )
291	135	a1i	|- ( x e. RR -> T e. RR+ )
292		1zzd	|- ( x e. RR -> 1 e. ZZ )
293	143 291 292 138	syl3anc	|- ( x e. RR -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
294	290 293	eqtrd	|- ( x e. RR -> ( ( x + T ) mod T ) = ( x mod T ) )
295	247 294	syl	|- ( x e. ( -u _pi (,) 0 ) -> ( ( x + T ) mod T ) = ( x mod T ) )
296	289 295	eqtr3d	|- ( x e. ( -u _pi (,) 0 ) -> ( x + T ) = ( x mod T ) )
297	269 296	breqtrd	|- ( x e. ( -u _pi (,) 0 ) -> _pi <_ ( x mod T ) )
298	246 249 297	lensymd	|- ( x e. ( -u _pi (,) 0 ) -> -. ( x mod T ) < _pi )
299	298	iffalsed	|- ( x e. ( -u _pi (,) 0 ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = -u 1 )
300	299	mpteq2ia	|- ( x e. ( -u _pi (,) 0 ) |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) = ( x e. ( -u _pi (,) 0 ) |-> -u 1 )
301	242 245 300	3eqtrri	|- ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) = ( F |` ( -u _pi (,) 0 ) )
302	301	oveq2i	|- ( RR _D ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) ) = ( RR _D ( F |` ( -u _pi (,) 0 ) ) )
303		iooretop	|- ( -u _pi (,) 0 ) e. ( topGen ` ran (,) )
304	303 201	eleqtri	|- ( -u _pi (,) 0 ) e. ( ( TopOpen ` CCfld ) |`t RR )
305	304	a1i	|- ( T. -> ( -u _pi (,) 0 ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
306	204	negcld	|- ( T. -> -u 1 e. CC )
307	198 305 306	dvmptconst	|- ( T. -> ( RR _D ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) ) = ( x e. ( -u _pi (,) 0 ) |-> 0 ) )
308	307	mptru	|- ( RR _D ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) ) = ( x e. ( -u _pi (,) 0 ) |-> 0 )
309		dvresioo	|- ( ( RR C_ RR /\ F : RR --> CC ) -> ( RR _D ( F |` ( -u _pi (,) 0 ) ) ) = ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) )
310	207 210 309	mp2an	|- ( RR _D ( F |` ( -u _pi (,) 0 ) ) ) = ( ( RR _D F ) |` ( -u _pi (,) 0 ) )
311	302 308 310	3eqtr3i	|- ( x e. ( -u _pi (,) 0 ) |-> 0 ) = ( ( RR _D F ) |` ( -u _pi (,) 0 ) )
312	311	dmeqi	|- dom ( x e. ( -u _pi (,) 0 ) |-> 0 ) = dom ( ( RR _D F ) |` ( -u _pi (,) 0 ) )
313		eqid	|- ( x e. ( -u _pi (,) 0 ) |-> 0 ) = ( x e. ( -u _pi (,) 0 ) |-> 0 )
314	93 313	dmmpti	|- dom ( x e. ( -u _pi (,) 0 ) |-> 0 ) = ( -u _pi (,) 0 )
315	312 314	eqtr3i	|- dom ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) = ( -u _pi (,) 0 )
316		ssdmres	|- ( ( -u _pi (,) 0 ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) = ( -u _pi (,) 0 ) )
317	315 316	mpbir	|- ( -u _pi (,) 0 ) C_ dom ( RR _D F )
318	317	sseli	|- ( x e. ( -u _pi (,) 0 ) -> x e. dom ( RR _D F ) )
319	241 318	elind	|- ( x e. ( -u _pi (,) 0 ) -> x e. ( ( -u _pi (,) _pi ) i^i dom ( RR _D F ) ) )
320	319 222	eleqtrrdi	|- ( x e. ( -u _pi (,) 0 ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
321	237 320	syl	|- ( ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) /\ -. 0 < x ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
322	225 321	pm2.61dan	|- ( ( x e. ( -u _pi (,) _pi ) /\ -. x = 0 ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
323	152 322	sylan	|- ( ( x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = 0 ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
324		eldifn	|- ( x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
325	324	adantr	|- ( ( x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = 0 ) -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
326	323 325	condan	|- ( x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x = 0 )
327		velsn	|- ( x e. { 0 } <-> x = 0 )
328	326 327	sylibr	|- ( x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x e. { 0 } )
329	328	ssriv	|- ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) C_ { 0 }
330		ssfi	|- ( ( { 0 } e. Fin /\ ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) C_ { 0 } ) -> ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) e. Fin )
331	151 329 330	mp2an	|- ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) e. Fin
332		inss1	|- ( ( -u _pi (,) _pi ) i^i dom ( RR _D F ) ) C_ ( -u _pi (,) _pi )
333	222 332	eqsstri	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ ( -u _pi (,) _pi )
334		ioosscn	|- ( -u _pi (,) _pi ) C_ CC
335	333 334	sstri	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ CC
336	335	a1i	|- ( T. -> dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ CC )
337		dvf	|- ( RR _D F ) : dom ( RR _D F ) --> CC
338		fresin	|- ( ( RR _D F ) : dom ( RR _D F ) --> CC -> ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) : ( dom ( RR _D F ) i^i ( -u _pi (,) _pi ) ) --> CC )
339		ffdm	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) : ( dom ( RR _D F ) i^i ( -u _pi (,) _pi ) ) --> CC -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) : dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) --> CC /\ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ ( dom ( RR _D F ) i^i ( -u _pi (,) _pi ) ) ) )
340	337 338 339	mp2b	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) : dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) --> CC /\ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ ( dom ( RR _D F ) i^i ( -u _pi (,) _pi ) ) )
341	340	simpli	|- ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) : dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) --> CC
342	341	a1i	|- ( T. -> ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) : dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) --> CC )
343	161	a1i	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> -u _pi e. RR* )
344	153	a1i	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> 0 e. RR* )
345		ioossre	|- ( -u _pi (,) _pi ) C_ RR
346	333	sseli	|- ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> x e. ( -u _pi (,) _pi ) )
347	345 346	sseldi	|- ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> x e. RR )
348	347	adantr	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> x e. RR )
349	346 230	syl	|- ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> -u _pi < x )
350	349	adantr	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> -u _pi < x )
351		simpr	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> x < 0 )
352	343 344 348 350 351	eliood	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> x e. ( -u _pi (,) 0 ) )
353		elun1	|- ( x e. ( -u _pi (,) 0 ) -> x e. ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) ) )
354	352 353	syl	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ x < 0 ) -> x e. ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) ) )
355		simpl	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
356		0red	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> 0 e. RR )
357	347	adantr	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> x e. RR )
358		simpr	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> -. x < 0 )
359	356 357 358	nltled	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> 0 <_ x )
360		id	|- ( x = 0 -> x = 0 )
361	207	a1i	|- ( T. -> RR C_ RR )
362		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
363	210	a1i	|- ( T. -> F : RR --> CC )
364		0red	|- ( T. -> 0 e. RR )
365		mnfxr	|- -oo e. RR*
366	365	a1i	|- ( T. -> -oo e. RR* )
367	364	mnfltd	|- ( T. -> -oo < 0 )
368	362 366 364 367	lptioo2	|- ( T. -> 0 e. ( ( limPt ` ( topGen ` ran (,) ) ) ` ( -oo (,) 0 ) ) )
369		incom	|- ( RR i^i ( -oo (,) 0 ) ) = ( ( -oo (,) 0 ) i^i RR )
370		ioossre	|- ( -oo (,) 0 ) C_ RR
371		df-ss	|- ( ( -oo (,) 0 ) C_ RR <-> ( ( -oo (,) 0 ) i^i RR ) = ( -oo (,) 0 ) )
372	370 371	mpbi	|- ( ( -oo (,) 0 ) i^i RR ) = ( -oo (,) 0 )
373	369 372	eqtr2i	|- ( -oo (,) 0 ) = ( RR i^i ( -oo (,) 0 ) )
374	373	fveq2i	|- ( ( limPt ` ( topGen ` ran (,) ) ) ` ( -oo (,) 0 ) ) = ( ( limPt ` ( topGen ` ran (,) ) ) ` ( RR i^i ( -oo (,) 0 ) ) )
375	368 374	eleqtrdi	|- ( T. -> 0 e. ( ( limPt ` ( topGen ` ran (,) ) ) ` ( RR i^i ( -oo (,) 0 ) ) ) )
376		pnfxr	|- +oo e. RR*
377	376	a1i	|- ( T. -> +oo e. RR* )
378	364	ltpnfd	|- ( T. -> 0 < +oo )
379	362 364 377 378	lptioo1	|- ( T. -> 0 e. ( ( limPt ` ( topGen ` ran (,) ) ) ` ( 0 (,) +oo ) ) )
380		incom	|- ( RR i^i ( 0 (,) +oo ) ) = ( ( 0 (,) +oo ) i^i RR )
381		ioossre	|- ( 0 (,) +oo ) C_ RR
382		df-ss	|- ( ( 0 (,) +oo ) C_ RR <-> ( ( 0 (,) +oo ) i^i RR ) = ( 0 (,) +oo ) )
383	381 382	mpbi	|- ( ( 0 (,) +oo ) i^i RR ) = ( 0 (,) +oo )
384	380 383	eqtr2i	|- ( 0 (,) +oo ) = ( RR i^i ( 0 (,) +oo ) )
385	384	fveq2i	|- ( ( limPt ` ( topGen ` ran (,) ) ) ` ( 0 (,) +oo ) ) = ( ( limPt ` ( topGen ` ran (,) ) ) ` ( RR i^i ( 0 (,) +oo ) ) )
386	379 385	eleqtrdi	|- ( T. -> 0 e. ( ( limPt ` ( topGen ` ran (,) ) ) ` ( RR i^i ( 0 (,) +oo ) ) ) )
387		eqid	|- ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) = ( x e. ( -u _pi (,) 0 ) |-> -u 1 )
388		mnfle	|- ( -u _pi e. RR* -> -oo <_ -u _pi )
389	161 388	ax-mp	|- -oo <_ -u _pi
390		iooss1	|- ( ( -oo e. RR* /\ -oo <_ -u _pi ) -> ( -u _pi (,) 0 ) C_ ( -oo (,) 0 ) )
391	365 389 390	mp2an	|- ( -u _pi (,) 0 ) C_ ( -oo (,) 0 )
392	391	a1i	|- ( T. -> ( -u _pi (,) 0 ) C_ ( -oo (,) 0 ) )
393		ioosscn	|- ( -oo (,) 0 ) C_ CC
394	392 393	sstrdi	|- ( T. -> ( -u _pi (,) 0 ) C_ CC )
395		0cnd	|- ( T. -> 0 e. CC )
396	387 394 306 395	constlimc	|- ( T. -> -u 1 e. ( ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) limCC 0 ) )
397		resabs1	|- ( ( -u _pi (,) 0 ) C_ ( -oo (,) 0 ) -> ( ( F |` ( -oo (,) 0 ) ) |` ( -u _pi (,) 0 ) ) = ( F |` ( -u _pi (,) 0 ) ) )
398	391 397	ax-mp	|- ( ( F |` ( -oo (,) 0 ) ) |` ( -u _pi (,) 0 ) ) = ( F |` ( -u _pi (,) 0 ) )
399	301 398	eqtr4i	|- ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) = ( ( F |` ( -oo (,) 0 ) ) |` ( -u _pi (,) 0 ) )
400	399	oveq1i	|- ( ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) limCC 0 ) = ( ( ( F |` ( -oo (,) 0 ) ) |` ( -u _pi (,) 0 ) ) limCC 0 )
401		fssres	|- ( ( F : RR --> CC /\ ( -oo (,) 0 ) C_ RR ) -> ( F |` ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
402	210 370 401	mp2an	|- ( F |` ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC
403	402	a1i	|- ( T. -> ( F |` ( -oo (,) 0 ) ) : ( -oo (,) 0 ) --> CC )
404	393	a1i	|- ( T. -> ( -oo (,) 0 ) C_ CC )
405		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) )
406		0le0	|- 0 <_ 0
407		elioc2	|- ( ( -u _pi e. RR* /\ 0 e. RR ) -> ( 0 e. ( -u _pi (,] 0 ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 <_ 0 ) ) )
408	161 71 407	mp2an	|- ( 0 e. ( -u _pi (,] 0 ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 <_ 0 ) )
409	71 166 406 408	mpbir3an	|- 0 e. ( -u _pi (,] 0 )
410	200	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
411		ovex	|- ( -oo (,] 0 ) e. _V
412		resttop	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( -oo (,] 0 ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) e. Top )
413	410 411 412	mp2an	|- ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) e. Top
414	161	a1i	|- ( T. -> -u _pi e. RR* )
415		eqid	|- ( ( topGen ` ran (,) ) |`t ( -oo (,] 0 ) ) = ( ( topGen ` ran (,) ) |`t ( -oo (,] 0 ) )
416	389	a1i	|- ( T. -> -oo <_ -u _pi )
417	366 414 364 362 415 416 364	iocopn	|- ( T. -> ( -u _pi (,] 0 ) e. ( ( topGen ` ran (,) ) |`t ( -oo (,] 0 ) ) )
418	417	mptru	|- ( -u _pi (,] 0 ) e. ( ( topGen ` ran (,) ) |`t ( -oo (,] 0 ) )
419	201	oveq1i	|- ( ( topGen ` ran (,) ) |`t ( -oo (,] 0 ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -oo (,] 0 ) )
420		iocssre	|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( -oo (,] 0 ) C_ RR )
421	365 71 420	mp2an	|- ( -oo (,] 0 ) C_ RR
422	197	elexi	|- RR e. _V
423		restabs	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( -oo (,] 0 ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -oo (,] 0 ) ) = ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) )
424	410 421 422 423	mp3an	|- ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -oo (,] 0 ) ) = ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) )
425	419 424	eqtri	|- ( ( topGen ` ran (,) ) |`t ( -oo (,] 0 ) ) = ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) )
426	418 425	eleqtri	|- ( -u _pi (,] 0 ) e. ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) )
427		isopn3i	|- ( ( ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) e. Top /\ ( -u _pi (,] 0 ) e. ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) ) ` ( -u _pi (,] 0 ) ) = ( -u _pi (,] 0 ) )
428	413 426 427	mp2an	|- ( ( int ` ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) ) ` ( -u _pi (,] 0 ) ) = ( -u _pi (,] 0 )
429		mnflt0	|- -oo < 0
430		ioounsn	|- ( ( -oo e. RR* /\ 0 e. RR* /\ -oo < 0 ) -> ( ( -oo (,) 0 ) u. { 0 } ) = ( -oo (,] 0 ) )
431	365 153 429 430	mp3an	|- ( ( -oo (,) 0 ) u. { 0 } ) = ( -oo (,] 0 )
432	431	eqcomi	|- ( -oo (,] 0 ) = ( ( -oo (,) 0 ) u. { 0 } )
433	432	oveq2i	|- ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) )
434	433	fveq2i	|- ( int ` ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) ) )
435		ioounsn	|- ( ( -u _pi e. RR* /\ 0 e. RR* /\ -u _pi < 0 ) -> ( ( -u _pi (,) 0 ) u. { 0 } ) = ( -u _pi (,] 0 ) )
436	161 153 166 435	mp3an	|- ( ( -u _pi (,) 0 ) u. { 0 } ) = ( -u _pi (,] 0 )
437	436	eqcomi	|- ( -u _pi (,] 0 ) = ( ( -u _pi (,) 0 ) u. { 0 } )
438	434 437	fveq12i	|- ( ( int ` ( ( TopOpen ` CCfld ) |`t ( -oo (,] 0 ) ) ) ` ( -u _pi (,] 0 ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) ) ) ` ( ( -u _pi (,) 0 ) u. { 0 } ) )
439	428 438	eqtr3i	|- ( -u _pi (,] 0 ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) ) ) ` ( ( -u _pi (,) 0 ) u. { 0 } ) )
440	409 439	eleqtri	|- 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) ) ) ` ( ( -u _pi (,) 0 ) u. { 0 } ) )
441	440	a1i	|- ( T. -> 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -oo (,) 0 ) u. { 0 } ) ) ) ` ( ( -u _pi (,) 0 ) u. { 0 } ) ) )
442	403 392 404 200 405 441	limcres	|- ( T. -> ( ( ( F |` ( -oo (,) 0 ) ) |` ( -u _pi (,) 0 ) ) limCC 0 ) = ( ( F |` ( -oo (,) 0 ) ) limCC 0 ) )
443	442	mptru	|- ( ( ( F |` ( -oo (,) 0 ) ) |` ( -u _pi (,) 0 ) ) limCC 0 ) = ( ( F |` ( -oo (,) 0 ) ) limCC 0 )
444	400 443	eqtri	|- ( ( x e. ( -u _pi (,) 0 ) |-> -u 1 ) limCC 0 ) = ( ( F |` ( -oo (,) 0 ) ) limCC 0 )
445	396 444	eleqtrdi	|- ( T. -> -u 1 e. ( ( F |` ( -oo (,) 0 ) ) limCC 0 ) )
446		eqid	|- ( x e. ( 0 (,) _pi ) |-> 1 ) = ( x e. ( 0 (,) _pi ) |-> 1 )
447		ioosscn	|- ( 0 (,) _pi ) C_ CC
448	447	a1i	|- ( T. -> ( 0 (,) _pi ) C_ CC )
449	446 448 204 395	constlimc	|- ( T. -> 1 e. ( ( x e. ( 0 (,) _pi ) |-> 1 ) limCC 0 ) )
450		ltpnf	|- ( _pi e. RR -> _pi < +oo )
451		xrltle	|- ( ( _pi e. RR* /\ +oo e. RR* ) -> ( _pi < +oo -> _pi <_ +oo ) )
452	155 376 451	mp2an	|- ( _pi < +oo -> _pi <_ +oo )
453	120 450 452	mp2b	|- _pi <_ +oo
454		iooss2	|- ( ( +oo e. RR* /\ _pi <_ +oo ) -> ( 0 (,) _pi ) C_ ( 0 (,) +oo ) )
455	376 453 454	mp2an	|- ( 0 (,) _pi ) C_ ( 0 (,) +oo )
456		resabs1	|- ( ( 0 (,) _pi ) C_ ( 0 (,) +oo ) -> ( ( F |` ( 0 (,) +oo ) ) |` ( 0 (,) _pi ) ) = ( F |` ( 0 (,) _pi ) ) )
457	455 456	ax-mp	|- ( ( F |` ( 0 (,) +oo ) ) |` ( 0 (,) _pi ) ) = ( F |` ( 0 (,) _pi ) )
458	195 457	eqtr4i	|- ( x e. ( 0 (,) _pi ) |-> 1 ) = ( ( F |` ( 0 (,) +oo ) ) |` ( 0 (,) _pi ) )
459	458	oveq1i	|- ( ( x e. ( 0 (,) _pi ) |-> 1 ) limCC 0 ) = ( ( ( F |` ( 0 (,) +oo ) ) |` ( 0 (,) _pi ) ) limCC 0 )
460		fssres	|- ( ( F : RR --> CC /\ ( 0 (,) +oo ) C_ RR ) -> ( F |` ( 0 (,) +oo ) ) : ( 0 (,) +oo ) --> CC )
461	210 381 460	mp2an	|- ( F |` ( 0 (,) +oo ) ) : ( 0 (,) +oo ) --> CC
462	461	a1i	|- ( T. -> ( F |` ( 0 (,) +oo ) ) : ( 0 (,) +oo ) --> CC )
463	455	a1i	|- ( T. -> ( 0 (,) _pi ) C_ ( 0 (,) +oo ) )
464		ioosscn	|- ( 0 (,) +oo ) C_ CC
465	464	a1i	|- ( T. -> ( 0 (,) +oo ) C_ CC )
466		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) )
467		elico2	|- ( ( 0 e. RR /\ _pi e. RR* ) -> ( 0 e. ( 0 [,) _pi ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 < _pi ) ) )
468	71 155 467	mp2an	|- ( 0 e. ( 0 [,) _pi ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 < _pi ) )
469	71 406 72 468	mpbir3an	|- 0 e. ( 0 [,) _pi )
470		ovex	|- ( 0 [,) +oo ) e. _V
471		resttop	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( 0 [,) +oo ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) e. Top )
472	410 470 471	mp2an	|- ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) e. Top
473	155	a1i	|- ( T. -> _pi e. RR* )
474		eqid	|- ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) )
475	453	a1i	|- ( T. -> _pi <_ +oo )
476	364 473 377 362 474 475	icoopn	|- ( T. -> ( 0 [,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) )
477	476	mptru	|- ( 0 [,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) )
478	201	oveq1i	|- ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( 0 [,) +oo ) )
479		rge0ssre	|- ( 0 [,) +oo ) C_ RR
480		restabs	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( 0 [,) +oo ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) )
481	410 479 422 480	mp3an	|- ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) )
482	478 481	eqtri	|- ( ( topGen ` ran (,) ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) )
483	477 482	eleqtri	|- ( 0 [,) _pi ) e. ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) )
484		isopn3i	|- ( ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) e. Top /\ ( 0 [,) _pi ) e. ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) ) ` ( 0 [,) _pi ) ) = ( 0 [,) _pi ) )
485	472 483 484	mp2an	|- ( ( int ` ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) ) ` ( 0 [,) _pi ) ) = ( 0 [,) _pi )
486		0ltpnf	|- 0 < +oo
487		snunioo1	|- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( ( 0 (,) +oo ) u. { 0 } ) = ( 0 [,) +oo ) )
488	153 376 486 487	mp3an	|- ( ( 0 (,) +oo ) u. { 0 } ) = ( 0 [,) +oo )
489	488	eqcomi	|- ( 0 [,) +oo ) = ( ( 0 (,) +oo ) u. { 0 } )
490	489	oveq2i	|- ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) )
491	490	fveq2i	|- ( int ` ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) ) )
492		snunioo1	|- ( ( 0 e. RR* /\ _pi e. RR* /\ 0 < _pi ) -> ( ( 0 (,) _pi ) u. { 0 } ) = ( 0 [,) _pi ) )
493	153 155 72 492	mp3an	|- ( ( 0 (,) _pi ) u. { 0 } ) = ( 0 [,) _pi )
494	493	eqcomi	|- ( 0 [,) _pi ) = ( ( 0 (,) _pi ) u. { 0 } )
495	491 494	fveq12i	|- ( ( int ` ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) ) ` ( 0 [,) _pi ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) ) ) ` ( ( 0 (,) _pi ) u. { 0 } ) )
496	485 495	eqtr3i	|- ( 0 [,) _pi ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) ) ) ` ( ( 0 (,) _pi ) u. { 0 } ) )
497	469 496	eleqtri	|- 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) ) ) ` ( ( 0 (,) _pi ) u. { 0 } ) )
498	497	a1i	|- ( T. -> 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( 0 (,) +oo ) u. { 0 } ) ) ) ` ( ( 0 (,) _pi ) u. { 0 } ) ) )
499	462 463 465 200 466 498	limcres	|- ( T. -> ( ( ( F |` ( 0 (,) +oo ) ) |` ( 0 (,) _pi ) ) limCC 0 ) = ( ( F |` ( 0 (,) +oo ) ) limCC 0 ) )
500	499	mptru	|- ( ( ( F |` ( 0 (,) +oo ) ) |` ( 0 (,) _pi ) ) limCC 0 ) = ( ( F |` ( 0 (,) +oo ) ) limCC 0 )
501	459 500	eqtri	|- ( ( x e. ( 0 (,) _pi ) |-> 1 ) limCC 0 ) = ( ( F |` ( 0 (,) +oo ) ) limCC 0 )
502	449 501	eleqtrdi	|- ( T. -> 1 e. ( ( F |` ( 0 (,) +oo ) ) limCC 0 ) )
503		neg1lt0	|- -u 1 < 0
504	109 71 108	lttri	|- ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
505	503 38 504	mp2an	|- -u 1 < 1
506	109 505	ltneii	|- -u 1 =/= 1
507	506	a1i	|- ( T. -> -u 1 =/= 1 )
508	200 361 362 363 364 375 386 445 502 507	jumpncnp	|- ( T. -> -. F e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
509	508	mptru	|- -. F e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` 0 )
510	208	a1i	|- ( 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> RR C_ CC )
511	210	a1i	|- ( 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> F : RR --> CC )
512	207	a1i	|- ( 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> RR C_ RR )
513		inss2	|- ( ( -u _pi (,) _pi ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F )
514	222 513	eqsstri	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ dom ( RR _D F )
515	514	sseli	|- ( 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> 0 e. dom ( RR _D F ) )
516	201 200	dvcnp2	|- ( ( ( RR C_ CC /\ F : RR --> CC /\ RR C_ RR ) /\ 0 e. dom ( RR _D F ) ) -> F e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
517	510 511 512 515 516	syl31anc	|- ( 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> F e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
518	509 517	mto	|- -. 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
519	518	a1i	|- ( x = 0 -> -. 0 e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
520	360 519	eqneltrd	|- ( x = 0 -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
521	520	necon2ai	|- ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> x =/= 0 )
522	521	adantr	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> x =/= 0 )
523	356 357 359 522	leneltd	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> 0 < x )
524	346 165	sylan	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ 0 < x ) -> x e. ( 0 (,) _pi ) )
525		elun2	|- ( x e. ( 0 (,) _pi ) -> x e. ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) ) )
526	524 525	syl	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ 0 < x ) -> x e. ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) ) )
527	355 523 526	syl2anc	|- ( ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ -. x < 0 ) -> x e. ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) ) )
528	354 527	pm2.61dan	|- ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> x e. ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) ) )
529		ovex	|- ( -u _pi (,) 0 ) e. _V
530		ovex	|- ( 0 (,) _pi ) e. _V
531	529 530	unipr	|- U. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } = ( ( -u _pi (,) 0 ) u. ( 0 (,) _pi ) )
532	528 531	eleqtrrdi	|- ( x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -> x e. U. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } )
533	532	ssriv	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ U. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) }
534	533	a1i	|- ( T. -> dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ U. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } )
535		ineq2	|- ( x = ( -u _pi (,) 0 ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) = ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( -u _pi (,) 0 ) ) )
536		retop	|- ( topGen ` ran (,) ) e. Top
537		ovex	|- ( RR _D F ) e. _V
538	537	resex	|- ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. _V
539	538	dmex	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. _V
540	536 539	pm3.2i	|- ( ( topGen ` ran (,) ) e. Top /\ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. _V )
541	320	ssriv	|- ( -u _pi (,) 0 ) C_ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
542		ssid	|- ( -u _pi (,) 0 ) C_ ( -u _pi (,) 0 )
543	303 541 542	3pm3.2i	|- ( ( -u _pi (,) 0 ) e. ( topGen ` ran (,) ) /\ ( -u _pi (,) 0 ) C_ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ ( -u _pi (,) 0 ) C_ ( -u _pi (,) 0 ) )
544		restopnb	|- ( ( ( ( topGen ` ran (,) ) e. Top /\ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. _V ) /\ ( ( -u _pi (,) 0 ) e. ( topGen ` ran (,) ) /\ ( -u _pi (,) 0 ) C_ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ ( -u _pi (,) 0 ) C_ ( -u _pi (,) 0 ) ) ) -> ( ( -u _pi (,) 0 ) e. ( topGen ` ran (,) ) <-> ( -u _pi (,) 0 ) e. ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) ) )
545	540 543 544	mp2an	|- ( ( -u _pi (,) 0 ) e. ( topGen ` ran (,) ) <-> ( -u _pi (,) 0 ) e. ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
546	303 545	mpbi	|- ( -u _pi (,) 0 ) e. ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
547		inss2	|- ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( -u _pi (,) 0 ) ) C_ ( -u _pi (,) 0 )
548	541 542	ssini	|- ( -u _pi (,) 0 ) C_ ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( -u _pi (,) 0 ) )
549	547 548	eqssi	|- ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( -u _pi (,) 0 ) ) = ( -u _pi (,) 0 )
550	201	oveq1i	|- ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
551	333 345	sstri	|- dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ RR
552		restabs	|- ( ( ( TopOpen ` CCfld ) e. Top /\ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) = ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
553	410 551 422 552	mp3an	|- ( ( ( TopOpen ` CCfld ) |`t RR ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) = ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
554	550 553	eqtr2i	|- ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) = ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
555	546 549 554	3eltr4i	|- ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( -u _pi (,) 0 ) ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
556	535 555	eqeltrdi	|- ( x = ( -u _pi (,) 0 ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
557	556	adantl	|- ( ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } /\ x = ( -u _pi (,) 0 ) ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
558		neqne	|- ( -. x = ( -u _pi (,) 0 ) -> x =/= ( -u _pi (,) 0 ) )
559		elprn1	|- ( ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } /\ x =/= ( -u _pi (,) 0 ) ) -> x = ( 0 (,) _pi ) )
560	558 559	sylan2	|- ( ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } /\ -. x = ( -u _pi (,) 0 ) ) -> x = ( 0 (,) _pi ) )
561		ineq2	|- ( x = ( 0 (,) _pi ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) = ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( 0 (,) _pi ) ) )
562	223	ssriv	|- ( 0 (,) _pi ) C_ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
563		ssid	|- ( 0 (,) _pi ) C_ ( 0 (,) _pi )
564	199 562 563	3pm3.2i	|- ( ( 0 (,) _pi ) e. ( topGen ` ran (,) ) /\ ( 0 (,) _pi ) C_ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ ( 0 (,) _pi ) C_ ( 0 (,) _pi ) )
565		restopnb	|- ( ( ( ( topGen ` ran (,) ) e. Top /\ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. _V ) /\ ( ( 0 (,) _pi ) e. ( topGen ` ran (,) ) /\ ( 0 (,) _pi ) C_ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) /\ ( 0 (,) _pi ) C_ ( 0 (,) _pi ) ) ) -> ( ( 0 (,) _pi ) e. ( topGen ` ran (,) ) <-> ( 0 (,) _pi ) e. ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) ) )
566	540 564 565	mp2an	|- ( ( 0 (,) _pi ) e. ( topGen ` ran (,) ) <-> ( 0 (,) _pi ) e. ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
567	199 566	mpbi	|- ( 0 (,) _pi ) e. ( ( topGen ` ran (,) ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
568		inss2	|- ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( 0 (,) _pi ) ) C_ ( 0 (,) _pi )
569	562 563	ssini	|- ( 0 (,) _pi ) C_ ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( 0 (,) _pi ) )
570	568 569	eqssi	|- ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( 0 (,) _pi ) ) = ( 0 (,) _pi )
571	567 570 554	3eltr4i	|- ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i ( 0 (,) _pi ) ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
572	561 571	eqeltrdi	|- ( x = ( 0 (,) _pi ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
573	560 572	syl	|- ( ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } /\ -. x = ( -u _pi (,) 0 ) ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
574	557 573	pm2.61dan	|- ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
575	574	adantl	|- ( ( T. /\ x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) e. ( ( TopOpen ` CCfld ) |`t dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
576		ssid	|- CC C_ CC
577	576	a1i	|- ( T. -> CC C_ CC )
578	394 395 577	constcncfg	|- ( T. -> ( x e. ( -u _pi (,) 0 ) |-> 0 ) e. ( ( -u _pi (,) 0 ) -cn-> CC ) )
579	578	mptru	|- ( x e. ( -u _pi (,) 0 ) |-> 0 ) e. ( ( -u _pi (,) 0 ) -cn-> CC )
580	579	a1i	|- ( x = ( -u _pi (,) 0 ) -> ( x e. ( -u _pi (,) 0 ) |-> 0 ) e. ( ( -u _pi (,) 0 ) -cn-> CC ) )
581		reseq2	|- ( x = ( -u _pi (,) 0 ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) 0 ) ) )
582		resabs1	|- ( ( -u _pi (,) 0 ) C_ ( -u _pi (,) _pi ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) 0 ) ) = ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) )
583	240 582	ax-mp	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) 0 ) ) = ( ( RR _D F ) |` ( -u _pi (,) 0 ) )
584	583 311	eqtr4i	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) 0 ) ) = ( x e. ( -u _pi (,) 0 ) |-> 0 )
585	581 584	eqtrdi	|- ( x = ( -u _pi (,) 0 ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) = ( x e. ( -u _pi (,) 0 ) |-> 0 ) )
586	535 549	eqtrdi	|- ( x = ( -u _pi (,) 0 ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) = ( -u _pi (,) 0 ) )
587	586	oveq1d	|- ( x = ( -u _pi (,) 0 ) -> ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) = ( ( -u _pi (,) 0 ) -cn-> CC ) )
588	580 585 587	3eltr4d	|- ( x = ( -u _pi (,) 0 ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) e. ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) )
589	588	adantl	|- ( ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } /\ x = ( -u _pi (,) 0 ) ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) e. ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) )
590	448 395 577	constcncfg	|- ( T. -> ( x e. ( 0 (,) _pi ) |-> 0 ) e. ( ( 0 (,) _pi ) -cn-> CC ) )
591	590	mptru	|- ( x e. ( 0 (,) _pi ) |-> 0 ) e. ( ( 0 (,) _pi ) -cn-> CC )
592	591	a1i	|- ( x = ( 0 (,) _pi ) -> ( x e. ( 0 (,) _pi ) |-> 0 ) e. ( ( 0 (,) _pi ) -cn-> CC ) )
593		reseq2	|- ( x = ( 0 (,) _pi ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) _pi ) ) )
594		resabs1	|- ( ( 0 (,) _pi ) C_ ( -u _pi (,) _pi ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) _pi ) ) = ( ( RR _D F ) |` ( 0 (,) _pi ) ) )
595	169 594	ax-mp	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) _pi ) ) = ( ( RR _D F ) |` ( 0 (,) _pi ) )
596	595 213	eqtr4i	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) _pi ) ) = ( x e. ( 0 (,) _pi ) |-> 0 )
597	593 596	eqtrdi	|- ( x = ( 0 (,) _pi ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) = ( x e. ( 0 (,) _pi ) |-> 0 ) )
598	561 570	eqtrdi	|- ( x = ( 0 (,) _pi ) -> ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) = ( 0 (,) _pi ) )
599	598	oveq1d	|- ( x = ( 0 (,) _pi ) -> ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) = ( ( 0 (,) _pi ) -cn-> CC ) )
600	592 597 599	3eltr4d	|- ( x = ( 0 (,) _pi ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) e. ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) )
601	560 600	syl	|- ( ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } /\ -. x = ( -u _pi (,) 0 ) ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) e. ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) )
602	589 601	pm2.61dan	|- ( x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) e. ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) )
603	602	adantl	|- ( ( T. /\ x e. { ( -u _pi (,) 0 ) , ( 0 (,) _pi ) } ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` x ) e. ( ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) i^i x ) -cn-> CC ) )
604	336 342 534 575 603	cncfuni	|- ( T. -> ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -cn-> CC ) )
605	604	mptru	|- ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. ( dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) -cn-> CC )
606		oveq1	|- ( x = -u _pi -> ( x (,) +oo ) = ( -u _pi (,) +oo ) )
607	606	reseq2d	|- ( x = -u _pi -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) +oo ) ) )
608		iooss2	|- ( ( +oo e. RR* /\ _pi <_ +oo ) -> ( -u _pi (,) _pi ) C_ ( -u _pi (,) +oo ) )
609	376 453 608	mp2an	|- ( -u _pi (,) _pi ) C_ ( -u _pi (,) +oo )
610		resabs2	|- ( ( -u _pi (,) _pi ) C_ ( -u _pi (,) +oo ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) +oo ) ) = ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
611	609 610	ax-mp	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -u _pi (,) +oo ) ) = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
612	607 611	eqtrdi	|- ( x = -u _pi -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) = ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
613		id	|- ( x = -u _pi -> x = -u _pi )
614	612 613	oveq12d	|- ( x = -u _pi -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi ) )
615	254	a1i	|- ( T. -> -u _pi e. CC )
616	313 394 395 615	constlimc	|- ( T. -> 0 e. ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC -u _pi ) )
617	616	mptru	|- 0 e. ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC -u _pi )
618	311	oveq1i	|- ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC -u _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) limCC -u _pi )
619	337	a1i	|- ( T. -> ( RR _D F ) : dom ( RR _D F ) --> CC )
620	160	a1i	|- ( T. -> -u _pi e. RR )
621	153	a1i	|- ( T. -> 0 e. RR* )
622	166	a1i	|- ( T. -> -u _pi < 0 )
623	317	a1i	|- ( T. -> ( -u _pi (,) 0 ) C_ dom ( RR _D F ) )
624	238	a1i	|- ( T. -> 0 <_ _pi )
625	619 620 621 622 623 473 624	limcresioolb	|- ( T. -> ( ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) limCC -u _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi ) )
626	625	mptru	|- ( ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) limCC -u _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi )
627	618 626	eqtri	|- ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC -u _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi )
628	617 627	eleqtri	|- 0 e. ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi )
629	628	ne0ii	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi ) =/= (/)
630	629	a1i	|- ( x = -u _pi -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC -u _pi ) =/= (/) )
631	614 630	eqnetrd	|- ( x = -u _pi -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) =/= (/) )
632	631	adantl	|- ( ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ x = -u _pi ) -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) =/= (/) )
633		eldifi	|- ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x e. ( -u _pi [,) _pi ) )
634	161	a1i	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> -u _pi e. RR* )
635	155	a1i	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> _pi e. RR* )
636		icossre	|- ( ( -u _pi e. RR /\ _pi e. RR* ) -> ( -u _pi [,) _pi ) C_ RR )
637	160 155 636	mp2an	|- ( -u _pi [,) _pi ) C_ RR
638	637	sseli	|- ( x e. ( -u _pi [,) _pi ) -> x e. RR )
639	638	adantr	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> x e. RR )
640	160	a1i	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> -u _pi e. RR )
641		icogelb	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ x e. ( -u _pi [,) _pi ) ) -> -u _pi <_ x )
642	161 155 641	mp3an12	|- ( x e. ( -u _pi [,) _pi ) -> -u _pi <_ x )
643	642	adantr	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> -u _pi <_ x )
644		neqne	|- ( -. x = -u _pi -> x =/= -u _pi )
645	644	adantl	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> x =/= -u _pi )
646	640 639 643 645	leneltd	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> -u _pi < x )
647		icoltub	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ x e. ( -u _pi [,) _pi ) ) -> x < _pi )
648	161 155 647	mp3an12	|- ( x e. ( -u _pi [,) _pi ) -> x < _pi )
649	648	adantr	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> x < _pi )
650	634 635 639 646 649	eliood	|- ( ( x e. ( -u _pi [,) _pi ) /\ -. x = -u _pi ) -> x e. ( -u _pi (,) _pi ) )
651	633 650	sylan	|- ( ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = -u _pi ) -> x e. ( -u _pi (,) _pi ) )
652		eldifn	|- ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
653	652	adantr	|- ( ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = -u _pi ) -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
654	651 653	eldifd	|- ( ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = -u _pi ) -> x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
655		oveq1	|- ( x = 0 -> ( x (,) +oo ) = ( 0 (,) +oo ) )
656	655	reseq2d	|- ( x = 0 -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) )
657	656 360	oveq12d	|- ( x = 0 -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) = ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) limCC 0 ) )
658	215 448 395 395	constlimc	|- ( T. -> 0 e. ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC 0 ) )
659	658	mptru	|- 0 e. ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC 0 )
660		resres	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) = ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( 0 (,) +oo ) ) )
661		iooin	|- ( ( ( -u _pi e. RR* /\ _pi e. RR* ) /\ ( 0 e. RR* /\ +oo e. RR* ) ) -> ( ( -u _pi (,) _pi ) i^i ( 0 (,) +oo ) ) = ( if ( -u _pi <_ 0 , 0 , -u _pi ) (,) if ( _pi <_ +oo , _pi , +oo ) ) )
662	161 155 153 376 661	mp4an	|- ( ( -u _pi (,) _pi ) i^i ( 0 (,) +oo ) ) = ( if ( -u _pi <_ 0 , 0 , -u _pi ) (,) if ( _pi <_ +oo , _pi , +oo ) )
663	167	iftruei	|- if ( -u _pi <_ 0 , 0 , -u _pi ) = 0
664	453	iftruei	|- if ( _pi <_ +oo , _pi , +oo ) = _pi
665	663 664	oveq12i	|- ( if ( -u _pi <_ 0 , 0 , -u _pi ) (,) if ( _pi <_ +oo , _pi , +oo ) ) = ( 0 (,) _pi )
666	662 665	eqtri	|- ( ( -u _pi (,) _pi ) i^i ( 0 (,) +oo ) ) = ( 0 (,) _pi )
667	666	reseq2i	|- ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( 0 (,) +oo ) ) ) = ( ( RR _D F ) |` ( 0 (,) _pi ) )
668	213	eqcomi	|- ( ( RR _D F ) |` ( 0 (,) _pi ) ) = ( x e. ( 0 (,) _pi ) |-> 0 )
669	660 667 668	3eqtrri	|- ( x e. ( 0 (,) _pi ) |-> 0 ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) )
670	669	oveq1i	|- ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC 0 ) = ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) limCC 0 )
671	659 670	eleqtri	|- 0 e. ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) limCC 0 )
672	671	ne0ii	|- ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) limCC 0 ) =/= (/)
673	672	a1i	|- ( x = 0 -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( 0 (,) +oo ) ) limCC 0 ) =/= (/) )
674	657 673	eqnetrd	|- ( x = 0 -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) =/= (/) )
675	654 326 674	3syl	|- ( ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = -u _pi ) -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) =/= (/) )
676	632 675	pm2.61dan	|- ( x e. ( ( -u _pi [,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) limCC x ) =/= (/) )
677		oveq2	|- ( x = _pi -> ( -oo (,) x ) = ( -oo (,) _pi ) )
678	677	reseq2d	|- ( x = _pi -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) _pi ) ) )
679		id	|- ( x = _pi -> x = _pi )
680	678 679	oveq12d	|- ( x = _pi -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) = ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) _pi ) ) limCC _pi ) )
681		iooss1	|- ( ( -oo e. RR* /\ -oo <_ -u _pi ) -> ( -u _pi (,) _pi ) C_ ( -oo (,) _pi ) )
682	365 389 681	mp2an	|- ( -u _pi (,) _pi ) C_ ( -oo (,) _pi )
683		resabs2	|- ( ( -u _pi (,) _pi ) C_ ( -oo (,) _pi ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) _pi ) ) = ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
684	682 683	ax-mp	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) _pi ) ) = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
685	684	oveq1i	|- ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) _pi ) ) limCC _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi )
686	680 685	eqtrdi	|- ( x = _pi -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi ) )
687	215 448 395 57	constlimc	|- ( T. -> 0 e. ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC _pi ) )
688	687	mptru	|- 0 e. ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC _pi )
689	213	oveq1i	|- ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC _pi ) = ( ( ( RR _D F ) |` ( 0 (,) _pi ) ) limCC _pi )
690	120	a1i	|- ( T. -> _pi e. RR )
691	72	a1i	|- ( T. -> 0 < _pi )
692	219	a1i	|- ( T. -> ( 0 (,) _pi ) C_ dom ( RR _D F ) )
693	167	a1i	|- ( T. -> -u _pi <_ 0 )
694	619 621 690 691 692 414 693	limcresiooub	|- ( T. -> ( ( ( RR _D F ) |` ( 0 (,) _pi ) ) limCC _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi ) )
695	694	mptru	|- ( ( ( RR _D F ) |` ( 0 (,) _pi ) ) limCC _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi )
696	689 695	eqtri	|- ( ( x e. ( 0 (,) _pi ) |-> 0 ) limCC _pi ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi )
697	688 696	eleqtri	|- 0 e. ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi )
698	697	ne0ii	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi ) =/= (/)
699	698	a1i	|- ( x = _pi -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) limCC _pi ) =/= (/) )
700	686 699	eqnetrd	|- ( x = _pi -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) =/= (/) )
701	700	adantl	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ x = _pi ) -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) =/= (/) )
702	161	a1i	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> -u _pi e. RR* )
703	155	a1i	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> _pi e. RR* )
704		negpitopissre	|- ( -u _pi (,] _pi ) C_ RR
705		eldifi	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x e. ( -u _pi (,] _pi ) )
706	704 705	sseldi	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x e. RR )
707	706	adantr	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> x e. RR )
708	161	a1i	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> -u _pi e. RR* )
709	155	a1i	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> _pi e. RR* )
710		iocgtlb	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ x e. ( -u _pi (,] _pi ) ) -> -u _pi < x )
711	708 709 705 710	syl3anc	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> -u _pi < x )
712	711	adantr	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> -u _pi < x )
713	120	a1i	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> _pi e. RR )
714		iocleub	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ x e. ( -u _pi (,] _pi ) ) -> x <_ _pi )
715	708 709 705 714	syl3anc	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> x <_ _pi )
716	715	adantr	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> x <_ _pi )
717		id	|- ( _pi = x -> _pi = x )
718	717	eqcomd	|- ( _pi = x -> x = _pi )
719	718	necon3bi	|- ( -. x = _pi -> _pi =/= x )
720	719	adantl	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> _pi =/= x )
721	707 713 716 720	leneltd	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> x < _pi )
722	702 703 707 712 721	eliood	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> x e. ( -u _pi (,) _pi ) )
723		eldifn	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
724	723	adantr	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> -. x e. dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
725	722 724	eldifd	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> x e. ( ( -u _pi (,) _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) )
726		oveq2	|- ( x = 0 -> ( -oo (,) x ) = ( -oo (,) 0 ) )
727	726	reseq2d	|- ( x = 0 -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) )
728	727 360	oveq12d	|- ( x = 0 -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) = ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) limCC 0 ) )
729	313 394 395 395	constlimc	|- ( T. -> 0 e. ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC 0 ) )
730	729	mptru	|- 0 e. ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC 0 )
731		resres	|- ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) = ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( -oo (,) 0 ) ) )
732		iooin	|- ( ( ( -u _pi e. RR* /\ _pi e. RR* ) /\ ( -oo e. RR* /\ 0 e. RR* ) ) -> ( ( -u _pi (,) _pi ) i^i ( -oo (,) 0 ) ) = ( if ( -u _pi <_ -oo , -oo , -u _pi ) (,) if ( _pi <_ 0 , _pi , 0 ) ) )
733	161 155 365 153 732	mp4an	|- ( ( -u _pi (,) _pi ) i^i ( -oo (,) 0 ) ) = ( if ( -u _pi <_ -oo , -oo , -u _pi ) (,) if ( _pi <_ 0 , _pi , 0 ) )
734		mnflt	|- ( -u _pi e. RR -> -oo < -u _pi )
735	160 734	ax-mp	|- -oo < -u _pi
736		xrltnle	|- ( ( -oo e. RR* /\ -u _pi e. RR* ) -> ( -oo < -u _pi <-> -. -u _pi <_ -oo ) )
737	365 161 736	mp2an	|- ( -oo < -u _pi <-> -. -u _pi <_ -oo )
738	735 737	mpbi	|- -. -u _pi <_ -oo
739	738	iffalsei	|- if ( -u _pi <_ -oo , -oo , -u _pi ) = -u _pi
740		xrltnle	|- ( ( 0 e. RR* /\ _pi e. RR* ) -> ( 0 < _pi <-> -. _pi <_ 0 ) )
741	153 155 740	mp2an	|- ( 0 < _pi <-> -. _pi <_ 0 )
742	72 741	mpbi	|- -. _pi <_ 0
743	742	iffalsei	|- if ( _pi <_ 0 , _pi , 0 ) = 0
744	739 743	oveq12i	|- ( if ( -u _pi <_ -oo , -oo , -u _pi ) (,) if ( _pi <_ 0 , _pi , 0 ) ) = ( -u _pi (,) 0 )
745	733 744	eqtri	|- ( ( -u _pi (,) _pi ) i^i ( -oo (,) 0 ) ) = ( -u _pi (,) 0 )
746	745	reseq2i	|- ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( -oo (,) 0 ) ) ) = ( ( RR _D F ) |` ( -u _pi (,) 0 ) )
747	311	eqcomi	|- ( ( RR _D F ) |` ( -u _pi (,) 0 ) ) = ( x e. ( -u _pi (,) 0 ) |-> 0 )
748	731 746 747	3eqtrri	|- ( x e. ( -u _pi (,) 0 ) |-> 0 ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) )
749	748	oveq1i	|- ( ( x e. ( -u _pi (,) 0 ) |-> 0 ) limCC 0 ) = ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) limCC 0 )
750	730 749	eleqtri	|- 0 e. ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) limCC 0 )
751	750	ne0ii	|- ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) limCC 0 ) =/= (/)
752	751	a1i	|- ( x = 0 -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) 0 ) ) limCC 0 ) =/= (/) )
753	728 752	eqnetrd	|- ( x = 0 -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) =/= (/) )
754	725 326 753	3syl	|- ( ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) /\ -. x = _pi ) -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) =/= (/) )
755	701 754	pm2.61dan	|- ( x e. ( ( -u _pi (,] _pi ) \ dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) ) -> ( ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) limCC x ) =/= (/) )
756		eqid	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) = ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 )
757		ioosscn	|- ( ( X - ( X mod T ) ) (,) X ) C_ CC
758	757	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( ( X - ( X mod T ) ) (,) X ) C_ CC )
759		1cnd	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> 1 e. CC )
760	27	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> X e. CC )
761	756 758 759 760	constlimc	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> 1 e. ( ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) limCC X ) )
762		ioossioc	|- ( 0 (,) _pi ) C_ ( 0 (,] _pi )
763	762	sseli	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( X mod T ) e. ( 0 (,] _pi ) )
764	763	iftrued	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) = 1 )
765	210	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> F : RR --> CC )
766		modcl	|- ( ( X e. RR /\ T e. RR+ ) -> ( X mod T ) e. RR )
767	3 135 766	mp2an	|- ( X mod T ) e. RR
768	3 767	resubcli	|- ( X - ( X mod T ) ) e. RR
769	768	rexri	|- ( X - ( X mod T ) ) e. RR*
770	769	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( X - ( X mod T ) ) e. RR* )
771	3	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> X e. RR )
772		elioore	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( X mod T ) e. RR )
773		ioogtlb	|- ( ( 0 e. RR* /\ _pi e. RR* /\ ( X mod T ) e. ( 0 (,) _pi ) ) -> 0 < ( X mod T ) )
774	153 155 773	mp3an12	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> 0 < ( X mod T ) )
775	772 774	elrpd	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( X mod T ) e. RR+ )
776	771 775	ltsubrpd	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( X - ( X mod T ) ) < X )
777		ioossre	|- ( ( X - ( X mod T ) ) (,) X ) C_ RR
778	777	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( ( X - ( X mod T ) ) (,) X ) C_ RR )
779	365	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> -oo e. RR* )
780		mnflt	|- ( ( X - ( X mod T ) ) e. RR -> -oo < ( X - ( X mod T ) ) )
781		xrltle	|- ( ( -oo e. RR* /\ ( X - ( X mod T ) ) e. RR* ) -> ( -oo < ( X - ( X mod T ) ) -> -oo <_ ( X - ( X mod T ) ) ) )
782	365 769 781	mp2an	|- ( -oo < ( X - ( X mod T ) ) -> -oo <_ ( X - ( X mod T ) ) )
783	768 780 782	mp2b	|- -oo <_ ( X - ( X mod T ) )
784	783	a1i	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> -oo <_ ( X - ( X mod T ) ) )
785	765 770 771 776 778 779 784	limcresiooub	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( ( F |` ( ( X - ( X mod T ) ) (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) X ) ) limCC X ) )
786		iooltub	|- ( ( 0 e. RR* /\ _pi e. RR* /\ ( X mod T ) e. ( 0 (,) _pi ) ) -> ( X mod T ) < _pi )
787	153 155 786	mp3an12	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( X mod T ) < _pi )
788	210	a1i	|- ( ( X mod T ) < _pi -> F : RR --> CC )
789	777	a1i	|- ( ( X mod T ) < _pi -> ( ( X - ( X mod T ) ) (,) X ) C_ RR )
790	788 789	feqresmpt	|- ( ( X mod T ) < _pi -> ( F |` ( ( X - ( X mod T ) ) (,) X ) ) = ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> ( F ` x ) ) )
791		elioore	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) -> x e. RR )
792	791 110 147	sylancl	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
793	792	adantl	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
794	791	adantl	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> x e. RR )
795	135	a1i	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> T e. RR+ )
796	794 795	modcld	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( x mod T ) e. RR )
797	767	a1i	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( X mod T ) e. RR )
798	120	a1i	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> _pi e. RR )
799	3	a1i	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) -> X e. RR )
800	135	a1i	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) -> T e. RR+ )
801		ioossico	|- ( ( X - ( X mod T ) ) (,) X ) C_ ( ( X - ( X mod T ) ) [,) X )
802	801	sseli	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) -> x e. ( ( X - ( X mod T ) ) [,) X ) )
803	799 800 802	ltmod	|- ( x e. ( ( X - ( X mod T ) ) (,) X ) -> ( x mod T ) < ( X mod T ) )
804	803	adantl	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( x mod T ) < ( X mod T ) )
805		simpl	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( X mod T ) < _pi )
806	796 797 798 804 805	lttrd	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( x mod T ) < _pi )
807	806	iftrued	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
808	793 807	eqtrd	|- ( ( ( X mod T ) < _pi /\ x e. ( ( X - ( X mod T ) ) (,) X ) ) -> ( F ` x ) = 1 )
809	808	mpteq2dva	|- ( ( X mod T ) < _pi -> ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> ( F ` x ) ) = ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) )
810	790 809	eqtrd	|- ( ( X mod T ) < _pi -> ( F |` ( ( X - ( X mod T ) ) (,) X ) ) = ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) )
811	787 810	syl	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( F |` ( ( X - ( X mod T ) ) (,) X ) ) = ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) )
812	811	oveq1d	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( ( F |` ( ( X - ( X mod T ) ) (,) X ) ) limCC X ) = ( ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) limCC X ) )
813	785 812	eqtr3d	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( x e. ( ( X - ( X mod T ) ) (,) X ) |-> 1 ) limCC X ) )
814	761 764 813	3eltr4d	|- ( ( X mod T ) e. ( 0 (,) _pi ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
815		eqid	|- ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) = ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 )
816		ioossre	|- ( ( X - _pi ) (,) X ) C_ RR
817	816	a1i	|- ( T. -> ( ( X - _pi ) (,) X ) C_ RR )
818	817 208	sstrdi	|- ( T. -> ( ( X - _pi ) (,) X ) C_ CC )
819	27	a1i	|- ( T. -> X e. CC )
820	815 818 306 819	constlimc	|- ( T. -> -u 1 e. ( ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) limCC X ) )
821	820	mptru	|- -u 1 e. ( ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) limCC X )
822	821	a1i	|- ( ( X mod T ) = 0 -> -u 1 e. ( ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) limCC X ) )
823		id	|- ( ( X mod T ) = 0 -> ( X mod T ) = 0 )
824		lbioc	|- -. 0 e. ( 0 (,] _pi )
825	824	a1i	|- ( ( X mod T ) = 0 -> -. 0 e. ( 0 (,] _pi ) )
826	823 825	eqneltrd	|- ( ( X mod T ) = 0 -> -. ( X mod T ) e. ( 0 (,] _pi ) )
827	826	iffalsed	|- ( ( X mod T ) = 0 -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) = -u 1 )
828	210	a1i	|- ( ( X mod T ) = 0 -> F : RR --> CC )
829	816	a1i	|- ( ( X mod T ) = 0 -> ( ( X - _pi ) (,) X ) C_ RR )
830	828 829	feqresmpt	|- ( ( X mod T ) = 0 -> ( F |` ( ( X - _pi ) (,) X ) ) = ( x e. ( ( X - _pi ) (,) X ) |-> ( F ` x ) ) )
831	829	sselda	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> x e. RR )
832	831 110 147	sylancl	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
833	120	a1i	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> _pi e. RR )
834	135	a1i	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> T e. RR+ )
835	831 834	modcld	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( x mod T ) e. RR )
836	3 120	resubcli	|- ( X - _pi ) e. RR
837	836	a1i	|- ( x e. ( ( X - _pi ) (,) X ) -> ( X - _pi ) e. RR )
838	122	a1i	|- ( x e. ( ( X - _pi ) (,) X ) -> T e. RR )
839	837 838	readdcld	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( X - _pi ) + T ) e. RR )
840		elioore	|- ( x e. ( ( X - _pi ) (,) X ) -> x e. RR )
841	840 838	readdcld	|- ( x e. ( ( X - _pi ) (,) X ) -> ( x + T ) e. RR )
842	3	a1i	|- ( x e. ( ( X - _pi ) (,) X ) -> X e. RR )
843	836	rexri	|- ( X - _pi ) e. RR*
844	843	a1i	|- ( x e. ( ( X - _pi ) (,) X ) -> ( X - _pi ) e. RR* )
845	842	rexrd	|- ( x e. ( ( X - _pi ) (,) X ) -> X e. RR* )
846		id	|- ( x e. ( ( X - _pi ) (,) X ) -> x e. ( ( X - _pi ) (,) X ) )
847		ioogtlb	|- ( ( ( X - _pi ) e. RR* /\ X e. RR* /\ x e. ( ( X - _pi ) (,) X ) ) -> ( X - _pi ) < x )
848	844 845 846 847	syl3anc	|- ( x e. ( ( X - _pi ) (,) X ) -> ( X - _pi ) < x )
849	837 840 838 848	ltadd1dd	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( X - _pi ) + T ) < ( x + T ) )
850	839 841 842 849	ltsub1dd	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( X - _pi ) + T ) - X ) < ( ( x + T ) - X ) )
851	850	adantl	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( X - _pi ) + T ) - X ) < ( ( x + T ) - X ) )
852	252	oveq2i	|- ( ( X - _pi ) + T ) = ( ( X - _pi ) + ( _pi + _pi ) )
853	56 56	addcli	|- ( _pi + _pi ) e. CC
854		subadd23	|- ( ( X e. CC /\ _pi e. CC /\ ( _pi + _pi ) e. CC ) -> ( ( X - _pi ) + ( _pi + _pi ) ) = ( X + ( ( _pi + _pi ) - _pi ) ) )
855	27 56 853 854	mp3an	|- ( ( X - _pi ) + ( _pi + _pi ) ) = ( X + ( ( _pi + _pi ) - _pi ) )
856	56 56	pncan3oi	|- ( ( _pi + _pi ) - _pi ) = _pi
857	856	oveq2i	|- ( X + ( ( _pi + _pi ) - _pi ) ) = ( X + _pi )
858	852 855 857	3eqtri	|- ( ( X - _pi ) + T ) = ( X + _pi )
859	858	oveq1i	|- ( ( ( X - _pi ) + T ) - X ) = ( ( X + _pi ) - X )
860		pncan2	|- ( ( X e. CC /\ _pi e. CC ) -> ( ( X + _pi ) - X ) = _pi )
861	27 56 860	mp2an	|- ( ( X + _pi ) - X ) = _pi
862	859 861	eqtr2i	|- _pi = ( ( ( X - _pi ) + T ) - X )
863	862	a1i	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> _pi = ( ( ( X - _pi ) + T ) - X ) )
864	841 842	resubcld	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( x + T ) - X ) e. RR )
865		modabs2	|- ( ( ( ( x + T ) - X ) e. RR /\ T e. RR+ ) -> ( ( ( ( x + T ) - X ) mod T ) mod T ) = ( ( ( x + T ) - X ) mod T ) )
866	864 135 865	sylancl	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( ( x + T ) - X ) mod T ) mod T ) = ( ( ( x + T ) - X ) mod T ) )
867	135	a1i	|- ( x e. ( ( X - _pi ) (,) X ) -> T e. RR+ )
868		0red	|- ( x e. ( ( X - _pi ) (,) X ) -> 0 e. RR )
869	839 842	resubcld	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( X - _pi ) + T ) - X ) e. RR )
870	72 862	breqtri	|- 0 < ( ( ( X - _pi ) + T ) - X )
871	870	a1i	|- ( x e. ( ( X - _pi ) (,) X ) -> 0 < ( ( ( X - _pi ) + T ) - X ) )
872	868 869 864 871 850	lttrd	|- ( x e. ( ( X - _pi ) (,) X ) -> 0 < ( ( x + T ) - X ) )
873	868 864 872	ltled	|- ( x e. ( ( X - _pi ) (,) X ) -> 0 <_ ( ( x + T ) - X ) )
874	842 838	readdcld	|- ( x e. ( ( X - _pi ) (,) X ) -> ( X + T ) e. RR )
875		iooltub	|- ( ( ( X - _pi ) e. RR* /\ X e. RR* /\ x e. ( ( X - _pi ) (,) X ) ) -> x < X )
876	844 845 846 875	syl3anc	|- ( x e. ( ( X - _pi ) (,) X ) -> x < X )
877	840 842 838 876	ltadd1dd	|- ( x e. ( ( X - _pi ) (,) X ) -> ( x + T ) < ( X + T ) )
878	841 874 842 877	ltsub1dd	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( x + T ) - X ) < ( ( X + T ) - X ) )
879		pncan2	|- ( ( X e. CC /\ T e. CC ) -> ( ( X + T ) - X ) = T )
880	27 123 879	mp2an	|- ( ( X + T ) - X ) = T
881	878 880	breqtrdi	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( x + T ) - X ) < T )
882		modid	|- ( ( ( ( ( x + T ) - X ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( ( x + T ) - X ) /\ ( ( x + T ) - X ) < T ) ) -> ( ( ( x + T ) - X ) mod T ) = ( ( x + T ) - X ) )
883	864 867 873 881 882	syl22anc	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( x + T ) - X ) mod T ) = ( ( x + T ) - X ) )
884	866 883	eqtr2d	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( x + T ) - X ) = ( ( ( ( x + T ) - X ) mod T ) mod T ) )
885	884	adantl	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( x + T ) - X ) = ( ( ( ( x + T ) - X ) mod T ) mod T ) )
886		oveq2	|- ( ( X mod T ) = 0 -> ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) = ( ( ( ( x + T ) - X ) mod T ) + 0 ) )
887	886	adantr	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) = ( ( ( ( x + T ) - X ) mod T ) + 0 ) )
888	864 867	modcld	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( x + T ) - X ) mod T ) e. RR )
889	888	recnd	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( x + T ) - X ) mod T ) e. CC )
890	889	addid1d	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( ( x + T ) - X ) mod T ) + 0 ) = ( ( ( x + T ) - X ) mod T ) )
891	890	adantl	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( ( x + T ) - X ) mod T ) + 0 ) = ( ( ( x + T ) - X ) mod T ) )
892	887 891	eqtr2d	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( x + T ) - X ) mod T ) = ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) )
893	892	oveq1d	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( ( x + T ) - X ) mod T ) mod T ) = ( ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) mod T ) )
894		modaddabs	|- ( ( ( ( x + T ) - X ) e. RR /\ X e. RR /\ T e. RR+ ) -> ( ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) mod T ) = ( ( ( ( x + T ) - X ) + X ) mod T ) )
895	864 842 867 894	syl3anc	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) mod T ) = ( ( ( ( x + T ) - X ) + X ) mod T ) )
896	895	adantl	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( ( ( x + T ) - X ) mod T ) + ( X mod T ) ) mod T ) = ( ( ( ( x + T ) - X ) + X ) mod T ) )
897	885 893 896	3eqtrd	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( x + T ) - X ) = ( ( ( ( x + T ) - X ) + X ) mod T ) )
898	145	recnd	|- ( x e. RR -> ( x + T ) e. CC )
899	27	a1i	|- ( x e. RR -> X e. CC )
900	898 899	npcand	|- ( x e. RR -> ( ( ( x + T ) - X ) + X ) = ( x + T ) )
901	124	a1i	|- ( x e. RR -> ( 1 x. T ) = T )
902	901	oveq2d	|- ( x e. RR -> ( x + ( 1 x. T ) ) = ( x + T ) )
903	900 902	eqtr4d	|- ( x e. RR -> ( ( ( x + T ) - X ) + X ) = ( x + ( 1 x. T ) ) )
904	903	oveq1d	|- ( x e. RR -> ( ( ( ( x + T ) - X ) + X ) mod T ) = ( ( x + ( 1 x. T ) ) mod T ) )
905	840 904	syl	|- ( x e. ( ( X - _pi ) (,) X ) -> ( ( ( ( x + T ) - X ) + X ) mod T ) = ( ( x + ( 1 x. T ) ) mod T ) )
906	905	adantl	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( ( ( x + T ) - X ) + X ) mod T ) = ( ( x + ( 1 x. T ) ) mod T ) )
907		1zzd	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> 1 e. ZZ )
908	831 834 907 138	syl3anc	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
909	897 906 908	3eqtrrd	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( x mod T ) = ( ( x + T ) - X ) )
910	851 863 909	3brtr4d	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> _pi < ( x mod T ) )
911	833 835 910	ltled	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> _pi <_ ( x mod T ) )
912	833 835 911	lensymd	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> -. ( x mod T ) < _pi )
913	912	iffalsed	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = -u 1 )
914	832 913	eqtrd	|- ( ( ( X mod T ) = 0 /\ x e. ( ( X - _pi ) (,) X ) ) -> ( F ` x ) = -u 1 )
915	914	mpteq2dva	|- ( ( X mod T ) = 0 -> ( x e. ( ( X - _pi ) (,) X ) |-> ( F ` x ) ) = ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) )
916	830 915	eqtr2d	|- ( ( X mod T ) = 0 -> ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) = ( F |` ( ( X - _pi ) (,) X ) ) )
917	916	oveq1d	|- ( ( X mod T ) = 0 -> ( ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) limCC X ) = ( ( F |` ( ( X - _pi ) (,) X ) ) limCC X ) )
918	843	a1i	|- ( T. -> ( X - _pi ) e. RR* )
919	3	a1i	|- ( T. -> X e. RR )
920		ltsubrp	|- ( ( X e. RR /\ _pi e. RR+ ) -> ( X - _pi ) < X )
921	3 184 920	mp2an	|- ( X - _pi ) < X
922	921	a1i	|- ( T. -> ( X - _pi ) < X )
923		mnflt	|- ( ( X - _pi ) e. RR -> -oo < ( X - _pi ) )
924		xrltle	|- ( ( -oo e. RR* /\ ( X - _pi ) e. RR* ) -> ( -oo < ( X - _pi ) -> -oo <_ ( X - _pi ) ) )
925	365 843 924	mp2an	|- ( -oo < ( X - _pi ) -> -oo <_ ( X - _pi ) )
926	836 923 925	mp2b	|- -oo <_ ( X - _pi )
927	926	a1i	|- ( T. -> -oo <_ ( X - _pi ) )
928	363 918 919 922 817 366 927	limcresiooub	|- ( T. -> ( ( F |` ( ( X - _pi ) (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) X ) ) limCC X ) )
929	928	mptru	|- ( ( F |` ( ( X - _pi ) (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) X ) ) limCC X )
930	917 929	eqtr2di	|- ( ( X mod T ) = 0 -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( x e. ( ( X - _pi ) (,) X ) |-> -u 1 ) limCC X ) )
931	822 827 930	3eltr4d	|- ( ( X mod T ) = 0 -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
932	931	adantl	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ ( X mod T ) = 0 ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
933	155	a1i	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> _pi e. RR* )
934	122	rexri	|- T e. RR*
935	934	a1i	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> T e. RR* )
936	767	rexri	|- ( X mod T ) e. RR*
937	936	a1i	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> ( X mod T ) e. RR* )
938	120	a1i	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> _pi e. RR )
939	767	a1i	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> ( X mod T ) e. RR )
940		pm4.56	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) <-> -. ( ( X mod T ) e. ( 0 (,) _pi ) \/ ( X mod T ) = 0 ) )
941	940	biimpi	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> -. ( ( X mod T ) e. ( 0 (,) _pi ) \/ ( X mod T ) = 0 ) )
942		olc	|- ( ( X mod T ) = 0 -> ( ( X mod T ) e. ( 0 (,) _pi ) \/ ( X mod T ) = 0 ) )
943	942	adantl	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) = 0 ) -> ( ( X mod T ) e. ( 0 (,) _pi ) \/ ( X mod T ) = 0 ) )
944	153	a1i	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> 0 e. RR* )
945	155	a1i	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> _pi e. RR* )
946	767	a1i	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> ( X mod T ) e. RR )
947		0red	|- ( ( X mod T ) =/= 0 -> 0 e. RR )
948	767	a1i	|- ( ( X mod T ) =/= 0 -> ( X mod T ) e. RR )
949		modge0	|- ( ( X e. RR /\ T e. RR+ ) -> 0 <_ ( X mod T ) )
950	3 135 949	mp2an	|- 0 <_ ( X mod T )
951	950	a1i	|- ( ( X mod T ) =/= 0 -> 0 <_ ( X mod T ) )
952		id	|- ( ( X mod T ) =/= 0 -> ( X mod T ) =/= 0 )
953	947 948 951 952	leneltd	|- ( ( X mod T ) =/= 0 -> 0 < ( X mod T ) )
954	953	adantl	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> 0 < ( X mod T ) )
955		simpl	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> ( X mod T ) < _pi )
956	944 945 946 954 955	eliood	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> ( X mod T ) e. ( 0 (,) _pi ) )
957	956	orcd	|- ( ( ( X mod T ) < _pi /\ ( X mod T ) =/= 0 ) -> ( ( X mod T ) e. ( 0 (,) _pi ) \/ ( X mod T ) = 0 ) )
958	943 957	pm2.61dane	|- ( ( X mod T ) < _pi -> ( ( X mod T ) e. ( 0 (,) _pi ) \/ ( X mod T ) = 0 ) )
959	941 958	nsyl	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> -. ( X mod T ) < _pi )
960	938 939 959	nltled	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> _pi <_ ( X mod T ) )
961		modlt	|- ( ( X e. RR /\ T e. RR+ ) -> ( X mod T ) < T )
962	3 135 961	mp2an	|- ( X mod T ) < T
963	962	a1i	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> ( X mod T ) < T )
964	933 935 937 960 963	elicod	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> ( X mod T ) e. ( _pi [,) T ) )
965		eqid	|- ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) = ( x e. ( ( X - _pi ) (,) X ) |-> 1 )
966	965 818 204 819	constlimc	|- ( T. -> 1 e. ( ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) limCC X ) )
967	966	mptru	|- 1 e. ( ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) limCC X )
968	967	a1i	|- ( ( X mod T ) = _pi -> 1 e. ( ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) limCC X ) )
969		id	|- ( ( X mod T ) = _pi -> ( X mod T ) = _pi )
970		ubioc1	|- ( ( 0 e. RR* /\ _pi e. RR* /\ 0 < _pi ) -> _pi e. ( 0 (,] _pi ) )
971	153 155 72 970	mp3an	|- _pi e. ( 0 (,] _pi )
972	969 971	eqeltrdi	|- ( ( X mod T ) = _pi -> ( X mod T ) e. ( 0 (,] _pi ) )
973	972	iftrued	|- ( ( X mod T ) = _pi -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) = 1 )
974	363 817	feqresmpt	|- ( T. -> ( F |` ( ( X - _pi ) (,) X ) ) = ( x e. ( ( X - _pi ) (,) X ) |-> ( F ` x ) ) )
975	974	mptru	|- ( F |` ( ( X - _pi ) (,) X ) ) = ( x e. ( ( X - _pi ) (,) X ) |-> ( F ` x ) )
976	840 110 147	sylancl	|- ( x e. ( ( X - _pi ) (,) X ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
977	976	adantl	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
978		simpr	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> x e. ( ( X - _pi ) (,) X ) )
979	969	eqcomd	|- ( ( X mod T ) = _pi -> _pi = ( X mod T ) )
980	979	oveq2d	|- ( ( X mod T ) = _pi -> ( X - _pi ) = ( X - ( X mod T ) ) )
981	980	oveq1d	|- ( ( X mod T ) = _pi -> ( ( X - _pi ) (,) X ) = ( ( X - ( X mod T ) ) (,) X ) )
982	981	adantr	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> ( ( X - _pi ) (,) X ) = ( ( X - ( X mod T ) ) (,) X ) )
983	978 982	eleqtrd	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> x e. ( ( X - ( X mod T ) ) (,) X ) )
984	983 803	syl	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> ( x mod T ) < ( X mod T ) )
985		simpl	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> ( X mod T ) = _pi )
986	984 985	breqtrd	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> ( x mod T ) < _pi )
987	986	iftrued	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
988	977 987	eqtrd	|- ( ( ( X mod T ) = _pi /\ x e. ( ( X - _pi ) (,) X ) ) -> ( F ` x ) = 1 )
989	988	mpteq2dva	|- ( ( X mod T ) = _pi -> ( x e. ( ( X - _pi ) (,) X ) |-> ( F ` x ) ) = ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) )
990	975 989	syl5req	|- ( ( X mod T ) = _pi -> ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) = ( F |` ( ( X - _pi ) (,) X ) ) )
991	990	oveq1d	|- ( ( X mod T ) = _pi -> ( ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) limCC X ) = ( ( F |` ( ( X - _pi ) (,) X ) ) limCC X ) )
992	991 929	eqtr2di	|- ( ( X mod T ) = _pi -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( x e. ( ( X - _pi ) (,) X ) |-> 1 ) limCC X ) )
993	968 973 992	3eltr4d	|- ( ( X mod T ) = _pi -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
994	993	adantl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ ( X mod T ) = _pi ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
995	155	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> _pi e. RR* )
996	934	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> T e. RR* )
997	767	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> ( X mod T ) e. RR )
998	120	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> _pi e. RR )
999		icogelb	|- ( ( _pi e. RR* /\ T e. RR* /\ ( X mod T ) e. ( _pi [,) T ) ) -> _pi <_ ( X mod T ) )
1000	155 934 999	mp3an12	|- ( ( X mod T ) e. ( _pi [,) T ) -> _pi <_ ( X mod T ) )
1001	1000	adantr	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> _pi <_ ( X mod T ) )
1002		neqne	|- ( -. ( X mod T ) = _pi -> ( X mod T ) =/= _pi )
1003	1002	adantl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> ( X mod T ) =/= _pi )
1004	998 997 1001 1003	leneltd	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> _pi < ( X mod T ) )
1005	962	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> ( X mod T ) < T )
1006	995 996 997 1004 1005	eliood	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> ( X mod T ) e. ( _pi (,) T ) )
1007		eqid	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 ) = ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 )
1008		ioossre	|- ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) C_ RR
1009	1008	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) C_ RR )
1010	1009 208	sstrdi	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) C_ CC )
1011		neg1cn	|- -u 1 e. CC
1012	1011	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> -u 1 e. CC )
1013	27	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> X e. CC )
1014	1007 1010 1012 1013	constlimc	|- ( ( X mod T ) e. ( _pi (,) T ) -> -u 1 e. ( ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 ) limCC X ) )
1015	153	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> 0 e. RR* )
1016	120	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> _pi e. RR )
1017	936	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( X mod T ) e. RR* )
1018		ioogtlb	|- ( ( _pi e. RR* /\ T e. RR* /\ ( X mod T ) e. ( _pi (,) T ) ) -> _pi < ( X mod T ) )
1019	155 934 1018	mp3an12	|- ( ( X mod T ) e. ( _pi (,) T ) -> _pi < ( X mod T ) )
1020	1015 1016 1017 1019	gtnelioc	|- ( ( X mod T ) e. ( _pi (,) T ) -> -. ( X mod T ) e. ( 0 (,] _pi ) )
1021	1020	iffalsed	|- ( ( X mod T ) e. ( _pi (,) T ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) = -u 1 )
1022	1008	a1i	|- ( T. -> ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) C_ RR )
1023	363 1022	feqresmpt	|- ( T. -> ( F |` ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) = ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> ( F ` x ) ) )
1024	1023	mptru	|- ( F |` ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) = ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> ( F ` x ) )
1025		elioore	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> x e. RR )
1026	1025 110 147	sylancl	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
1027	1026	adantl	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
1028	120	a1i	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> _pi e. RR )
1029	135	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> T e. RR+ )
1030	1025 1029	modcld	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( x mod T ) e. RR )
1031	1030	adantl	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> ( x mod T ) e. RR )
1032	3 120	readdcli	|- ( X + _pi ) e. RR
1033	1032	recni	|- ( X + _pi ) e. CC
1034	1033	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X + _pi ) e. CC )
1035	27	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> X e. CC )
1036	767	recni	|- ( X mod T ) e. CC
1037	1036	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X mod T ) e. CC )
1038	1034 1035 1037	nnncan2d	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( ( X + _pi ) - ( X mod T ) ) - ( X - ( X mod T ) ) ) = ( ( X + _pi ) - X ) )
1039	1038 861	eqtr2di	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> _pi = ( ( ( X + _pi ) - ( X mod T ) ) - ( X - ( X mod T ) ) ) )
1040	1032 767	resubcli	|- ( ( X + _pi ) - ( X mod T ) ) e. RR
1041	1040	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X + _pi ) - ( X mod T ) ) e. RR )
1042	768	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - ( X mod T ) ) e. RR )
1043	1040	rexri	|- ( ( X + _pi ) - ( X mod T ) ) e. RR*
1044	1043	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X + _pi ) - ( X mod T ) ) e. RR* )
1045	3	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> X e. RR )
1046	1045	rexrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> X e. RR* )
1047		id	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) )
1048		ioogtlb	|- ( ( ( ( X + _pi ) - ( X mod T ) ) e. RR* /\ X e. RR* /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> ( ( X + _pi ) - ( X mod T ) ) < x )
1049	1044 1046 1047 1048	syl3anc	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X + _pi ) - ( X mod T ) ) < x )
1050	1041 1025 1042 1049	ltsub1dd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( ( X + _pi ) - ( X mod T ) ) - ( X - ( X mod T ) ) ) < ( x - ( X - ( X mod T ) ) ) )
1051	1039 1050	eqbrtrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> _pi < ( x - ( X - ( X mod T ) ) ) )
1052	1025	recnd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> x e. CC )
1053		sub31	|- ( ( x e. CC /\ X e. CC /\ ( X mod T ) e. CC ) -> ( x - ( X - ( X mod T ) ) ) = ( ( X mod T ) - ( X - x ) ) )
1054	1052 1035 1037 1053	syl3anc	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( x - ( X - ( X mod T ) ) ) = ( ( X mod T ) - ( X - x ) ) )
1055	1051 1054	breqtrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> _pi < ( ( X mod T ) - ( X - x ) ) )
1056	1055	adantl	|- ( ( _pi < ( X mod T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> _pi < ( ( X mod T ) - ( X - x ) ) )
1057	1045 1025	resubcld	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - x ) e. RR )
1058		0red	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 e. RR )
1059		iooltub	|- ( ( ( ( X + _pi ) - ( X mod T ) ) e. RR* /\ X e. RR* /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> x < X )
1060	1044 1046 1047 1059	syl3anc	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> x < X )
1061	1025 1045	posdifd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( x < X <-> 0 < ( X - x ) ) )
1062	1060 1061	mpbid	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 < ( X - x ) )
1063	1058 1057 1062	ltled	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 <_ ( X - x ) )
1064	1045 1041	resubcld	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - ( ( X + _pi ) - ( X mod T ) ) ) e. RR )
1065	122	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> T e. RR )
1066	1041 1025 1045 1049	ltsub2dd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - x ) < ( X - ( ( X + _pi ) - ( X mod T ) ) ) )
1067		sub31	|- ( ( X e. CC /\ ( X + _pi ) e. CC /\ ( X mod T ) e. CC ) -> ( X - ( ( X + _pi ) - ( X mod T ) ) ) = ( ( X mod T ) - ( ( X + _pi ) - X ) ) )
1068	27 1033 1036 1067	mp3an	|- ( X - ( ( X + _pi ) - ( X mod T ) ) ) = ( ( X mod T ) - ( ( X + _pi ) - X ) )
1069	861	oveq2i	|- ( ( X mod T ) - ( ( X + _pi ) - X ) ) = ( ( X mod T ) - _pi )
1070	1068 1069	eqtri	|- ( X - ( ( X + _pi ) - ( X mod T ) ) ) = ( ( X mod T ) - _pi )
1071		ltsubrp	|- ( ( ( X mod T ) e. RR /\ _pi e. RR+ ) -> ( ( X mod T ) - _pi ) < ( X mod T ) )
1072	767 184 1071	mp2an	|- ( ( X mod T ) - _pi ) < ( X mod T )
1073	767 120	resubcli	|- ( ( X mod T ) - _pi ) e. RR
1074	1073 767 122	lttri	|- ( ( ( ( X mod T ) - _pi ) < ( X mod T ) /\ ( X mod T ) < T ) -> ( ( X mod T ) - _pi ) < T )
1075	1072 962 1074	mp2an	|- ( ( X mod T ) - _pi ) < T
1076	1070 1075	eqbrtri	|- ( X - ( ( X + _pi ) - ( X mod T ) ) ) < T
1077	1076	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - ( ( X + _pi ) - ( X mod T ) ) ) < T )
1078	1057 1064 1065 1066 1077	lttrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - x ) < T )
1079		modid	|- ( ( ( ( X - x ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( X - x ) /\ ( X - x ) < T ) ) -> ( ( X - x ) mod T ) = ( X - x ) )
1080	1057 1029 1063 1078 1079	syl22anc	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X - x ) mod T ) = ( X - x ) )
1081	1080	oveq2d	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X mod T ) - ( ( X - x ) mod T ) ) = ( ( X mod T ) - ( X - x ) ) )
1082	1081	oveq1d	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( ( X mod T ) - ( ( X - x ) mod T ) ) mod T ) = ( ( ( X mod T ) - ( X - x ) ) mod T ) )
1083	767	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X mod T ) e. RR )
1084	1083 1057	resubcld	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X mod T ) - ( X - x ) ) e. RR )
1085	120	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> _pi e. RR )
1086	1054 1084	eqeltrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( x - ( X - ( X mod T ) ) ) e. RR )
1087	72	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 < _pi )
1088	1058 1085 1086 1087 1051	lttrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 < ( x - ( X - ( X mod T ) ) ) )
1089	1088 1054	breqtrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 < ( ( X mod T ) - ( X - x ) ) )
1090	1058 1084 1089	ltled	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> 0 <_ ( ( X mod T ) - ( X - x ) ) )
1091	1045 1042	resubcld	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - ( X - ( X mod T ) ) ) e. RR )
1092	1025 1045 1042 1060	ltsub1dd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( x - ( X - ( X mod T ) ) ) < ( X - ( X - ( X mod T ) ) ) )
1093		nncan	|- ( ( X e. CC /\ ( X mod T ) e. CC ) -> ( X - ( X - ( X mod T ) ) ) = ( X mod T ) )
1094	27 1036 1093	mp2an	|- ( X - ( X - ( X mod T ) ) ) = ( X mod T )
1095	1094 962	eqbrtri	|- ( X - ( X - ( X mod T ) ) ) < T
1096	1095	a1i	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - ( X - ( X mod T ) ) ) < T )
1097	1086 1091 1065 1092 1096	lttrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( x - ( X - ( X mod T ) ) ) < T )
1098	1054 1097	eqbrtrrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X mod T ) - ( X - x ) ) < T )
1099		modid	|- ( ( ( ( ( X mod T ) - ( X - x ) ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( ( X mod T ) - ( X - x ) ) /\ ( ( X mod T ) - ( X - x ) ) < T ) ) -> ( ( ( X mod T ) - ( X - x ) ) mod T ) = ( ( X mod T ) - ( X - x ) ) )
1100	1084 1029 1090 1098 1099	syl22anc	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( ( X mod T ) - ( X - x ) ) mod T ) = ( ( X mod T ) - ( X - x ) ) )
1101	1082 1100	eqtr2d	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X mod T ) - ( X - x ) ) = ( ( ( X mod T ) - ( ( X - x ) mod T ) ) mod T ) )
1102		modsubmodmod	|- ( ( X e. RR /\ ( X - x ) e. RR /\ T e. RR+ ) -> ( ( ( X mod T ) - ( ( X - x ) mod T ) ) mod T ) = ( ( X - ( X - x ) ) mod T ) )
1103	1045 1057 1029 1102	syl3anc	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( ( X mod T ) - ( ( X - x ) mod T ) ) mod T ) = ( ( X - ( X - x ) ) mod T ) )
1104	1035 1052	nncand	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( X - ( X - x ) ) = x )
1105	1104	oveq1d	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X - ( X - x ) ) mod T ) = ( x mod T ) )
1106	1101 1103 1105	3eqtrd	|- ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) -> ( ( X mod T ) - ( X - x ) ) = ( x mod T ) )
1107	1106	adantl	|- ( ( _pi < ( X mod T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> ( ( X mod T ) - ( X - x ) ) = ( x mod T ) )
1108	1056 1107	breqtrd	|- ( ( _pi < ( X mod T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> _pi < ( x mod T ) )
1109	1019 1108	sylan	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> _pi < ( x mod T ) )
1110	1028 1031 1109	ltled	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> _pi <_ ( x mod T ) )
1111	1028 1031 1110	lensymd	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> -. ( x mod T ) < _pi )
1112	1111	iffalsed	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = -u 1 )
1113	1027 1112	eqtrd	|- ( ( ( X mod T ) e. ( _pi (,) T ) /\ x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) -> ( F ` x ) = -u 1 )
1114	1113	mpteq2dva	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> ( F ` x ) ) = ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 ) )
1115	1024 1114	syl5req	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 ) = ( F |` ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) )
1116	1115	oveq1d	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 ) limCC X ) = ( ( F |` ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) limCC X ) )
1117	210	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> F : RR --> CC )
1118	1043	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( X + _pi ) - ( X mod T ) ) e. RR* )
1119	3	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> X e. RR )
1120		elioore	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( X mod T ) e. RR )
1121		ltaddsublt	|- ( ( X e. RR /\ _pi e. RR /\ ( X mod T ) e. RR ) -> ( _pi < ( X mod T ) <-> ( ( X + _pi ) - ( X mod T ) ) < X ) )
1122	1119 1016 1120 1121	syl3anc	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( _pi < ( X mod T ) <-> ( ( X + _pi ) - ( X mod T ) ) < X ) )
1123	1019 1122	mpbid	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( X + _pi ) - ( X mod T ) ) < X )
1124	365	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> -oo e. RR* )
1125		mnflt	|- ( ( ( X + _pi ) - ( X mod T ) ) e. RR -> -oo < ( ( X + _pi ) - ( X mod T ) ) )
1126		xrltle	|- ( ( -oo e. RR* /\ ( ( X + _pi ) - ( X mod T ) ) e. RR* ) -> ( -oo < ( ( X + _pi ) - ( X mod T ) ) -> -oo <_ ( ( X + _pi ) - ( X mod T ) ) ) )
1127	365 1043 1126	mp2an	|- ( -oo < ( ( X + _pi ) - ( X mod T ) ) -> -oo <_ ( ( X + _pi ) - ( X mod T ) ) )
1128	1040 1125 1127	mp2b	|- -oo <_ ( ( X + _pi ) - ( X mod T ) )
1129	1128	a1i	|- ( ( X mod T ) e. ( _pi (,) T ) -> -oo <_ ( ( X + _pi ) - ( X mod T ) ) )
1130	1117 1118 1119 1123 1009 1124 1129	limcresiooub	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( F |` ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) X ) ) limCC X ) )
1131	1116 1130	eqtr2d	|- ( ( X mod T ) e. ( _pi (,) T ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( x e. ( ( ( X + _pi ) - ( X mod T ) ) (,) X ) |-> -u 1 ) limCC X ) )
1132	1014 1021 1131	3eltr4d	|- ( ( X mod T ) e. ( _pi (,) T ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
1133	1006 1132	syl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ -. ( X mod T ) = _pi ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
1134	994 1133	pm2.61dan	|- ( ( X mod T ) e. ( _pi [,) T ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
1135	964 1134	syl	|- ( ( -. ( X mod T ) e. ( 0 (,) _pi ) /\ -. ( X mod T ) = 0 ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
1136	932 1135	pm2.61dan	|- ( -. ( X mod T ) e. ( 0 (,) _pi ) -> if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
1137	814 1136	pm2.61i	|- if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. ( ( F |` ( -oo (,) X ) ) limCC X )
1138		eqid	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) = ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 )
1139		ioossre	|- ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) C_ RR
1140	1139	a1i	|- ( T. -> ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) C_ RR )
1141	1140 208	sstrdi	|- ( T. -> ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) C_ CC )
1142	1138 1141 204 819	constlimc	|- ( T. -> 1 e. ( ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) limCC X ) )
1143	1142	mptru	|- 1 e. ( ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) limCC X )
1144	1143	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> 1 e. ( ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) limCC X ) )
1145	2	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> F = ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) ) )
1146		oveq1	|- ( x = X -> ( x mod T ) = ( X mod T ) )
1147	1146	breq1d	|- ( x = X -> ( ( x mod T ) < _pi <-> ( X mod T ) < _pi ) )
1148	1147	ifbid	|- ( x = X -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = if ( ( X mod T ) < _pi , 1 , -u 1 ) )
1149	1148	adantl	|- ( ( ( X mod T ) e. ( 0 [,) _pi ) /\ x = X ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = if ( ( X mod T ) < _pi , 1 , -u 1 ) )
1150	3	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> X e. RR )
1151	108 109	ifcli	|- if ( ( X mod T ) < _pi , 1 , -u 1 ) e. RR
1152	1151	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> if ( ( X mod T ) < _pi , 1 , -u 1 ) e. RR )
1153	1145 1149 1150 1152	fvmptd	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( F ` X ) = if ( ( X mod T ) < _pi , 1 , -u 1 ) )
1154		icoltub	|- ( ( 0 e. RR* /\ _pi e. RR* /\ ( X mod T ) e. ( 0 [,) _pi ) ) -> ( X mod T ) < _pi )
1155	153 155 1154	mp3an12	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( X mod T ) < _pi )
1156	1155	iftrued	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> if ( ( X mod T ) < _pi , 1 , -u 1 ) = 1 )
1157	1153 1156	eqtrd	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( F ` X ) = 1 )
1158	363 1140	feqresmpt	|- ( T. -> ( F |` ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) = ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> ( F ` x ) ) )
1159	1158	mptru	|- ( F |` ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) = ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> ( F ` x ) )
1160		elioore	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> x e. RR )
1161	1160 110 147	sylancl	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
1162	1161	adantl	|- ( ( ( X mod T ) e. ( 0 [,) _pi ) /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
1163	3	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> X e. RR )
1164	1160 1163	resubcld	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( x - X ) e. RR )
1165	135	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> T e. RR+ )
1166		0red	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> 0 e. RR )
1167	1163	rexrd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> X e. RR* )
1168	120 767	resubcli	|- ( _pi - ( X mod T ) ) e. RR
1169	3 1168	readdcli	|- ( X + ( _pi - ( X mod T ) ) ) e. RR
1170	1169	rexri	|- ( X + ( _pi - ( X mod T ) ) ) e. RR*
1171	1170	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X + ( _pi - ( X mod T ) ) ) e. RR* )
1172		id	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) )
1173		ioogtlb	|- ( ( X e. RR* /\ ( X + ( _pi - ( X mod T ) ) ) e. RR* /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> X < x )
1174	1167 1171 1172 1173	syl3anc	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> X < x )
1175	1163 1160	posdifd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X < x <-> 0 < ( x - X ) ) )
1176	1174 1175	mpbid	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> 0 < ( x - X ) )
1177	1166 1164 1176	ltled	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> 0 <_ ( x - X ) )
1178	120	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> _pi e. RR )
1179	122	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> T e. RR )
1180	1169	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X + ( _pi - ( X mod T ) ) ) e. RR )
1181	1180 1163	resubcld	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X + ( _pi - ( X mod T ) ) ) - X ) e. RR )
1182		iooltub	|- ( ( X e. RR* /\ ( X + ( _pi - ( X mod T ) ) ) e. RR* /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> x < ( X + ( _pi - ( X mod T ) ) ) )
1183	1167 1171 1172 1182	syl3anc	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> x < ( X + ( _pi - ( X mod T ) ) ) )
1184	1160 1180 1163 1183	ltsub1dd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( x - X ) < ( ( X + ( _pi - ( X mod T ) ) ) - X ) )
1185	1168	recni	|- ( _pi - ( X mod T ) ) e. CC
1186		pncan2	|- ( ( X e. CC /\ ( _pi - ( X mod T ) ) e. CC ) -> ( ( X + ( _pi - ( X mod T ) ) ) - X ) = ( _pi - ( X mod T ) ) )
1187	27 1185 1186	mp2an	|- ( ( X + ( _pi - ( X mod T ) ) ) - X ) = ( _pi - ( X mod T ) )
1188		subge02	|- ( ( _pi e. RR /\ ( X mod T ) e. RR ) -> ( 0 <_ ( X mod T ) <-> ( _pi - ( X mod T ) ) <_ _pi ) )
1189	120 767 1188	mp2an	|- ( 0 <_ ( X mod T ) <-> ( _pi - ( X mod T ) ) <_ _pi )
1190	950 1189	mpbi	|- ( _pi - ( X mod T ) ) <_ _pi
1191	1187 1190	eqbrtri	|- ( ( X + ( _pi - ( X mod T ) ) ) - X ) <_ _pi
1192	1191	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X + ( _pi - ( X mod T ) ) ) - X ) <_ _pi )
1193	1164 1181 1178 1184 1192	ltletrd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( x - X ) < _pi )
1194	187	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> _pi < T )
1195	1164 1178 1179 1193 1194	lttrd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( x - X ) < T )
1196		modid	|- ( ( ( ( x - X ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( x - X ) /\ ( x - X ) < T ) ) -> ( ( x - X ) mod T ) = ( x - X ) )
1197	1164 1165 1177 1195 1196	syl22anc	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( x - X ) mod T ) = ( x - X ) )
1198	1197	oveq2d	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( ( x - X ) mod T ) ) = ( ( X mod T ) + ( x - X ) ) )
1199	1198	oveq1d	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) = ( ( ( X mod T ) + ( x - X ) ) mod T ) )
1200	767	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X mod T ) e. RR )
1201	1200 1164	readdcld	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) e. RR )
1202	1163 1163	resubcld	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X - X ) e. RR )
1203	1200 1202	readdcld	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( X - X ) ) e. RR )
1204	27	subidi	|- ( X - X ) = 0
1205	1204	oveq2i	|- ( ( X mod T ) + ( X - X ) ) = ( ( X mod T ) + 0 )
1206	1036	addid1i	|- ( ( X mod T ) + 0 ) = ( X mod T )
1207	1205 1206	eqtr2i	|- ( X mod T ) = ( ( X mod T ) + ( X - X ) )
1208	950 1207	breqtri	|- 0 <_ ( ( X mod T ) + ( X - X ) )
1209	1208	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> 0 <_ ( ( X mod T ) + ( X - X ) ) )
1210	1163 1160 1163 1174	ltsub1dd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X - X ) < ( x - X ) )
1211	1202 1164 1200 1210	ltadd2dd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( X - X ) ) < ( ( X mod T ) + ( x - X ) ) )
1212	1166 1203 1201 1209 1211	lelttrd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> 0 < ( ( X mod T ) + ( x - X ) ) )
1213	1166 1201 1212	ltled	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> 0 <_ ( ( X mod T ) + ( x - X ) ) )
1214	1164 1181 1200 1184	ltadd2dd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) < ( ( X mod T ) + ( ( X + ( _pi - ( X mod T ) ) ) - X ) ) )
1215	1187	oveq2i	|- ( ( X mod T ) + ( ( X + ( _pi - ( X mod T ) ) ) - X ) ) = ( ( X mod T ) + ( _pi - ( X mod T ) ) )
1216	1036 56	pncan3i	|- ( ( X mod T ) + ( _pi - ( X mod T ) ) ) = _pi
1217	1215 1216	eqtri	|- ( ( X mod T ) + ( ( X + ( _pi - ( X mod T ) ) ) - X ) ) = _pi
1218	1214 1217	breqtrdi	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) < _pi )
1219	1201 1178 1179 1218 1194	lttrd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) < T )
1220		modid	|- ( ( ( ( ( X mod T ) + ( x - X ) ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( ( X mod T ) + ( x - X ) ) /\ ( ( X mod T ) + ( x - X ) ) < T ) ) -> ( ( ( X mod T ) + ( x - X ) ) mod T ) = ( ( X mod T ) + ( x - X ) ) )
1221	1201 1165 1213 1219 1220	syl22anc	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( ( X mod T ) + ( x - X ) ) mod T ) = ( ( X mod T ) + ( x - X ) ) )
1222	1199 1221	eqtr2d	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) = ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) )
1223		modaddabs	|- ( ( X e. RR /\ ( x - X ) e. RR /\ T e. RR+ ) -> ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) = ( ( X + ( x - X ) ) mod T ) )
1224	1163 1164 1165 1223	syl3anc	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) = ( ( X + ( x - X ) ) mod T ) )
1225	27	a1i	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> X e. CC )
1226	1160	recnd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> x e. CC )
1227	1225 1226	pncan3d	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( X + ( x - X ) ) = x )
1228	1227	oveq1d	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( ( X + ( x - X ) ) mod T ) = ( x mod T ) )
1229	1222 1224 1228	3eqtrrd	|- ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) -> ( x mod T ) = ( ( X mod T ) + ( x - X ) ) )
1230	1229	adantl	|- ( ( ( X mod T ) < _pi /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> ( x mod T ) = ( ( X mod T ) + ( x - X ) ) )
1231	1218	adantl	|- ( ( ( X mod T ) < _pi /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) < _pi )
1232	1230 1231	eqbrtrd	|- ( ( ( X mod T ) < _pi /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> ( x mod T ) < _pi )
1233	1155 1232	sylan	|- ( ( ( X mod T ) e. ( 0 [,) _pi ) /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> ( x mod T ) < _pi )
1234	1233	iftrued	|- ( ( ( X mod T ) e. ( 0 [,) _pi ) /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
1235	1162 1234	eqtrd	|- ( ( ( X mod T ) e. ( 0 [,) _pi ) /\ x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) -> ( F ` x ) = 1 )
1236	1235	mpteq2dva	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> ( F ` x ) ) = ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) )
1237	1159 1236	syl5req	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) = ( F |` ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) )
1238	1237	oveq1d	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) limCC X ) = ( ( F |` ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) limCC X ) )
1239	210	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> F : RR --> CC )
1240	1170	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( X + ( _pi - ( X mod T ) ) ) e. RR* )
1241	1168	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( _pi - ( X mod T ) ) e. RR )
1242	767	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( X mod T ) e. RR )
1243	120	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> _pi e. RR )
1244	1242 1243	posdifd	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( ( X mod T ) < _pi <-> 0 < ( _pi - ( X mod T ) ) ) )
1245	1155 1244	mpbid	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> 0 < ( _pi - ( X mod T ) ) )
1246	1241 1245	elrpd	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( _pi - ( X mod T ) ) e. RR+ )
1247	1150 1246	ltaddrpd	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> X < ( X + ( _pi - ( X mod T ) ) ) )
1248	1139	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) C_ RR )
1249	376	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> +oo e. RR* )
1250		ltpnf	|- ( ( X + ( _pi - ( X mod T ) ) ) e. RR -> ( X + ( _pi - ( X mod T ) ) ) < +oo )
1251		xrltle	|- ( ( ( X + ( _pi - ( X mod T ) ) ) e. RR* /\ +oo e. RR* ) -> ( ( X + ( _pi - ( X mod T ) ) ) < +oo -> ( X + ( _pi - ( X mod T ) ) ) <_ +oo ) )
1252	1170 376 1251	mp2an	|- ( ( X + ( _pi - ( X mod T ) ) ) < +oo -> ( X + ( _pi - ( X mod T ) ) ) <_ +oo )
1253	1169 1250 1252	mp2b	|- ( X + ( _pi - ( X mod T ) ) ) <_ +oo
1254	1253	a1i	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( X + ( _pi - ( X mod T ) ) ) <_ +oo )
1255	1239 1150 1240 1247 1248 1249 1254	limcresioolb	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( ( F |` ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) ) limCC X ) = ( ( F |` ( X (,) +oo ) ) limCC X ) )
1256	1238 1255	eqtr2d	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) = ( ( x e. ( X (,) ( X + ( _pi - ( X mod T ) ) ) ) |-> 1 ) limCC X ) )
1257	1144 1157 1256	3eltr4d	|- ( ( X mod T ) e. ( 0 [,) _pi ) -> ( F ` X ) e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
1258	155	a1i	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> _pi e. RR* )
1259	934	a1i	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> T e. RR* )
1260	936	a1i	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> ( X mod T ) e. RR* )
1261	153	a1i	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> 0 e. RR* )
1262	155	a1i	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> _pi e. RR* )
1263	936	a1i	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> ( X mod T ) e. RR* )
1264	950	a1i	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> 0 <_ ( X mod T ) )
1265	767	a1i	|- ( -. _pi <_ ( X mod T ) -> ( X mod T ) e. RR )
1266	120	a1i	|- ( -. _pi <_ ( X mod T ) -> _pi e. RR )
1267	1265 1266	ltnled	|- ( -. _pi <_ ( X mod T ) -> ( ( X mod T ) < _pi <-> -. _pi <_ ( X mod T ) ) )
1268	1267	ibir	|- ( -. _pi <_ ( X mod T ) -> ( X mod T ) < _pi )
1269	1268	adantl	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> ( X mod T ) < _pi )
1270	1261 1262 1263 1264 1269	elicod	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> ( X mod T ) e. ( 0 [,) _pi ) )
1271		simpl	|- ( ( -. ( X mod T ) e. ( 0 [,) _pi ) /\ -. _pi <_ ( X mod T ) ) -> -. ( X mod T ) e. ( 0 [,) _pi ) )
1272	1270 1271	condan	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> _pi <_ ( X mod T ) )
1273	962	a1i	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> ( X mod T ) < T )
1274	1258 1259 1260 1272 1273	elicod	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> ( X mod T ) e. ( _pi [,) T ) )
1275		eqid	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) = ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 )
1276		ioossre	|- ( X (,) ( X + ( T - ( X mod T ) ) ) ) C_ RR
1277	1276	a1i	|- ( T. -> ( X (,) ( X + ( T - ( X mod T ) ) ) ) C_ RR )
1278	1277 208	sstrdi	|- ( T. -> ( X (,) ( X + ( T - ( X mod T ) ) ) ) C_ CC )
1279	1275 1278 306 819	constlimc	|- ( T. -> -u 1 e. ( ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) limCC X ) )
1280	1279	mptru	|- -u 1 e. ( ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) limCC X )
1281	1280	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> -u 1 e. ( ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) limCC X ) )
1282		1ex	|- 1 e. _V
1283	109	elexi	|- -u 1 e. _V
1284	1282 1283	ifex	|- if ( ( X mod T ) < _pi , 1 , -u 1 ) e. _V
1285	1148 2 1284	fvmpt	|- ( X e. RR -> ( F ` X ) = if ( ( X mod T ) < _pi , 1 , -u 1 ) )
1286	3 1285	ax-mp	|- ( F ` X ) = if ( ( X mod T ) < _pi , 1 , -u 1 )
1287	1286	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( F ` X ) = if ( ( X mod T ) < _pi , 1 , -u 1 ) )
1288	120	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> _pi e. RR )
1289	767	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( X mod T ) e. RR )
1290	1288 1289 1000	lensymd	|- ( ( X mod T ) e. ( _pi [,) T ) -> -. ( X mod T ) < _pi )
1291	1290	iffalsed	|- ( ( X mod T ) e. ( _pi [,) T ) -> if ( ( X mod T ) < _pi , 1 , -u 1 ) = -u 1 )
1292	1287 1291	eqtrd	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( F ` X ) = -u 1 )
1293	363 1277	feqresmpt	|- ( T. -> ( F |` ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) = ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> ( F ` x ) ) )
1294	1293	mptru	|- ( F |` ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) = ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> ( F ` x ) )
1295		elioore	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> x e. RR )
1296	1295 110 147	sylancl	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
1297	1296	adantl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
1298	120	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> _pi e. RR )
1299	3	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> X e. RR )
1300	1295 1299	resubcld	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( x - X ) e. RR )
1301	135	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> T e. RR+ )
1302		0red	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> 0 e. RR )
1303	1299	rexrd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> X e. RR* )
1304	122 767	resubcli	|- ( T - ( X mod T ) ) e. RR
1305	3 1304	readdcli	|- ( X + ( T - ( X mod T ) ) ) e. RR
1306	1305	rexri	|- ( X + ( T - ( X mod T ) ) ) e. RR*
1307	1306	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( X + ( T - ( X mod T ) ) ) e. RR* )
1308		id	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) )
1309		ioogtlb	|- ( ( X e. RR* /\ ( X + ( T - ( X mod T ) ) ) e. RR* /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> X < x )
1310	1303 1307 1308 1309	syl3anc	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> X < x )
1311	1299 1295	posdifd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( X < x <-> 0 < ( x - X ) ) )
1312	1310 1311	mpbid	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> 0 < ( x - X ) )
1313	1302 1300 1312	ltled	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> 0 <_ ( x - X ) )
1314	1305	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( X + ( T - ( X mod T ) ) ) e. RR )
1315	1314 1299	resubcld	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X + ( T - ( X mod T ) ) ) - X ) e. RR )
1316	122	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> T e. RR )
1317		iooltub	|- ( ( X e. RR* /\ ( X + ( T - ( X mod T ) ) ) e. RR* /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> x < ( X + ( T - ( X mod T ) ) ) )
1318	1303 1307 1308 1317	syl3anc	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> x < ( X + ( T - ( X mod T ) ) ) )
1319	1295 1314 1299 1318	ltsub1dd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( x - X ) < ( ( X + ( T - ( X mod T ) ) ) - X ) )
1320	1304	recni	|- ( T - ( X mod T ) ) e. CC
1321		pncan2	|- ( ( X e. CC /\ ( T - ( X mod T ) ) e. CC ) -> ( ( X + ( T - ( X mod T ) ) ) - X ) = ( T - ( X mod T ) ) )
1322	27 1320 1321	mp2an	|- ( ( X + ( T - ( X mod T ) ) ) - X ) = ( T - ( X mod T ) )
1323		subge02	|- ( ( T e. RR /\ ( X mod T ) e. RR ) -> ( 0 <_ ( X mod T ) <-> ( T - ( X mod T ) ) <_ T ) )
1324	122 767 1323	mp2an	|- ( 0 <_ ( X mod T ) <-> ( T - ( X mod T ) ) <_ T )
1325	950 1324	mpbi	|- ( T - ( X mod T ) ) <_ T
1326	1322 1325	eqbrtri	|- ( ( X + ( T - ( X mod T ) ) ) - X ) <_ T
1327	1326	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X + ( T - ( X mod T ) ) ) - X ) <_ T )
1328	1300 1315 1316 1319 1327	ltletrd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( x - X ) < T )
1329	1300 1301 1313 1328 1196	syl22anc	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( x - X ) mod T ) = ( x - X ) )
1330	1329	oveq2d	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( ( x - X ) mod T ) ) = ( ( X mod T ) + ( x - X ) ) )
1331	1330	oveq1d	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) = ( ( ( X mod T ) + ( x - X ) ) mod T ) )
1332		readdcl	|- ( ( ( X mod T ) e. RR /\ ( x - X ) e. RR ) -> ( ( X mod T ) + ( x - X ) ) e. RR )
1333	767 1300 1332	sylancr	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) e. RR )
1334	767	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( X mod T ) e. RR )
1335	950	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> 0 <_ ( X mod T ) )
1336	1334 1300 1335 1312	addgegt0d	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> 0 < ( ( X mod T ) + ( x - X ) ) )
1337	1302 1333 1336	ltled	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> 0 <_ ( ( X mod T ) + ( x - X ) ) )
1338	1300 1315 1334 1319	ltadd2dd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) < ( ( X mod T ) + ( ( X + ( T - ( X mod T ) ) ) - X ) ) )
1339	1322	oveq2i	|- ( ( X mod T ) + ( ( X + ( T - ( X mod T ) ) ) - X ) ) = ( ( X mod T ) + ( T - ( X mod T ) ) )
1340	1036 123	pncan3i	|- ( ( X mod T ) + ( T - ( X mod T ) ) ) = T
1341	1339 1340	eqtri	|- ( ( X mod T ) + ( ( X + ( T - ( X mod T ) ) ) - X ) ) = T
1342	1338 1341	breqtrdi	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) < T )
1343	1333 1301 1337 1342 1220	syl22anc	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( ( X mod T ) + ( x - X ) ) mod T ) = ( ( X mod T ) + ( x - X ) ) )
1344	1331 1343	eqtr2d	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) = ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) )
1345	1299 1300 1301 1223	syl3anc	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( ( X mod T ) + ( ( x - X ) mod T ) ) mod T ) = ( ( X + ( x - X ) ) mod T ) )
1346	27	a1i	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> X e. CC )
1347	1295	recnd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> x e. CC )
1348	1346 1347	pncan3d	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( X + ( x - X ) ) = x )
1349	1348	oveq1d	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X + ( x - X ) ) mod T ) = ( x mod T ) )
1350	1344 1345 1349	3eqtrd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) = ( x mod T ) )
1351	1350	adantl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) = ( x mod T ) )
1352	1333	adantl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( ( X mod T ) + ( x - X ) ) e. RR )
1353	1351 1352	eqeltrrd	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( x mod T ) e. RR )
1354	767	a1i	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( X mod T ) e. RR )
1355	1000	adantr	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> _pi <_ ( X mod T ) )
1356	1300 1312	elrpd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( x - X ) e. RR+ )
1357	1334 1356	ltaddrpd	|- ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) -> ( X mod T ) < ( ( X mod T ) + ( x - X ) ) )
1358	1357	adantl	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( X mod T ) < ( ( X mod T ) + ( x - X ) ) )
1359	1298 1354 1352 1355 1358	lelttrd	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> _pi < ( ( X mod T ) + ( x - X ) ) )
1360	1298 1352 1359	ltled	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> _pi <_ ( ( X mod T ) + ( x - X ) ) )
1361	1360 1351	breqtrd	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> _pi <_ ( x mod T ) )
1362	1298 1353 1361	lensymd	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> -. ( x mod T ) < _pi )
1363	1362	iffalsed	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = -u 1 )
1364	1297 1363	eqtrd	|- ( ( ( X mod T ) e. ( _pi [,) T ) /\ x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) -> ( F ` x ) = -u 1 )
1365	1364	mpteq2dva	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> ( F ` x ) ) = ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) )
1366	1294 1365	syl5req	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) = ( F |` ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) )
1367	1366	oveq1d	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) limCC X ) = ( ( F |` ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) limCC X ) )
1368	210	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> F : RR --> CC )
1369	3	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> X e. RR )
1370	1306	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( X + ( T - ( X mod T ) ) ) e. RR* )
1371	1304	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( T - ( X mod T ) ) e. RR )
1372	962	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( X mod T ) < T )
1373	122	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> T e. RR )
1374	1289 1373	posdifd	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( ( X mod T ) < T <-> 0 < ( T - ( X mod T ) ) ) )
1375	1372 1374	mpbid	|- ( ( X mod T ) e. ( _pi [,) T ) -> 0 < ( T - ( X mod T ) ) )
1376	1371 1375	elrpd	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( T - ( X mod T ) ) e. RR+ )
1377	1369 1376	ltaddrpd	|- ( ( X mod T ) e. ( _pi [,) T ) -> X < ( X + ( T - ( X mod T ) ) ) )
1378	1276	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( X (,) ( X + ( T - ( X mod T ) ) ) ) C_ RR )
1379	376	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> +oo e. RR* )
1380		ltpnf	|- ( ( X + ( T - ( X mod T ) ) ) e. RR -> ( X + ( T - ( X mod T ) ) ) < +oo )
1381		xrltle	|- ( ( ( X + ( T - ( X mod T ) ) ) e. RR* /\ +oo e. RR* ) -> ( ( X + ( T - ( X mod T ) ) ) < +oo -> ( X + ( T - ( X mod T ) ) ) <_ +oo ) )
1382	1306 376 1381	mp2an	|- ( ( X + ( T - ( X mod T ) ) ) < +oo -> ( X + ( T - ( X mod T ) ) ) <_ +oo )
1383	1305 1380 1382	mp2b	|- ( X + ( T - ( X mod T ) ) ) <_ +oo
1384	1383	a1i	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( X + ( T - ( X mod T ) ) ) <_ +oo )
1385	1368 1369 1370 1377 1378 1379 1384	limcresioolb	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( ( F |` ( X (,) ( X + ( T - ( X mod T ) ) ) ) ) limCC X ) = ( ( F |` ( X (,) +oo ) ) limCC X ) )
1386	1367 1385	eqtr2d	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) = ( ( x e. ( X (,) ( X + ( T - ( X mod T ) ) ) ) |-> -u 1 ) limCC X ) )
1387	1281 1292 1386	3eltr4d	|- ( ( X mod T ) e. ( _pi [,) T ) -> ( F ` X ) e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
1388	1274 1387	syl	|- ( -. ( X mod T ) e. ( 0 [,) _pi ) -> ( F ` X ) e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
1389	1257 1388	pm2.61i	|- ( F ` X ) e. ( ( F |` ( X (,) +oo ) ) limCC X )
1390		id	|- ( n e. NN0 -> n e. NN0 )
1391	1 2 1390	sqwvfoura	|- ( n e. NN0 -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) = 0 )
1392	1391	eqcomd	|- ( n e. NN0 -> 0 = ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
1393	1392	mpteq2ia	|- ( n e. NN0 |-> 0 ) = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
1394		id	|- ( n e. NN -> n e. NN )
1395	1 2 1394	sqwvfourb	|- ( n e. NN -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) = if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) )
1396	1395	eqcomd	|- ( n e. NN -> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) = ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
1397	1396	mpteq2ia	|- ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
1398		nnnn0	|- ( n e. NN -> n e. NN0 )
1399		0red	|- ( n e. NN -> 0 e. RR )
1400		eqid	|- ( n e. NN0 |-> 0 ) = ( n e. NN0 |-> 0 )
1401	1400	fvmpt2	|- ( ( n e. NN0 /\ 0 e. RR ) -> ( ( n e. NN0 |-> 0 ) ` n ) = 0 )
1402	1398 1399 1401	syl2anc	|- ( n e. NN -> ( ( n e. NN0 |-> 0 ) ` n ) = 0 )
1403	1402	oveq1d	|- ( n e. NN -> ( ( ( n e. NN0 |-> 0 ) ` n ) x. ( cos ` ( n x. X ) ) ) = ( 0 x. ( cos ` ( n x. X ) ) ) )
1404	78	coscld	|- ( n e. NN -> ( cos ` ( n x. X ) ) e. CC )
1405	1404	mul02d	|- ( n e. NN -> ( 0 x. ( cos ` ( n x. X ) ) ) = 0 )
1406	1403 1405	eqtrd	|- ( n e. NN -> ( ( ( n e. NN0 |-> 0 ) ` n ) x. ( cos ` ( n x. X ) ) ) = 0 )
1407		ovex	|- ( 4 / ( n x. _pi ) ) e. _V
1408	93 1407	ifex	|- if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) e. _V
1409		eqid	|- ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) = ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) )
1410	1409	fvmpt2	|- ( ( n e. NN /\ if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) e. _V ) -> ( ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) ` n ) = if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) )
1411	1408 1410	mpan2	|- ( n e. NN -> ( ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) ` n ) = if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) )
1412	1411	oveq1d	|- ( n e. NN -> ( ( ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) ` n ) x. ( sin ` ( n x. X ) ) ) = ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) )
1413	1406 1412	oveq12d	|- ( n e. NN -> ( ( ( ( n e. NN0 |-> 0 ) ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( 0 + ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) ) )
1414	64 76	ifcld	|- ( n e. NN -> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) e. CC )
1415	1414 79	mulcld	|- ( n e. NN -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) e. CC )
1416	1415	addid2d	|- ( n e. NN -> ( 0 + ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) ) = ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) )
1417		iftrue	|- ( 2 || n -> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) = 0 )
1418	1417	oveq1d	|- ( 2 || n -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = ( 0 x. ( sin ` ( n x. X ) ) ) )
1419	79	mul02d	|- ( n e. NN -> ( 0 x. ( sin ` ( n x. X ) ) ) = 0 )
1420	1418 1419	sylan9eqr	|- ( ( n e. NN /\ 2 || n ) -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = 0 )
1421		iftrue	|- ( 2 || n -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = 0 )
1422	1421	eqcomd	|- ( 2 || n -> 0 = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1423	1422	adantl	|- ( ( n e. NN /\ 2 || n ) -> 0 = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1424	1420 1423	eqtrd	|- ( ( n e. NN /\ 2 || n ) -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1425		iffalse	|- ( -. 2 || n -> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) = ( 4 / ( n x. _pi ) ) )
1426	1425	oveq1d	|- ( -. 2 || n -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) )
1427	1426	adantl	|- ( ( n e. NN /\ -. 2 || n ) -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) )
1428		iffalse	|- ( -. 2 || n -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) )
1429	1428	eqcomd	|- ( -. 2 || n -> ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1430	1429	adantl	|- ( ( n e. NN /\ -. 2 || n ) -> ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1431	1427 1430	eqtrd	|- ( ( n e. NN /\ -. 2 || n ) -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1432	1424 1431	pm2.61dan	|- ( n e. NN -> ( if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) x. ( sin ` ( n x. X ) ) ) = if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) )
1433	1413 1416 1432	3eqtrrd	|- ( n e. NN -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( ( n e. NN0 |-> 0 ) ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) ` n ) x. ( sin ` ( n x. X ) ) ) ) )
1434	1433	mpteq2ia	|- ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) = ( n e. NN |-> ( ( ( ( n e. NN0 |-> 0 ) ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( ( n e. NN |-> if ( 2 || n , 0 , ( 4 / ( n x. _pi ) ) ) ) ` n ) x. ( sin ` ( n x. X ) ) ) ) )
1435	112 1 149 150 331 605 676 755 3 1137 1389 1393 1397 1434	fourierclim	|- seq 1 ( + , ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ) ~~> ( ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) - ( ( ( n e. NN0 |-> 0 ) ` 0 ) / 2 ) )
1436		0nn0	|- 0 e. NN0
1437		eqidd	|- ( n = 0 -> 0 = 0 )
1438	1437 1400 93	fvmpt	|- ( 0 e. NN0 -> ( ( n e. NN0 |-> 0 ) ` 0 ) = 0 )
1439	1436 1438	ax-mp	|- ( ( n e. NN0 |-> 0 ) ` 0 ) = 0
1440	1439	oveq1i	|- ( ( ( n e. NN0 |-> 0 ) ` 0 ) / 2 ) = ( 0 / 2 )
1441	32	recni	|- 2 e. CC
1442	71 131	gtneii	|- 2 =/= 0
1443	1441 1442	div0i	|- ( 0 / 2 ) = 0
1444	1440 1443	eqtri	|- ( ( ( n e. NN0 |-> 0 ) ` 0 ) / 2 ) = 0
1445	1444	oveq2i	|- ( ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) - ( ( ( n e. NN0 |-> 0 ) ` 0 ) / 2 ) ) = ( ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) - 0 )
1446	204	mptru	|- 1 e. CC
1447	1446 1011	ifcli	|- if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) e. CC
1448	1151	recni	|- if ( ( X mod T ) < _pi , 1 , -u 1 ) e. CC
1449	1286 1448	eqeltri	|- ( F ` X ) e. CC
1450	1447 1449	addcli	|- ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) e. CC
1451	1450 1441 1442	divcli	|- ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) e. CC
1452	1451	subid1i	|- ( ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) - 0 ) = ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 )
1453	1445 1452	eqtri	|- ( ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) - ( ( ( n e. NN0 |-> 0 ) ` 0 ) / 2 ) ) = ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 )
1454	1435 1453	breqtri	|- seq 1 ( + , ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ) ~~> ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 )
1455	1454	a1i	|- ( T. -> seq 1 ( + , ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ) ~~> ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) )
1456	83 107 1455	sumnnodd	|- ( T. -> ( seq 1 ( + , ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) /\ sum_ k e. NN ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` k ) = sum_ k e. NN ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) )
1457	1456	mptru	|- ( seq 1 ( + , ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) /\ sum_ k e. NN ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` k ) = sum_ k e. NN ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) )
1458	1457	simpli	|- seq 1 ( + , ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 )
1459		breq2	|- ( n = ( ( 2 x. k ) - 1 ) -> ( 2 || n <-> 2 || ( ( 2 x. k ) - 1 ) ) )
1460		oveq1	|- ( n = ( ( 2 x. k ) - 1 ) -> ( n x. _pi ) = ( ( ( 2 x. k ) - 1 ) x. _pi ) )
1461	1460	oveq2d	|- ( n = ( ( 2 x. k ) - 1 ) -> ( 4 / ( n x. _pi ) ) = ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) )
1462		oveq1	|- ( n = ( ( 2 x. k ) - 1 ) -> ( n x. X ) = ( ( ( 2 x. k ) - 1 ) x. X ) )
1463	1462	fveq2d	|- ( n = ( ( 2 x. k ) - 1 ) -> ( sin ` ( n x. X ) ) = ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) )
1464	1461 1463	oveq12d	|- ( n = ( ( 2 x. k ) - 1 ) -> ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) = ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) )
1465	1459 1464	ifbieq2d	|- ( n = ( ( 2 x. k ) - 1 ) -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = if ( 2 || ( ( 2 x. k ) - 1 ) , 0 , ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) ) )
1466	1465	adantl	|- ( ( k e. NN /\ n = ( ( 2 x. k ) - 1 ) ) -> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) = if ( 2 || ( ( 2 x. k ) - 1 ) , 0 , ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) ) )
1467		elnnz	|- ( ( ( 2 x. k ) - 1 ) e. NN <-> ( ( ( 2 x. k ) - 1 ) e. ZZ /\ 0 < ( ( 2 x. k ) - 1 ) ) )
1468	25 52 1467	sylanbrc	|- ( k e. NN -> ( ( 2 x. k ) - 1 ) e. NN )
1469		ovex	|- ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) e. _V
1470	93 1469	ifex	|- if ( 2 || ( ( 2 x. k ) - 1 ) , 0 , ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) ) e. _V
1471	1470	a1i	|- ( k e. NN -> if ( 2 || ( ( 2 x. k ) - 1 ) , 0 , ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) ) e. _V )
1472	84 1466 1468 1471	fvmptd	|- ( k e. NN -> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) = if ( 2 || ( ( 2 x. k ) - 1 ) , 0 , ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) ) )
1473		dvdsmul1	|- ( ( 2 e. ZZ /\ k e. ZZ ) -> 2 || ( 2 x. k ) )
1474	20 22 1473	sylancr	|- ( k e. NN -> 2 || ( 2 x. k ) )
1475	23	zcnd	|- ( k e. NN -> ( 2 x. k ) e. CC )
1476		1cnd	|- ( k e. NN -> 1 e. CC )
1477	1475 1476	npcand	|- ( k e. NN -> ( ( ( 2 x. k ) - 1 ) + 1 ) = ( 2 x. k ) )
1478	1477	eqcomd	|- ( k e. NN -> ( 2 x. k ) = ( ( ( 2 x. k ) - 1 ) + 1 ) )
1479	1474 1478	breqtrd	|- ( k e. NN -> 2 || ( ( ( 2 x. k ) - 1 ) + 1 ) )
1480		oddp1even	|- ( ( ( 2 x. k ) - 1 ) e. ZZ -> ( -. 2 || ( ( 2 x. k ) - 1 ) <-> 2 || ( ( ( 2 x. k ) - 1 ) + 1 ) ) )
1481	25 1480	syl	|- ( k e. NN -> ( -. 2 || ( ( 2 x. k ) - 1 ) <-> 2 || ( ( ( 2 x. k ) - 1 ) + 1 ) ) )
1482	1479 1481	mpbird	|- ( k e. NN -> -. 2 || ( ( 2 x. k ) - 1 ) )
1483	1482	iffalsed	|- ( k e. NN -> if ( 2 || ( ( 2 x. k ) - 1 ) , 0 , ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) ) = ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) )
1484	56	a1i	|- ( k e. NN -> _pi e. CC )
1485	26 1484	mulcomd	|- ( k e. NN -> ( ( ( 2 x. k ) - 1 ) x. _pi ) = ( _pi x. ( ( 2 x. k ) - 1 ) ) )
1486	1485	oveq2d	|- ( k e. NN -> ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) = ( 4 / ( _pi x. ( ( 2 x. k ) - 1 ) ) ) )
1487	58	a1i	|- ( k e. NN -> 4 e. CC )
1488	73	a1i	|- ( k e. NN -> _pi =/= 0 )
1489	1487 1484 26 1488 53	divdiv1d	|- ( k e. NN -> ( ( 4 / _pi ) / ( ( 2 x. k ) - 1 ) ) = ( 4 / ( _pi x. ( ( 2 x. k ) - 1 ) ) ) )
1490	1486 1489	eqtr4d	|- ( k e. NN -> ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) = ( ( 4 / _pi ) / ( ( 2 x. k ) - 1 ) ) )
1491	1490	oveq1d	|- ( k e. NN -> ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) = ( ( ( 4 / _pi ) / ( ( 2 x. k ) - 1 ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) )
1492	1487 1484 1488	divcld	|- ( k e. NN -> ( 4 / _pi ) e. CC )
1493	1492 26 30 53	div32d	|- ( k e. NN -> ( ( ( 4 / _pi ) / ( ( 2 x. k ) - 1 ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1494	1491 1493	eqtrd	|- ( k e. NN -> ( ( 4 / ( ( ( 2 x. k ) - 1 ) x. _pi ) ) x. ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1495	1472 1483 1494	3eqtrd	|- ( k e. NN -> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1496	1495	mpteq2ia	|- ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) = ( k e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1497		oveq2	|- ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
1498	1497	oveq1d	|- ( k = n -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. n ) - 1 ) )
1499	1498	oveq1d	|- ( k = n -> ( ( ( 2 x. k ) - 1 ) x. X ) = ( ( ( 2 x. n ) - 1 ) x. X ) )
1500	1499	fveq2d	|- ( k = n -> ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) = ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) )
1501	1500 1498	oveq12d	|- ( k = n -> ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) = ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) )
1502	1501	oveq2d	|- ( k = n -> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) )
1503	1502	cbvmptv	|- ( k e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) ) = ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) )
1504	1496 1503	eqtri	|- ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) = ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) )
1505		seqeq3	|- ( ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) = ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) -> seq 1 ( + , ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) ) = seq 1 ( + , ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ) )
1506	1504 1505	ax-mp	|- seq 1 ( + , ( k e. NN |-> ( ( n e. NN |-> if ( 2 || n , 0 , ( ( 4 / ( n x. _pi ) ) x. ( sin ` ( n x. X ) ) ) ) ) ` ( ( 2 x. k ) - 1 ) ) ) ) = seq 1 ( + , ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) )
1507	1 2 3 5	fourierswlem	|- Y = ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 )
1508	1507	eqcomi	|- ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 ) = Y
1509	1458 1506 1508	3brtr3i	|- seq 1 ( + , ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ) ~~> Y
1510	1509	a1i	|- ( T. -> seq 1 ( + , ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ) ~~> Y )
1511		eqid	|- ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) = ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) )
1512	65 69 74	divcld	|- ( n e. NN -> ( 4 / _pi ) e. CC )
1513	1441	a1i	|- ( n e. NN -> 2 e. CC )
1514	1513 66	mulcld	|- ( n e. NN -> ( 2 x. n ) e. CC )
1515		id	|- ( ( 2 x. n ) e. CC -> ( 2 x. n ) e. CC )
1516		1cnd	|- ( ( 2 x. n ) e. CC -> 1 e. CC )
1517	1515 1516	subcld	|- ( ( 2 x. n ) e. CC -> ( ( 2 x. n ) - 1 ) e. CC )
1518	1514 1517	syl	|- ( n e. NN -> ( ( 2 x. n ) - 1 ) e. CC )
1519	1518 77	mulcld	|- ( n e. NN -> ( ( ( 2 x. n ) - 1 ) x. X ) e. CC )
1520	1519	sincld	|- ( n e. NN -> ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) e. CC )
1521	32	a1i	|- ( n e. NN -> 2 e. RR )
1522		nnre	|- ( n e. NN -> n e. RR )
1523	1521 1522	remulcld	|- ( n e. NN -> ( 2 x. n ) e. RR )
1524	1523	recnd	|- ( n e. NN -> ( 2 x. n ) e. CC )
1525		1cnd	|- ( n e. NN -> 1 e. CC )
1526	1524 1525	subcld	|- ( n e. NN -> ( ( 2 x. n ) - 1 ) e. CC )
1527		1red	|- ( n e. NN -> 1 e. RR )
1528	39 1521	eqeltrid	|- ( n e. NN -> ( 2 x. 1 ) e. RR )
1529		1lt2	|- 1 < 2
1530	1529	a1i	|- ( n e. NN -> 1 < 2 )
1531	1530 39	breqtrrdi	|- ( n e. NN -> 1 < ( 2 x. 1 ) )
1532	47	a1i	|- ( n e. NN -> 0 <_ 2 )
1533		nnge1	|- ( n e. NN -> 1 <_ n )
1534	1527 1522 1521 1532 1533	lemul2ad	|- ( n e. NN -> ( 2 x. 1 ) <_ ( 2 x. n ) )
1535	1527 1528 1523 1531 1534	ltletrd	|- ( n e. NN -> 1 < ( 2 x. n ) )
1536	1527 1535	gtned	|- ( n e. NN -> ( 2 x. n ) =/= 1 )
1537	1524 1525 1536	subne0d	|- ( n e. NN -> ( ( 2 x. n ) - 1 ) =/= 0 )
1538	1520 1526 1537	divcld	|- ( n e. NN -> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) e. CC )
1539	1512 1538	mulcld	|- ( n e. NN -> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) e. CC )
1540	1511 1539	fmpti	|- ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) : NN --> CC
1541	1540	a1i	|- ( T. -> ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) : NN --> CC )
1542	1541	ffvelrnda	|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ` k ) e. CC )
1543		divcan6	|- ( ( ( _pi e. CC /\ _pi =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( _pi / 4 ) x. ( 4 / _pi ) ) = 1 )
1544	56 73 58 60 1543	mp4an	|- ( ( _pi / 4 ) x. ( 4 / _pi ) ) = 1
1545	1544	eqcomi	|- 1 = ( ( _pi / 4 ) x. ( 4 / _pi ) )
1546	1545	oveq1i	|- ( 1 x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = ( ( ( _pi / 4 ) x. ( 4 / _pi ) ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
1547	54	mulid2d	|- ( k e. NN -> ( 1 x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
1548	60	a1i	|- ( k e. NN -> 4 =/= 0 )
1549	1484 1487 1548	divcld	|- ( k e. NN -> ( _pi / 4 ) e. CC )
1550	1549 1492 54	mulassd	|- ( k e. NN -> ( ( ( _pi / 4 ) x. ( 4 / _pi ) ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = ( ( _pi / 4 ) x. ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) ) )
1551	1546 1547 1550	3eqtr3a	|- ( k e. NN -> ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) = ( ( _pi / 4 ) x. ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) ) )
1552		eqidd	|- ( k e. NN -> ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) = ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) )
1553	13	oveq2d	|- ( n = k -> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1554	1553	adantl	|- ( ( k e. NN /\ n = k ) -> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1555	1494 1469	eqeltrrdi	|- ( k e. NN -> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) e. _V )
1556	1552 1554 15 1555	fvmptd	|- ( k e. NN -> ( ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ` k ) = ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) )
1557	1556	oveq2d	|- ( k e. NN -> ( ( _pi / 4 ) x. ( ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ` k ) ) = ( ( _pi / 4 ) x. ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) ) )
1558	1557	eqcomd	|- ( k e. NN -> ( ( _pi / 4 ) x. ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) ) = ( ( _pi / 4 ) x. ( ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ` k ) ) )
1559	18 1551 1558	3eqtrd	|- ( k e. NN -> ( ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ` k ) = ( ( _pi / 4 ) x. ( ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ` k ) ) )
1560	1559	adantl	|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ` k ) = ( ( _pi / 4 ) x. ( ( n e. NN |-> ( ( 4 / _pi ) x. ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ` k ) ) )
1561	6 7 62 1510 1542 1560	isermulc2	|- ( T. -> seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> ( ( _pi / 4 ) x. Y ) )
1562		climrel	|- Rel ~~>
1563	1562	releldmi	|- ( seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> ( ( _pi / 4 ) x. Y ) -> seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) e. dom ~~> )
1564	1561 1563	syl	|- ( T. -> seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) e. dom ~~> )
1565	6 7 19 55 1564	isumclim2	|- ( T. -> seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) )
1566	1565	mptru	|- seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) )
1567	1561	mptru	|- seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> ( ( _pi / 4 ) x. Y )
1568		climuni	|- ( ( seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) /\ seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) ~~> ( ( _pi / 4 ) x. Y ) ) -> sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) = ( ( _pi / 4 ) x. Y ) )
1569	1566 1567 1568	mp2an	|- sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) = ( ( _pi / 4 ) x. Y )
1570	1569	oveq2i	|- ( ( 4 / _pi ) x. sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = ( ( 4 / _pi ) x. ( ( _pi / 4 ) x. Y ) )
1571	58 56 73	divcli	|- ( 4 / _pi ) e. CC
1572	56 58 60	divcli	|- ( _pi / 4 ) e. CC
1573	1286 1151	eqeltri	|- ( F ` X ) e. RR
1574	71 1573	ifcli	|- if ( ( X mod _pi ) = 0 , 0 , ( F ` X ) ) e. RR
1575	5 1574	eqeltri	|- Y e. RR
1576	1575	recni	|- Y e. CC
1577	1571 1572 1576	mulassi	|- ( ( ( 4 / _pi ) x. ( _pi / 4 ) ) x. Y ) = ( ( 4 / _pi ) x. ( ( _pi / 4 ) x. Y ) )
1578	1572 1571 1544	mulcomli	|- ( ( 4 / _pi ) x. ( _pi / 4 ) ) = 1
1579	1578	oveq1i	|- ( ( ( 4 / _pi ) x. ( _pi / 4 ) ) x. Y ) = ( 1 x. Y )
1580	1576	mulid2i	|- ( 1 x. Y ) = Y
1581	1579 1580	eqtri	|- ( ( ( 4 / _pi ) x. ( _pi / 4 ) ) x. Y ) = Y
1582	1570 1577 1581	3eqtr2i	|- ( ( 4 / _pi ) x. sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = Y
1583		seqeq3	|- ( S = ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) -> seq 1 ( + , S ) = seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) ) )
1584	4 1583	ax-mp	|- seq 1 ( + , S ) = seq 1 ( + , ( n e. NN |-> ( ( sin ` ( ( ( 2 x. n ) - 1 ) x. X ) ) / ( ( 2 x. n ) - 1 ) ) ) )
1585	1584 1567	eqbrtri	|- seq 1 ( + , S ) ~~> ( ( _pi / 4 ) x. Y )
1586	1582 1585	pm3.2i	|- ( ( ( 4 / _pi ) x. sum_ k e. NN ( ( sin ` ( ( ( 2 x. k ) - 1 ) x. X ) ) / ( ( 2 x. k ) - 1 ) ) ) = Y /\ seq 1 ( + , S ) ~~> ( ( _pi / 4 ) x. Y ) )