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