Theorem fourierdlem49

Description: The given periodic function F has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem49.a	|- ( ph -> A e. RR )
	fourierdlem49.b	|- ( ph -> B e. RR )
	fourierdlem49.altb	|- ( ph -> A < B )
	fourierdlem49.p	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem49.t	|- T = ( B - A )
	fourierdlem49.m	|- ( ph -> M e. NN )
	fourierdlem49.q	|- ( ph -> Q e. ( P ` M ) )
	fourierdlem49.d	|- ( ph -> D C_ RR )
	fourierdlem49.f	|- ( ph -> F : D --> RR )
	fourierdlem49.dper	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
	fourierdlem49.per	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
	fourierdlem49.cn	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem49.l	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
	fourierdlem49.x	|- ( ph -> X e. RR )
	fourierdlem49.z	|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
	fourierdlem49.e	|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
Assertion	fourierdlem49	|- ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem49.a	|- ( ph -> A e. RR )
2		fourierdlem49.b	|- ( ph -> B e. RR )
3		fourierdlem49.altb	|- ( ph -> A < B )
4		fourierdlem49.p	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
5		fourierdlem49.t	|- T = ( B - A )
6		fourierdlem49.m	|- ( ph -> M e. NN )
7		fourierdlem49.q	|- ( ph -> Q e. ( P ` M ) )
8		fourierdlem49.d	|- ( ph -> D C_ RR )
9		fourierdlem49.f	|- ( ph -> F : D --> RR )
10		fourierdlem49.dper	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
11		fourierdlem49.per	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
12		fourierdlem49.cn	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
13		fourierdlem49.l	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
14		fourierdlem49.x	|- ( ph -> X e. RR )
15		fourierdlem49.z	|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
16		fourierdlem49.e	|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
17		ovex	|- ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
18	15	fvmpt2	|- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
19	17 18	mpan2	|- ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
20	19	oveq2d	|- ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
21	20	mpteq2ia	|- ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
22	16 21	eqtri	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
23	1 2 3 5 22	fourierdlem4	|- ( ph -> E : RR --> ( A (,] B ) )
24	23 14	ffvelcdmd	|- ( ph -> ( E ` X ) e. ( A (,] B ) )
25		simpr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
26	4	fourierdlem2	|- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
27	6 26	syl	|- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
28	7 27	mpbid	|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
29	28	simpld	|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
30		elmapi	|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
31	29 30	syl	|- ( ph -> Q : ( 0 ... M ) --> RR )
32	31	ffnd	|- ( ph -> Q Fn ( 0 ... M ) )
33	32	ad2antrr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
34		fvelrnb	|- ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
35	33 34	syl	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
36	25 35	mpbid	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
37		fveq2	|- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
38		fvoveq1	|- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
39	37 38	oveq12d	|- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
40	39	eleq2d	|- ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
41		nnuz	|- NN = ( ZZ>= ` 1 )
42		1zzd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
43		elfzelz	|- ( j e. ( 0 ... M ) -> j e. ZZ )
44	43	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
45		1e0p1	|- 1 = ( 0 + 1 )
46	44	zred	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
47		elfzle1	|- ( j e. ( 0 ... M ) -> 0 <_ j )
48	47	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ j )
49		id	|- ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
50	49	eqcomd	|- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
51	50	ad2antlr	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
52		fveq2	|- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
53	52	adantl	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
54	28	simprld	|- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
55	54	simpld	|- ( ph -> ( Q ` 0 ) = A )
56	55	ad2antrr	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
57	51 53 56	3eqtrd	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
58	57	adantllr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
59	58	adantllr	|- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
60	1	adantr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
61	1	rexrd	|- ( ph -> A e. RR* )
62	61	adantr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
63	2	rexrd	|- ( ph -> B e. RR* )
64	63	adantr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
65		simpr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
66	62 64 65	iocgtlbd	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
67	60 66	gtned	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
68	67	neneqd	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
69	68	ad3antrrr	|- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> -. ( E ` X ) = A )
70	59 69	pm2.65da	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
71	70	neqned	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
72	46 48 71	ne0gt0d	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
73		0zd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
74	73 44	zltp1led	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
75	72 74	mpbid	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
76	45 75	eqbrtrid	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
77	41 42 44 76	eluzd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
78		nnm1nn0	|- ( j e. NN -> ( j - 1 ) e. NN0 )
79	77 78	syl	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. NN0 )
80		nn0uz	|- NN0 = ( ZZ>= ` 0 )
81	79 80	eleqtrdi	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
82	6	nnzd	|- ( ph -> M e. ZZ )
83	82	ad3antrrr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
84		peano2zm	|- ( j e. ZZ -> ( j - 1 ) e. ZZ )
85	43 84	syl	|- ( j e. ( 0 ... M ) -> ( j - 1 ) e. ZZ )
86	85	zred	|- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
87	43	zred	|- ( j e. ( 0 ... M ) -> j e. RR )
88		elfzel2	|- ( j e. ( 0 ... M ) -> M e. ZZ )
89	88	zred	|- ( j e. ( 0 ... M ) -> M e. RR )
90	87	ltm1d	|- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
91		elfzle2	|- ( j e. ( 0 ... M ) -> j <_ M )
92	86 87 89 90 91	ltletrd	|- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
93	92	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
94	81 83 93	elfzod	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ..^ M ) )
95	31	ad3antrrr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
96	44 84	syl	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
97	79	nn0ge0d	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
98	86 89 92	ltled	|- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
99	98	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
100	73 83 96 97 99	elfzd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
101	95 100	ffvelcdmd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
102	101	rexrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
103	31	ffvelcdmda	|- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
104	103	rexrd	|- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
105	104	adantlr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
106	105	adantr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
107		iocssre	|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
108	61 2 107	syl2anc	|- ( ph -> ( A (,] B ) C_ RR )
109	108	sselda	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
110	109	rexrd	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
111	110	ad2antrr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
112		simplll	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
113		ovex	|- ( j - 1 ) e. _V
114		eleq1	|- ( i = ( j - 1 ) -> ( i e. ( 0 ..^ M ) <-> ( j - 1 ) e. ( 0 ..^ M ) ) )
115	114	anbi2d	|- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) ) )
116	37 38	breq12d	|- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
117	115 116	imbi12d	|- ( i = ( j - 1 ) -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
118	28	simprrd	|- ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
119	118	r19.21bi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
120	113 117 119	vtocl	|- ( ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
121	112 94 120	syl2anc	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
122	43	zcnd	|- ( j e. ( 0 ... M ) -> j e. CC )
123		1cnd	|- ( j e. ( 0 ... M ) -> 1 e. CC )
124	122 123	npcand	|- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
125	124	eqcomd	|- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
126	125	fveq2d	|- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
127	126	eqcomd	|- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
128	127	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
129	121 128	breqtrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
130		simpr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
131	129 130	breqtrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
132	108 24	sseldd	|- ( ph -> ( E ` X ) e. RR )
133	132	leidd	|- ( ph -> ( E ` X ) <_ ( E ` X ) )
134	133	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
135	50	adantl	|- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
136	134 135	breqtrd	|- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
137	136	adantllr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
138	102 106 111 131 137	eliocd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) )
139	126	oveq2d	|- ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
140	139	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
141	138 140	eleqtrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
142	40 94 141	rspcedvdw	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
143	142	ex	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
144	143	adantlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) /\ j e. ( 0 ... M ) ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
145	144	rexlimdva	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
146	36 145	mpd	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
147	6	ad2antrr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
148	31	ad2antrr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
149		iocssicc	|- ( A (,] B ) C_ ( A [,] B )
150	55	eqcomd	|- ( ph -> A = ( Q ` 0 ) )
151	54	simprd	|- ( ph -> ( Q ` M ) = B )
152	151	eqcomd	|- ( ph -> B = ( Q ` M ) )
153	150 152	oveq12d	|- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
154	149 153	sseqtrid	|- ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
155	154	sselda	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
156	155	adantr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
157		simpr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
158		fveq2	|- ( k = j -> ( Q ` k ) = ( Q ` j ) )
159	158	breq1d	|- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
160	159	cbvrabv	|- { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) }
161	160	supeq1i	|- sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
162	147 148 156 157 161	fourierdlem25	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
163		ioossioc	|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
164	163	sseli	|- ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
165	164	a1i	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0 ..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
166	165	reximdva	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
167	162 166	mpd	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
168	146 167	pm2.61dan	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
169	24 168	mpdan	|- ( ph -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
170		resindm	|- ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( -oo (,) ( E ` X ) ) )
171	9	fdmd	|- ( ph -> dom F = D )
172	171	ineq2d	|- ( ph -> ( ( -oo (,) ( E ` X ) ) i^i dom F ) = ( ( -oo (,) ( E ` X ) ) i^i D ) )
173	172	reseq2d	|- ( ph -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
174	170 173	eqtr3id	|- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
175	174	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
176	175	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) limCC ( E ` X ) ) )
177		ax-resscn	|- RR C_ CC
178	177	a1i	|- ( ph -> RR C_ CC )
179	9 178	fssd	|- ( ph -> F : D --> CC )
180	179	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> F : D --> CC )
181		inss2	|- ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D
182	181	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D )
183	180 182	fssresd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) : ( ( -oo (,) ( E ` X ) ) i^i D ) --> CC )
184		mnfxr	|- -oo e. RR*
185	31	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
186		elfzofz	|- ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
187	186	adantl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
188	185 187	ffvelcdmd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
189	188	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
190	189	mnfled	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo <_ ( Q ` i ) )
191		iooss1	|- ( ( -oo e. RR* /\ -oo <_ ( Q ` i ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
192	184 190 191	sylancr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
193	192	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
194		fzofzp1	|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
195	194	adantl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
196	185 195	ffvelcdmd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
197	196	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
198	197	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
199	188	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
200	199	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
201		simp3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
202	200 198 201	iocleubd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
203		iooss2	|- ( ( ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) <_ ( Q ` ( i + 1 ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
204	198 202 203	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
205		cncff	|- ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
206		fdm	|- ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
207	12 205 206	3syl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
208		ssdmres	|- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
209	207 208	sylibr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
210	171	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom F = D )
211	209 210	sseqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
212	211	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
213	204 212	sstrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
214	193 213	ssind	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( -oo (,) ( E ` X ) ) i^i D ) )
215	8 178	sstrd	|- ( ph -> D C_ CC )
216	215	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D C_ CC )
217	216	ssinss2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ CC )
218		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
219		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
220	132	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
221	220	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR* )
222	200 198 201	iocgtlbd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
223	220	leidd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( E ` X ) )
224	200 221 221 222 223	eliocd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( E ` X ) ) )
225		ioounsn	|- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ ( Q ` i ) < ( E ` X ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
226	200 221 222 225	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
227	226	fveq2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) )
228	218	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
229		ovex	|- ( -oo (,) ( E ` X ) ) e. _V
230	229	inex1	|- ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V
231		snex	|- { ( E ` X ) } e. _V
232	230 231	unex	|- ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V
233		resttop	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top )
234	228 232 233	mp2an	|- ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top
235		retop	|- ( topGen ` ran (,) ) e. Top
236		iooretop	|- ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) )
237	236	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) ) )
238		elrestr	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V /\ ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
239	235 232 237 238	mp3an12i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
240		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x = ( E ` X ) )
241		pnfxr	|- +oo e. RR*
242	241	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> +oo e. RR* )
243	220	ltpnfd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < +oo )
244	200 242 220 222 243	eliood	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) +oo ) )
245		snidg	|- ( ( E ` X ) e. RR -> ( E ` X ) e. { ( E ` X ) } )
246		elun2	|- ( ( E ` X ) e. { ( E ` X ) } -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
247	132 245 246	3syl	|- ( ph -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
248	247	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
249	244 248	elind	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
250	249	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
251	240 250	eqeltrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
252	251	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
253	200	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
254	241	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> +oo e. RR* )
255	189	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
256	132	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR )
257		iocssre	|- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
258	255 256 257	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
259		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
260	258 259	sseldd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
261	260	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
262	256	rexrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR* )
263	255 262 259	iocgtlbd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
264	263	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
265	261	ltpnfd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x < +oo )
266	253 254 261 264 265	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
267	266	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
268	184	a1i	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo e. RR* )
269	262	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR* )
270	260	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
271	270	mnfltd	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo < x )
272	132	ad3antrrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
273	255 262 259	iocleubd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
274	273	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x <_ ( E ` X ) )
275		neqne	|- ( -. x = ( E ` X ) -> x =/= ( E ` X ) )
276	275	necomd	|- ( -. x = ( E ` X ) -> ( E ` X ) =/= x )
277	276	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) =/= x )
278	270 272 274 277	leneltd	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
279	268 269 270 271 278	eliood	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
280	279	3adantll3	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
281	212	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
282	200	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` i ) e. RR* )
283	198	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
284	261	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
285	264	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` i ) < x )
286	220	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
287	197	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
288	278	3adantll3	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
289	202	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
290	284 286 287 288 289	ltletrd	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( Q ` ( i + 1 ) ) )
291	282 283 284 285 290	eliood	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
292	281 291	sseldd	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. D )
293	280 292	elind	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
294		elun1	|- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
295	293 294	syl	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
296	267 295	elind	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
297	252 296	pm2.61dan	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
298	200	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) e. RR* )
299	221	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( E ` X ) e. RR* )
300		elinel1	|- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
301		elioore	|- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR )
302	301	rexrd	|- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR* )
303	300 302	syl	|- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. RR* )
304	303	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. RR* )
305	189	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) e. RR* )
306	241	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> +oo e. RR* )
307	300	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
308	305 306 307	ioogtlbd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
309	308	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
310		elinel2	|- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
311		elsni	|- ( x e. { ( E ` X ) } -> x = ( E ` X ) )
312	311	adantl	|- ( ( ph /\ x e. { ( E ` X ) } ) -> x = ( E ` X ) )
313	133	adantr	|- ( ( ph /\ x e. { ( E ` X ) } ) -> ( E ` X ) <_ ( E ` X ) )
314	312 313	eqbrtrd	|- ( ( ph /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
315	314	adantlr	|- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
316		simpll	|- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> ph )
317		elunnel2	|- ( ( x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) /\ -. x e. { ( E ` X ) } ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
318	317	adantll	|- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
319		elinel1	|- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( -oo (,) ( E ` X ) ) )
320		elioore	|- ( x e. ( -oo (,) ( E ` X ) ) -> x e. RR )
321	320	adantl	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. RR )
322	132	adantr	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR )
323	184	a1i	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> -oo e. RR* )
324	322	rexrd	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR* )
325		simpr	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. ( -oo (,) ( E ` X ) ) )
326	323 324 325	iooltubd	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
327	321 322 326	ltled	|- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x <_ ( E ` X ) )
328	319 327	sylan2	|- ( ( ph /\ x e. ( ( -oo (,) ( E ` X ) ) i^i D ) ) -> x <_ ( E ` X ) )
329	316 318 328	syl2anc	|- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
330	315 329	pm2.61dan	|- ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
331	330	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
332	310 331	sylan2	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x <_ ( E ` X ) )
333	332	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x <_ ( E ` X ) )
334	298 299 304 309 333	eliocd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
335	297 334	impbida	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( x e. ( ( Q ` i ) (,] ( E ` X ) ) <-> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) )
336	335	eqrdv	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) = ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
337		ioossre	|- ( -oo (,) ( E ` X ) ) C_ RR
338		ssinss1	|- ( ( -oo (,) ( E ` X ) ) C_ RR -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ RR )
339	337 338	mp1i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ RR )
340	220	snssd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { ( E ` X ) } C_ RR )
341	339 340	unssd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) C_ RR )
342		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
343	218 342	rerest	|- ( ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
344	341 343	syl	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
345	239 336 344	3eltr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
346		isopn3i	|- ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top /\ ( ( Q ` i ) (,] ( E ` X ) ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) = ( ( Q ` i ) (,] ( E ` X ) ) )
347	234 345 346	sylancr	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) = ( ( Q ` i ) (,] ( E ` X ) ) )
348	227 347	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) )
349	224 348	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) )
350	183 214 217 218 219 349	limcres	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) limCC ( E ` X ) ) )
351	214	resabs1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
352	351	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
353	176 350 352	3eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
354	179	ffdmd	|- ( ph -> F : dom F --> CC )
355	354	adantr	|- ( ( ph /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> F : dom F --> CC )
356	355	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> F : dom F --> CC )
357		ioosscn	|- ( ( Q ` i ) (,) ( E ` X ) ) C_ CC
358	357	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ CC )
359	171	eqcomd	|- ( ph -> D = dom F )
360	359	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D = dom F )
361	213 360	sseqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ dom F )
362	361	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ dom F )
363		oveq2	|- ( x = X -> ( B - x ) = ( B - X ) )
364	363	fvoveq1d	|- ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
365	364	oveq1d	|- ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
366	2 14	resubcld	|- ( ph -> ( B - X ) e. RR )
367	2 1	resubcld	|- ( ph -> ( B - A ) e. RR )
368	5 367	eqeltrid	|- ( ph -> T e. RR )
369	1 2	posdifd	|- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
370	3 369	mpbid	|- ( ph -> 0 < ( B - A ) )
371	370 5	breqtrrdi	|- ( ph -> 0 < T )
372	371	gt0ne0d	|- ( ph -> T =/= 0 )
373	366 368 372	redivcld	|- ( ph -> ( ( B - X ) / T ) e. RR )
374	373	flcld	|- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
375	374	zred	|- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
376	375 368	remulcld	|- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
377	15 365 14 376	fvmptd3	|- ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
378	377 376	eqeltrd	|- ( ph -> ( Z ` X ) e. RR )
379	378	recnd	|- ( ph -> ( Z ` X ) e. CC )
380	379	adantr	|- ( ( ph /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( Z ` X ) e. CC )
381	380	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( Z ` X ) e. CC )
382	381	negcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> -u ( Z ` X ) e. CC )
383		eqid	|- { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) }
384		ioosscn	|- ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ CC
385	384	sseli	|- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. CC )
386	385	adantl	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. CC )
387	379	adantr	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. CC )
388	386 387	pncand	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = y )
389	388	eqcomd	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) - ( Z ` X ) ) )
390	389	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) - ( Z ` X ) ) )
391	377	oveq2d	|- ( ph -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
392	391	adantr	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
393	386 387	addcld	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. CC )
394	376	recnd	|- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
395	394	adantr	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
396	393 395	negsubd	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
397	374	zcnd	|- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
398	368	recnd	|- ( ph -> T e. CC )
399	397 398	mulneg1d	|- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
400	399	eqcomd	|- ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
401	400	oveq2d	|- ( ph -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
402	401	adantr	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
403	392 396 402	3eqtr2d	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
404	403	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
405	374	znegcld	|- ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
406	405	adantr	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
407	406	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
408		simpl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
409	213	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
410	189	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR* )
411	132	rexrd	|- ( ph -> ( E ` X ) e. RR* )
412	411	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) e. RR* )
413		elioore	|- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
414	413	adantl	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
415	378	adantr	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
416	414 415	readdcld	|- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
417	416	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
418	378	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Z ` X ) e. RR )
419	188 418	resubcld	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
420	419	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
421	420	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
422	14	rexrd	|- ( ph -> X e. RR* )
423	422	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
424		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
425	421 423 424	ioogtlbd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
426	188	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
427	378	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
428	413	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
429	426 427 428	ltsubaddd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < y <-> ( Q ` i ) < ( y + ( Z ` X ) ) ) )
430	425 429	mpbid	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
431	14	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
432	421 423 424	iooltubd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
433	428 431 427 432	ltadd1dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
434		id	|- ( x = X -> x = X )
435		fveq2	|- ( x = X -> ( Z ` x ) = ( Z ` X ) )
436	434 435	oveq12d	|- ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
437	14 378	readdcld	|- ( ph -> ( X + ( Z ` X ) ) e. RR )
438	16 436 14 437	fvmptd3	|- ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
439	438	eqcomd	|- ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
440	439	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
441	433 440	breqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
442	410 412 417 430 441	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( E ` X ) ) )
443	442	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( E ` X ) ) )
444	409 443	sseldd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. D )
445	408 444 407	3jca	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
446		eleq1	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
447	446	3anbi3d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
448		oveq1	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
449	448	oveq2d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
450	449	eleq1d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
451	447 450	imbi12d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) ) )
452		ovex	|- ( y + ( Z ` X ) ) e. _V
453		eleq1	|- ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
454	453	3anbi2d	|- ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
455		oveq1	|- ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
456	455	eleq1d	|- ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
457	454 456	imbi12d	|- ( x = ( y + ( Z ` X ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) ) )
458	452 457 10	vtocl	|- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
459	451 458	vtoclg	|- ( -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
460	407 445 459	sylc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
461	404 460	eqeltrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) e. D )
462	390 461	eqeltrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. D )
463	462	ssd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
464	188	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
465	379	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Z ` X ) e. CC )
466	464 465	negsubd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + -u ( Z ` X ) ) = ( ( Q ` i ) - ( Z ` X ) ) )
467	466	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) = ( ( Q ` i ) + -u ( Z ` X ) ) )
468	438	oveq1d	|- ( ph -> ( ( E ` X ) + -u ( Z ` X ) ) = ( ( X + ( Z ` X ) ) + -u ( Z ` X ) ) )
469	437	recnd	|- ( ph -> ( X + ( Z ` X ) ) e. CC )
470	469 379	negsubd	|- ( ph -> ( ( X + ( Z ` X ) ) + -u ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
471	14	recnd	|- ( ph -> X e. CC )
472	471 379	pncand	|- ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
473	468 470 472	3eqtrrd	|- ( ph -> X = ( ( E ` X ) + -u ( Z ` X ) ) )
474	473	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X = ( ( E ` X ) + -u ( Z ` X ) ) )
475	467 474	oveq12d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) = ( ( ( Q ` i ) + -u ( Z ` X ) ) (,) ( ( E ` X ) + -u ( Z ` X ) ) ) )
476	132	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E ` X ) e. RR )
477	418	renegcld	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u ( Z ` X ) e. RR )
478	188 476 477	iooshift	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + -u ( Z ` X ) ) (,) ( ( E ` X ) + -u ( Z ` X ) ) ) = { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } )
479	475 478	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
480	479	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
481	171	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> dom F = D )
482	463 480 481	3sstr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } C_ dom F )
483	482	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } C_ dom F )
484	377	negeqd	|- ( ph -> -u ( Z ` X ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
485	484 400	eqtrd	|- ( ph -> -u ( Z ` X ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
486	485	oveq2d	|- ( ph -> ( x + -u ( Z ` X ) ) = ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
487	486	fveq2d	|- ( ph -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
488	487	adantr	|- ( ( ph /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
489	488	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
490	405	adantr	|- ( ( ph /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
491	490	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
492		simpl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ph )
493	213	sselda	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> x e. D )
494	492 493 491	3jca	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
495	446	3anbi3d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
496	448	oveq2d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
497	496	fveqeq2d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
498	495 497	imbi12d	|- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
499	498 11	vtoclg	|- ( -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
500	491 494 499	sylc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) )
501	489 500	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` x ) )
502	501	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` x ) )
503		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
504	356 358 362 382 383 483 502 503	limcperiod	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> y e. ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) )
505	479	reseq2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) = ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) )
506	474	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( E ` X ) + -u ( Z ` X ) ) = X )
507	505 506	oveq12d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
508	507	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
509	508	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) limCC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
510	504 509	eleqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) -> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
511	354	adantr	|- ( ( ph /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> F : dom F --> CC )
512	511	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> F : dom F --> CC )
513	384	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ CC )
514	463 481	sseqtrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ dom F )
515	514	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ dom F )
516	379	adantr	|- ( ( ph /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( Z ` X ) e. CC )
517	516	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( Z ` X ) e. CC )
518		eqid	|- { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) }
519	464 465	npcand	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` i ) )
520	519	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) )
521	438	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
522	520 521	oveq12d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) = ( ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) (,) ( X + ( Z ` X ) ) ) )
523	14	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
524	419 523 418	iooshift	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) (,) ( X + ( Z ` X ) ) ) = { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } )
525	522 524	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = ( ( Q ` i ) (,) ( E ` X ) ) )
526	525	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = ( ( Q ` i ) (,) ( E ` X ) ) )
527	213 526 481	3sstr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } C_ dom F )
528	527	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } C_ dom F )
529	377	oveq2d	|- ( ph -> ( x + ( Z ` X ) ) = ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
530	529	fveq2d	|- ( ph -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
531	530	adantr	|- ( ( ph /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
532	531	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
533	374	adantr	|- ( ( ph /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
534	533	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
535		simpl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
536	463	sselda	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. D )
537	535 536 534	3jca	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
538		eleq1	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
539	538	3anbi3d	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
540		oveq1	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
541	540	oveq2d	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
542	541	fveqeq2d	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
543	539 542	imbi12d	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
544	543 11	vtoclg	|- ( ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
545	534 537 544	sylc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) )
546	532 545	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` x ) )
547	546	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` x ) )
548		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
549	512 513 515 517 518 528 547 548	limcperiod	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> y e. ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) )
550	525	reseq2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
551	439	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
552	550 551	oveq12d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
553	552	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
554	553	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) limCC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
555	549 554	eleqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) -> y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
556	510 555	impbida	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) <-> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) ) )
557	556	eqrdv	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
558		resindm	|- ( F |` ( ( -oo (,) X ) i^i dom F ) ) = ( F |` ( -oo (,) X ) )
559	171	ineq2d	|- ( ph -> ( ( -oo (,) X ) i^i dom F ) = ( ( -oo (,) X ) i^i D ) )
560	559	reseq2d	|- ( ph -> ( F |` ( ( -oo (,) X ) i^i dom F ) ) = ( F |` ( ( -oo (,) X ) i^i D ) ) )
561	558 560	eqtr3id	|- ( ph -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i D ) ) )
562	561	oveq1d	|- ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) )
563	562	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) )
564		inss2	|- ( ( -oo (,) X ) i^i D ) C_ D
565	564	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) X ) i^i D ) C_ D )
566	180 565	fssresd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( -oo (,) X ) i^i D ) ) : ( ( -oo (,) X ) i^i D ) --> CC )
567	420	mnfled	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo <_ ( ( Q ` i ) - ( Z ` X ) ) )
568		iooss1	|- ( ( -oo e. RR* /\ -oo <_ ( ( Q ` i ) - ( Z ` X ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
569	184 567 568	sylancr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
570	569	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
571	570 463	ssind	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( ( -oo (,) X ) i^i D ) )
572	216	ssinss2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) X ) i^i D ) C_ CC )
573		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
574	420	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
575	422	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. RR* )
576	438	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
577	222 576	breqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + ( Z ` X ) ) )
578	378	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
579	14	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
580	199 578 579	ltsubaddd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < X <-> ( Q ` i ) < ( X + ( Z ` X ) ) ) )
581	577 580	mpbird	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
582	14	leidd	|- ( ph -> X <_ X )
583	582	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X <_ X )
584	574 575 575 581 583	eliocd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
585		ioounsn	|- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ ( ( Q ` i ) - ( Z ` X ) ) < X ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
586	574 575 581 585	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
587	586	fveq2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) )
588		ovex	|- ( -oo (,) X ) e. _V
589	588	inex1	|- ( ( -oo (,) X ) i^i D ) e. _V
590		snex	|- { X } e. _V
591	589 590	unex	|- ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V
592		resttop	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top )
593	228 591 592	mp2an	|- ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top
594		iooretop	|- ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) )
595	594	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) ) )
596		elrestr	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
597	235 591 595 596	mp3an12i	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
598	420	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
599	241	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> +oo e. RR* )
600	14	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> X e. RR )
601		iocssre	|- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) C_ RR )
602	598 600 601	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) C_ RR )
603		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
604	602 603	sseldd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. RR )
605	422	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> X e. RR* )
606	598 605 603	iocgtlbd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
607	604	ltpnfd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x < +oo )
608	598 599 604 606 607	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
609	608	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
610		eqvisset	|- ( x = X -> X e. _V )
611		snidg	|- ( X e. _V -> X e. { X } )
612	610 611	syl	|- ( x = X -> X e. { X } )
613	434 612	eqeltrd	|- ( x = X -> x e. { X } )
614		elun2	|- ( x e. { X } -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
615	613 614	syl	|- ( x = X -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
616	615	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ x = X ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
617		simpll	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
618	420	ad2antrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
619	422	ad3antrrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X e. RR* )
620	604	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. RR )
621	606	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
622	14	ad3antrrr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X e. RR )
623	598 605 603	iocleubd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x <_ X )
624	623	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x <_ X )
625	434	eqcoms	|- ( X = x -> x = X )
626	625	necon3bi	|- ( -. x = X -> X =/= x )
627	626	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X =/= x )
628	620 622 624 627	leneltd	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x < X )
629	618 619 620 621 628	eliood	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
630	629	3adantll3	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
631	571	sselda	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. ( ( -oo (,) X ) i^i D ) )
632		elun1	|- ( x e. ( ( -oo (,) X ) i^i D ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
633	631 632	syl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
634	617 630 633	syl2anc	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
635	616 634	pm2.61dan	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
636	609 635	elind	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
637	574	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
638	575	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> X e. RR* )
639		elinel1	|- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
640		elioore	|- ( x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) -> x e. RR )
641	639 640	syl	|- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. RR )
642	641	rexrd	|- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. RR* )
643	642	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. RR* )
644	420	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
645	241	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> +oo e. RR* )
646	639	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
647	644 645 646	ioogtlbd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
648	647	3adantl3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
649		elinel2	|- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
650		elsni	|- ( x e. { X } -> x = X )
651	650	adantl	|- ( ( ph /\ x e. { X } ) -> x = X )
652	582	adantr	|- ( ( ph /\ x e. { X } ) -> X <_ X )
653	651 652	eqbrtrd	|- ( ( ph /\ x e. { X } ) -> x <_ X )
654	653	adantlr	|- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ x e. { X } ) -> x <_ X )
655		simpll	|- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> ph )
656		elunnel2	|- ( ( x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) /\ -. x e. { X } ) -> x e. ( ( -oo (,) X ) i^i D ) )
657	656	adantll	|- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x e. ( ( -oo (,) X ) i^i D ) )
658	657	elin1d	|- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x e. ( -oo (,) X ) )
659		elioore	|- ( x e. ( -oo (,) X ) -> x e. RR )
660	659	adantl	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> x e. RR )
661	14	adantr	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> X e. RR )
662	184	a1i	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> -oo e. RR* )
663	422	adantr	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> X e. RR* )
664		simpr	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> x e. ( -oo (,) X ) )
665	662 663 664	iooltubd	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> x < X )
666	660 661 665	ltled	|- ( ( ph /\ x e. ( -oo (,) X ) ) -> x <_ X )
667	655 658 666	syl2anc	|- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x <_ X )
668	654 667	pm2.61dan	|- ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x <_ X )
669	649 668	sylan2	|- ( ( ph /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x <_ X )
670	669	3ad2antl1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x <_ X )
671	637 638 643 648 670	eliocd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
672	636 671	impbida	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) <-> x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) )
673	672	eqrdv	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) = ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
674	8	ssinss2d	|- ( ph -> ( ( -oo (,) X ) i^i D ) C_ RR )
675	14	snssd	|- ( ph -> { X } C_ RR )
676	674 675	unssd	|- ( ph -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR )
677	676	3ad2ant1	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR )
678	218 342	rerest	|- ( ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
679	677 678	syl	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
680	597 673 679	3eltr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
681		isopn3i	|- ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
682	593 680 681	sylancr	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
683	587 682	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) )
684	584 683	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) )
685	566 571 572 218 573 684	limcres	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) limCC X ) )
686	571	resabs1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) = ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) )
687	686	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) )
688	563 685 687	3eqtr2rd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) X ) ) limCC X ) )
689	353 557 688	3eqtrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
690	689	rexlimdv3a	|- ( ph -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) ) )
691	169 690	mpd	|- ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
692	119	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
693	12	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
694	13	3adant3	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
695		eqid	|- if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) = if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) )
696		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
697	199 197 692 693 694 199 220 222 204 695 696	fourierdlem33	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
698	204	resabs1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
699	698	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
700	697 699	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) )
701	700	ne0d	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
702	353 701	eqnetrd	|- ( ( ph /\ i e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
703	702	rexlimdv3a	|- ( ph -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) ) )
704	169 703	mpd	|- ( ph -> ( ( F |` ( -oo (,) ( E ` X ) ) ) limCC ( E ` X ) ) =/= (/) )
705	691 704	eqnetrd	|- ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) )