Theorem fourierdlem48

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

	Ref	Expression
Hypotheses	fourierdlem48.a	|- ( ph -> A e. RR )
	fourierdlem48.b	|- ( ph -> B e. RR )
	fourierdlem48.altb	|- ( ph -> A < B )
	fourierdlem48.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 ) ) ) } )
	fourierdlem48.t	|- T = ( B - A )
	fourierdlem48.m	|- ( ph -> M e. NN )
	fourierdlem48.q	|- ( ph -> Q e. ( P ` M ) )
	fourierdlem48.f	|- ( ph -> F : D --> RR )
	fourierdlem48.dper	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
	fourierdlem48.per	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
	fourierdlem48.cn	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem48.r	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
	fourierdlem48.x	|- ( ph -> X e. RR )
	fourierdlem48.z	|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
	fourierdlem48.e	|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
	fourierdlem48.ch	|- ( ch <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ y = ( X + ( k x. T ) ) ) )
Assertion	fourierdlem48	|- ( ph -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem48.a	|- ( ph -> A e. RR )
2		fourierdlem48.b	|- ( ph -> B e. RR )
3		fourierdlem48.altb	|- ( ph -> A < B )
4		fourierdlem48.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		fourierdlem48.t	|- T = ( B - A )
6		fourierdlem48.m	|- ( ph -> M e. NN )
7		fourierdlem48.q	|- ( ph -> Q e. ( P ` M ) )
8		fourierdlem48.f	|- ( ph -> F : D --> RR )
9		fourierdlem48.dper	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
10		fourierdlem48.per	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
11		fourierdlem48.cn	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
12		fourierdlem48.r	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
13		fourierdlem48.x	|- ( ph -> X e. RR )
14		fourierdlem48.z	|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
15		fourierdlem48.e	|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
16		fourierdlem48.ch	|- ( ch <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ y = ( X + ( k x. T ) ) ) )
17		simpl	|- ( ( ph /\ ( E ` X ) = B ) -> ph )
18		0zd	|- ( ph -> 0 e. ZZ )
19	6	nnzd	|- ( ph -> M e. ZZ )
20	6	nngt0d	|- ( ph -> 0 < M )
21		fzolb	|- ( 0 e. ( 0 ..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
22	18 19 20 21	syl3anbrc	|- ( ph -> 0 e. ( 0 ..^ M ) )
23	22	adantr	|- ( ( ph /\ ( E ` X ) = B ) -> 0 e. ( 0 ..^ M ) )
24	2 13	resubcld	|- ( ph -> ( B - X ) e. RR )
25	2 1	resubcld	|- ( ph -> ( B - A ) e. RR )
26	5 25	eqeltrid	|- ( ph -> T e. RR )
27	1 2	posdifd	|- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
28	3 27	mpbid	|- ( ph -> 0 < ( B - A ) )
29	28 5	breqtrrdi	|- ( ph -> 0 < T )
30	29	gt0ne0d	|- ( ph -> T =/= 0 )
31	24 26 30	redivcld	|- ( ph -> ( ( B - X ) / T ) e. RR )
32	31	adantr	|- ( ( ph /\ ( E ` X ) = B ) -> ( ( B - X ) / T ) e. RR )
33	32	flcld	|- ( ( ph /\ ( E ` X ) = B ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
34		1zzd	|- ( ( ph /\ ( E ` X ) = B ) -> 1 e. ZZ )
35	33 34	zsubcld	|- ( ( ph /\ ( E ` X ) = B ) -> ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) e. ZZ )
36		id	|- ( ( E ` X ) = B -> ( E ` X ) = B )
37	5	a1i	|- ( ( E ` X ) = B -> T = ( B - A ) )
38	36 37	oveq12d	|- ( ( E ` X ) = B -> ( ( E ` X ) - T ) = ( B - ( B - A ) ) )
39	2	recnd	|- ( ph -> B e. CC )
40	1	recnd	|- ( ph -> A e. CC )
41	39 40	nncand	|- ( ph -> ( B - ( B - A ) ) = A )
42	38 41	sylan9eqr	|- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = A )
43	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 ) ) ) ) ) )
44	6 43	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 ) ) ) ) ) )
45	7 44	mpbid	|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
46	45	simpld	|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
47		elmapi	|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
48	46 47	syl	|- ( ph -> Q : ( 0 ... M ) --> RR )
49	6	nnnn0d	|- ( ph -> M e. NN0 )
50		nn0uz	|- NN0 = ( ZZ>= ` 0 )
51	49 50	eleqtrdi	|- ( ph -> M e. ( ZZ>= ` 0 ) )
52		eluzfz1	|- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
53	51 52	syl	|- ( ph -> 0 e. ( 0 ... M ) )
54	48 53	ffvelrnd	|- ( ph -> ( Q ` 0 ) e. RR )
55	54	rexrd	|- ( ph -> ( Q ` 0 ) e. RR* )
56		1zzd	|- ( ph -> 1 e. ZZ )
57	18 19 56	3jca	|- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) )
58		0le1	|- 0 <_ 1
59	58	a1i	|- ( ph -> 0 <_ 1 )
60	6	nnge1d	|- ( ph -> 1 <_ M )
61	57 59 60	jca32	|- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
62		elfz2	|- ( 1 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
63	61 62	sylibr	|- ( ph -> 1 e. ( 0 ... M ) )
64	48 63	ffvelrnd	|- ( ph -> ( Q ` 1 ) e. RR )
65	64	rexrd	|- ( ph -> ( Q ` 1 ) e. RR* )
66	1	rexrd	|- ( ph -> A e. RR* )
67	45	simprd	|- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
68	67	simplld	|- ( ph -> ( Q ` 0 ) = A )
69	1	leidd	|- ( ph -> A <_ A )
70	68 69	eqbrtrd	|- ( ph -> ( Q ` 0 ) <_ A )
71	68	eqcomd	|- ( ph -> A = ( Q ` 0 ) )
72		0re	|- 0 e. RR
73		eleq1	|- ( i = 0 -> ( i e. ( 0 ..^ M ) <-> 0 e. ( 0 ..^ M ) ) )
74	73	anbi2d	|- ( i = 0 -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ 0 e. ( 0 ..^ M ) ) ) )
75		fveq2	|- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
76		oveq1	|- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
77	76	fveq2d	|- ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
78	75 77	breq12d	|- ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
79	74 78	imbi12d	|- ( i = 0 -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
80	45	simprrd	|- ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
81	80	r19.21bi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
82	79 81	vtoclg	|- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
83	72 82	ax-mp	|- ( ( ph /\ 0 e. ( 0 ..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
84	22 83	mpdan	|- ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
85		1e0p1	|- 1 = ( 0 + 1 )
86	85	fveq2i	|- ( Q ` 1 ) = ( Q ` ( 0 + 1 ) )
87	84 86	breqtrrdi	|- ( ph -> ( Q ` 0 ) < ( Q ` 1 ) )
88	71 87	eqbrtrd	|- ( ph -> A < ( Q ` 1 ) )
89	55 65 66 70 88	elicod	|- ( ph -> A e. ( ( Q ` 0 ) [,) ( Q ` 1 ) ) )
90	86	oveq2i	|- ( ( Q ` 0 ) [,) ( Q ` 1 ) ) = ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) )
91	89 90	eleqtrdi	|- ( ph -> A e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) )
92	91	adantr	|- ( ( ph /\ ( E ` X ) = B ) -> A e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) )
93	42 92	eqeltrd	|- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) )
94	15	a1i	|- ( ph -> E = ( x e. RR |-> ( x + ( Z ` x ) ) ) )
95		id	|- ( x = X -> x = X )
96		fveq2	|- ( x = X -> ( Z ` x ) = ( Z ` X ) )
97	95 96	oveq12d	|- ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
98	97	adantl	|- ( ( ph /\ x = X ) -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
99	14	a1i	|- ( ph -> Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
100		oveq2	|- ( x = X -> ( B - x ) = ( B - X ) )
101	100	oveq1d	|- ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
102	101	fveq2d	|- ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
103	102	oveq1d	|- ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
104	103	adantl	|- ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
105	31	flcld	|- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
106	105	zred	|- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
107	106 26	remulcld	|- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
108	99 104 13 107	fvmptd	|- ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
109	108 107	eqeltrd	|- ( ph -> ( Z ` X ) e. RR )
110	13 109	readdcld	|- ( ph -> ( X + ( Z ` X ) ) e. RR )
111	94 98 13 110	fvmptd	|- ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
112	108	oveq2d	|- ( ph -> ( X + ( Z ` X ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
113	111 112	eqtrd	|- ( ph -> ( E ` X ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
114	113	oveq1d	|- ( ph -> ( ( E ` X ) - T ) = ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - T ) )
115	13	recnd	|- ( ph -> X e. CC )
116	107	recnd	|- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
117	26	recnd	|- ( ph -> T e. CC )
118	115 116 117	addsubassd	|- ( ph -> ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - T ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - T ) ) )
119	105	zcnd	|- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
120	119 117	mulsubfacd	|- ( ph -> ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - T ) = ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) )
121	120	oveq2d	|- ( ph -> ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - T ) ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) )
122	114 118 121	3eqtrd	|- ( ph -> ( ( E ` X ) - T ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) )
123	122	adantr	|- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) )
124		oveq1	|- ( k = ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) -> ( k x. T ) = ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) )
125	124	oveq2d	|- ( k = ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) -> ( X + ( k x. T ) ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) )
126	125	eqeq2d	|- ( k = ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) -> ( ( ( E ` X ) - T ) = ( X + ( k x. T ) ) <-> ( ( E ` X ) - T ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) ) )
127	126	anbi2d	|- ( k = ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) -> ( ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) <-> ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) ) ) )
128	127	rspcev	|- ( ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) e. ZZ /\ ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) ) ) -> E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) )
129	35 93 123 128	syl12anc	|- ( ( ph /\ ( E ` X ) = B ) -> E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) )
130	75 77	oveq12d	|- ( i = 0 -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) )
131	130	eleq2d	|- ( i = 0 -> ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) ) )
132	131	anbi1d	|- ( i = 0 -> ( ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) <-> ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) )
133	132	rexbidv	|- ( i = 0 -> ( E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) <-> E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) )
134	133	rspcev	|- ( ( 0 e. ( 0 ..^ M ) /\ E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` 0 ) [,) ( Q ` ( 0 + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) -> E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) )
135	23 129 134	syl2anc	|- ( ( ph /\ ( E ` X ) = B ) -> E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) )
136		ovex	|- ( ( E ` X ) - T ) e. _V
137		eleq1	|- ( y = ( ( E ` X ) - T ) -> ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
138		eqeq1	|- ( y = ( ( E ` X ) - T ) -> ( y = ( X + ( k x. T ) ) <-> ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) )
139	137 138	anbi12d	|- ( y = ( ( E ` X ) - T ) -> ( ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) <-> ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) )
140	139	2rexbidv	|- ( y = ( ( E ` X ) - T ) -> ( E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) <-> E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) )
141	140	anbi2d	|- ( y = ( ( E ` X ) - T ) -> ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) <-> ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) ) )
142	141	imbi1d	|- ( y = ( ( E ` X ) - T ) -> ( ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) <-> ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) ) )
143		simpr	|- ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) )
144		nfv	|- F/ i ph
145		nfre1	|- F/ i E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) )
146	144 145	nfan	|- F/ i ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) )
147		nfv	|- F/ k ph
148		nfcv	|- F/_ k ( 0 ..^ M )
149		nfre1	|- F/ k E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) )
150	148 149	nfrex	|- F/ k E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) )
151	147 150	nfan	|- F/ k ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) )
152		simp1	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ph )
153		simp2l	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> i e. ( 0 ..^ M ) )
154		simp3l	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
155	152 153 154	jca31	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
156		simp2r	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> k e. ZZ )
157		simp3r	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> y = ( X + ( k x. T ) ) )
158	16	biimpi	|- ( ch -> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ y = ( X + ( k x. T ) ) ) )
159	158	simplld	|- ( ch -> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
160	159	simplld	|- ( ch -> ph )
161		frel	|- ( F : D --> RR -> Rel F )
162	160 8 161	3syl	|- ( ch -> Rel F )
163		resindm	|- ( Rel F -> ( F |` ( ( X (,) +oo ) i^i dom F ) ) = ( F |` ( X (,) +oo ) ) )
164	163	eqcomd	|- ( Rel F -> ( F |` ( X (,) +oo ) ) = ( F |` ( ( X (,) +oo ) i^i dom F ) ) )
165	162 164	syl	|- ( ch -> ( F |` ( X (,) +oo ) ) = ( F |` ( ( X (,) +oo ) i^i dom F ) ) )
166		fdm	|- ( F : D --> RR -> dom F = D )
167	160 8 166	3syl	|- ( ch -> dom F = D )
168	167	ineq2d	|- ( ch -> ( ( X (,) +oo ) i^i dom F ) = ( ( X (,) +oo ) i^i D ) )
169	168	reseq2d	|- ( ch -> ( F |` ( ( X (,) +oo ) i^i dom F ) ) = ( F |` ( ( X (,) +oo ) i^i D ) ) )
170	165 169	eqtrd	|- ( ch -> ( F |` ( X (,) +oo ) ) = ( F |` ( ( X (,) +oo ) i^i D ) ) )
171	170	oveq1d	|- ( ch -> ( ( F |` ( X (,) +oo ) ) limCC X ) = ( ( F |` ( ( X (,) +oo ) i^i D ) ) limCC X ) )
172	160 8	syl	|- ( ch -> F : D --> RR )
173		ax-resscn	|- RR C_ CC
174	173	a1i	|- ( ch -> RR C_ CC )
175	172 174	fssd	|- ( ch -> F : D --> CC )
176		inss2	|- ( ( X (,) +oo ) i^i D ) C_ D
177	176	a1i	|- ( ch -> ( ( X (,) +oo ) i^i D ) C_ D )
178	175 177	fssresd	|- ( ch -> ( F |` ( ( X (,) +oo ) i^i D ) ) : ( ( X (,) +oo ) i^i D ) --> CC )
179		pnfxr	|- +oo e. RR*
180	179	a1i	|- ( ch -> +oo e. RR* )
181	159	simplrd	|- ( ch -> i e. ( 0 ..^ M ) )
182	48	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
183		fzofzp1	|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
184	183	adantl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
185	182 184	ffvelrnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
186	160 181 185	syl2anc	|- ( ch -> ( Q ` ( i + 1 ) ) e. RR )
187	158	simplrd	|- ( ch -> k e. ZZ )
188	187	zred	|- ( ch -> k e. RR )
189	160 26	syl	|- ( ch -> T e. RR )
190	188 189	remulcld	|- ( ch -> ( k x. T ) e. RR )
191	186 190	resubcld	|- ( ch -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR )
192	191	rexrd	|- ( ch -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* )
193	191	ltpnfd	|- ( ch -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) < +oo )
194	192 180 193	xrltled	|- ( ch -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) <_ +oo )
195		iooss2	|- ( ( +oo e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) <_ +oo ) -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ ( X (,) +oo ) )
196	180 194 195	syl2anc	|- ( ch -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ ( X (,) +oo ) )
197	187	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> k e. ZZ )
198	197	zcnd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> k e. CC )
199	189	recnd	|- ( ch -> T e. CC )
200	199	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> T e. CC )
201	198 200	mulneg1d	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( -u k x. T ) = -u ( k x. T ) )
202	201	oveq2d	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) = ( ( w + ( k x. T ) ) + -u ( k x. T ) ) )
203		elioore	|- ( w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> w e. RR )
204	203	recnd	|- ( w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> w e. CC )
205	204	adantl	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w e. CC )
206	198 200	mulcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( k x. T ) e. CC )
207	205 206	addcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. CC )
208	207 206	negsubd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) + -u ( k x. T ) ) = ( ( w + ( k x. T ) ) - ( k x. T ) ) )
209	205 206	pncand	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) - ( k x. T ) ) = w )
210	202 208 209	3eqtrrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w = ( ( w + ( k x. T ) ) + ( -u k x. T ) ) )
211	160	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ph )
212	159	simpld	|- ( ch -> ( ph /\ i e. ( 0 ..^ M ) ) )
213		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 )
214		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 ) ) ) )
215	11 213 214	3syl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
216		ssdmres	|- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
217	215 216	sylibr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
218	8 166	syl	|- ( ph -> dom F = D )
219	218	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom F = D )
220	217 219	sseqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
221	212 220	syl	|- ( ch -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
222	221	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
223		elfzofz	|- ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
224	223	adantl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
225	182 224	ffvelrnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
226	160 181 225	syl2anc	|- ( ch -> ( Q ` i ) e. RR )
227	226	rexrd	|- ( ch -> ( Q ` i ) e. RR* )
228	227	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( Q ` i ) e. RR* )
229	186	rexrd	|- ( ch -> ( Q ` ( i + 1 ) ) e. RR* )
230	229	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
231	203	adantl	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w e. RR )
232	197	zred	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> k e. RR )
233	211 26	syl	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> T e. RR )
234	232 233	remulcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( k x. T ) e. RR )
235	231 234	readdcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. RR )
236	226	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( Q ` i ) e. RR )
237	160 13	syl	|- ( ch -> X e. RR )
238	237 190	readdcld	|- ( ch -> ( X + ( k x. T ) ) e. RR )
239	238	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( X + ( k x. T ) ) e. RR )
240	16	simprbi	|- ( ch -> y = ( X + ( k x. T ) ) )
241	240	eqcomd	|- ( ch -> ( X + ( k x. T ) ) = y )
242	159	simprd	|- ( ch -> y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
243	241 242	eqeltrd	|- ( ch -> ( X + ( k x. T ) ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
244		icogelb	|- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( X + ( k x. T ) ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ ( X + ( k x. T ) ) )
245	227 229 243 244	syl3anc	|- ( ch -> ( Q ` i ) <_ ( X + ( k x. T ) ) )
246	245	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( Q ` i ) <_ ( X + ( k x. T ) ) )
247	211 13	syl	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X e. RR )
248	247	rexrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X e. RR* )
249	186	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
250	249 234	resubcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR )
251	250	rexrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* )
252		simpr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
253		ioogtlb	|- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X < w )
254	248 251 252 253	syl3anc	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X < w )
255	247 231 234 254	ltadd1dd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( X + ( k x. T ) ) < ( w + ( k x. T ) ) )
256	236 239 235 246 255	lelttrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( Q ` i ) < ( w + ( k x. T ) ) )
257		iooltub	|- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
258	248 251 252 257	syl3anc	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
259	231 250 234 258	ltadd1dd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) < ( ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) + ( k x. T ) ) )
260	186	recnd	|- ( ch -> ( Q ` ( i + 1 ) ) e. CC )
261	190	recnd	|- ( ch -> ( k x. T ) e. CC )
262	260 261	npcand	|- ( ch -> ( ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) + ( k x. T ) ) = ( Q ` ( i + 1 ) ) )
263	262	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) + ( k x. T ) ) = ( Q ` ( i + 1 ) ) )
264	259 263	breqtrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) < ( Q ` ( i + 1 ) ) )
265	228 230 235 256 264	eliood	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
266	222 265	sseldd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. D )
267	197	znegcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> -u k e. ZZ )
268		ovex	|- ( w + ( k x. T ) ) e. _V
269		eleq1	|- ( x = ( w + ( k x. T ) ) -> ( x e. D <-> ( w + ( k x. T ) ) e. D ) )
270	269	3anbi2d	|- ( x = ( w + ( k x. T ) ) -> ( ( ph /\ x e. D /\ -u k e. ZZ ) <-> ( ph /\ ( w + ( k x. T ) ) e. D /\ -u k e. ZZ ) ) )
271		oveq1	|- ( x = ( w + ( k x. T ) ) -> ( x + ( -u k x. T ) ) = ( ( w + ( k x. T ) ) + ( -u k x. T ) ) )
272	271	eleq1d	|- ( x = ( w + ( k x. T ) ) -> ( ( x + ( -u k x. T ) ) e. D <-> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D ) )
273	270 272	imbi12d	|- ( x = ( w + ( k x. T ) ) -> ( ( ( ph /\ x e. D /\ -u k e. ZZ ) -> ( x + ( -u k x. T ) ) e. D ) <-> ( ( ph /\ ( w + ( k x. T ) ) e. D /\ -u k e. ZZ ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D ) ) )
274		negex	|- -u k e. _V
275		eleq1	|- ( j = -u k -> ( j e. ZZ <-> -u k e. ZZ ) )
276	275	3anbi3d	|- ( j = -u k -> ( ( ph /\ x e. D /\ j e. ZZ ) <-> ( ph /\ x e. D /\ -u k e. ZZ ) ) )
277		oveq1	|- ( j = -u k -> ( j x. T ) = ( -u k x. T ) )
278	277	oveq2d	|- ( j = -u k -> ( x + ( j x. T ) ) = ( x + ( -u k x. T ) ) )
279	278	eleq1d	|- ( j = -u k -> ( ( x + ( j x. T ) ) e. D <-> ( x + ( -u k x. T ) ) e. D ) )
280	276 279	imbi12d	|- ( j = -u k -> ( ( ( ph /\ x e. D /\ j e. ZZ ) -> ( x + ( j x. T ) ) e. D ) <-> ( ( ph /\ x e. D /\ -u k e. ZZ ) -> ( x + ( -u k x. T ) ) e. D ) ) )
281		eleq1	|- ( k = j -> ( k e. ZZ <-> j e. ZZ ) )
282	281	3anbi3d	|- ( k = j -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ j e. ZZ ) ) )
283		oveq1	|- ( k = j -> ( k x. T ) = ( j x. T ) )
284	283	oveq2d	|- ( k = j -> ( x + ( k x. T ) ) = ( x + ( j x. T ) ) )
285	284	eleq1d	|- ( k = j -> ( ( x + ( k x. T ) ) e. D <-> ( x + ( j x. T ) ) e. D ) )
286	282 285	imbi12d	|- ( k = j -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ x e. D /\ j e. ZZ ) -> ( x + ( j x. T ) ) e. D ) ) )
287	286 9	chvarvv	|- ( ( ph /\ x e. D /\ j e. ZZ ) -> ( x + ( j x. T ) ) e. D )
288	274 280 287	vtocl	|- ( ( ph /\ x e. D /\ -u k e. ZZ ) -> ( x + ( -u k x. T ) ) e. D )
289	268 273 288	vtocl	|- ( ( ph /\ ( w + ( k x. T ) ) e. D /\ -u k e. ZZ ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D )
290	211 266 267 289	syl3anc	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D )
291	210 290	eqeltrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w e. D )
292	291	ralrimiva	|- ( ch -> A. w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w e. D )
293		dfss3	|- ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ D <-> A. w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w e. D )
294	292 293	sylibr	|- ( ch -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ D )
295	196 294	ssind	|- ( ch -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ ( ( X (,) +oo ) i^i D ) )
296		ioosscn	|- ( X (,) +oo ) C_ CC
297		ssinss1	|- ( ( X (,) +oo ) C_ CC -> ( ( X (,) +oo ) i^i D ) C_ CC )
298	296 297	mp1i	|- ( ch -> ( ( X (,) +oo ) i^i D ) C_ CC )
299		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
300		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
301	237	rexrd	|- ( ch -> X e. RR* )
302	237	leidd	|- ( ch -> X <_ X )
303	240	oveq1d	|- ( ch -> ( y - ( k x. T ) ) = ( ( X + ( k x. T ) ) - ( k x. T ) ) )
304	237	recnd	|- ( ch -> X e. CC )
305	304 261	pncand	|- ( ch -> ( ( X + ( k x. T ) ) - ( k x. T ) ) = X )
306	303 305	eqtr2d	|- ( ch -> X = ( y - ( k x. T ) ) )
307		icossre	|- ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR* ) -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) C_ RR )
308	226 229 307	syl2anc	|- ( ch -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) C_ RR )
309	308 242	sseldd	|- ( ch -> y e. RR )
310		icoltub	|- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> y < ( Q ` ( i + 1 ) ) )
311	227 229 242 310	syl3anc	|- ( ch -> y < ( Q ` ( i + 1 ) ) )
312	309 186 190 311	ltsub1dd	|- ( ch -> ( y - ( k x. T ) ) < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
313	306 312	eqbrtrd	|- ( ch -> X < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
314	301 192 301 302 313	elicod	|- ( ch -> X e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
315		snunioo1	|- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* /\ X < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) u. { X } ) = ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
316	301 192 313 315	syl3anc	|- ( ch -> ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) u. { X } ) = ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
317	316	fveq2d	|- ( ch -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) ` ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) u. { X } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) ` ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) )
318	299	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
319		ovex	|- ( X (,) +oo ) e. _V
320	319	inex1	|- ( ( X (,) +oo ) i^i D ) e. _V
321		snex	|- { X } e. _V
322	320 321	unex	|- ( ( ( X (,) +oo ) i^i D ) u. { X } ) e. _V
323		resttop	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( ( X (,) +oo ) i^i D ) u. { X } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) e. Top )
324	318 322 323	mp2an	|- ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) e. Top
325	324	a1i	|- ( ch -> ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) e. Top )
326		retop	|- ( topGen ` ran (,) ) e. Top
327	326	a1i	|- ( ch -> ( topGen ` ran (,) ) e. Top )
328	322	a1i	|- ( ch -> ( ( ( X (,) +oo ) i^i D ) u. { X } ) e. _V )
329		iooretop	|- ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) e. ( topGen ` ran (,) )
330	329	a1i	|- ( ch -> ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) e. ( topGen ` ran (,) ) )
331		elrestr	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( X (,) +oo ) i^i D ) u. { X } ) e. _V /\ ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) e. ( topGen ` ran (,) ) ) -> ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
332	327 328 330 331	syl3anc	|- ( ch -> ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
333		mnfxr	|- -oo e. RR*
334	333	a1i	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> -oo e. RR* )
335	192	adantr	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* )
336		icossre	|- ( ( X e. RR /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* ) -> ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ RR )
337	237 192 336	syl2anc	|- ( ch -> ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ RR )
338	337	sselda	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. RR )
339	338	mnfltd	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> -oo < x )
340	301	adantr	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X e. RR* )
341		simpr	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
342		icoltub	|- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
343	340 335 341 342	syl3anc	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
344	334 335 338 339 343	eliood	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
345		vsnid	|- x e. { x }
346	345	a1i	|- ( x = X -> x e. { x } )
347		sneq	|- ( x = X -> { x } = { X } )
348	346 347	eleqtrd	|- ( x = X -> x e. { X } )
349		elun2	|- ( x e. { X } -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
350	348 349	syl	|- ( x = X -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
351	350	adantl	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ x = X ) -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
352	301	ad2antrr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> X e. RR* )
353	179	a1i	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> +oo e. RR* )
354	338	adantr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x e. RR )
355	237	ad2antrr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> X e. RR )
356		icogelb	|- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X <_ x )
357	340 335 341 356	syl3anc	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> X <_ x )
358	357	adantr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> X <_ x )
359		neqne	|- ( -. x = X -> x =/= X )
360	359	adantl	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x =/= X )
361	355 354 358 360	leneltd	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> X < x )
362	354	ltpnfd	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x < +oo )
363	352 353 354 361 362	eliood	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x e. ( X (,) +oo ) )
364	187	zcnd	|- ( ch -> k e. CC )
365	364 199	mulneg1d	|- ( ch -> ( -u k x. T ) = -u ( k x. T ) )
366	365	oveq2d	|- ( ch -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) = ( ( w + ( k x. T ) ) + -u ( k x. T ) ) )
367	366	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) = ( ( w + ( k x. T ) ) + -u ( k x. T ) ) )
368		ioosscn	|- ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ CC
369	368	sseli	|- ( w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> w e. CC )
370	369	adantl	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w e. CC )
371	261	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( k x. T ) e. CC )
372	370 371	addcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. CC )
373	372 371	negsubd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) + -u ( k x. T ) ) = ( ( w + ( k x. T ) ) - ( k x. T ) ) )
374	370 371	pncand	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) - ( k x. T ) ) = w )
375	367 373 374	3eqtrrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w = ( ( w + ( k x. T ) ) + ( -u k x. T ) ) )
376	190	adantr	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( k x. T ) e. RR )
377	231 376	readdcld	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. RR )
378	228 230 377 256 264	eliood	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
379	222 378	sseldd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. D )
380	275	3anbi3d	|- ( j = -u k -> ( ( ph /\ ( w + ( k x. T ) ) e. D /\ j e. ZZ ) <-> ( ph /\ ( w + ( k x. T ) ) e. D /\ -u k e. ZZ ) ) )
381	277	oveq2d	|- ( j = -u k -> ( ( w + ( k x. T ) ) + ( j x. T ) ) = ( ( w + ( k x. T ) ) + ( -u k x. T ) ) )
382	381	eleq1d	|- ( j = -u k -> ( ( ( w + ( k x. T ) ) + ( j x. T ) ) e. D <-> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D ) )
383	380 382	imbi12d	|- ( j = -u k -> ( ( ( ph /\ ( w + ( k x. T ) ) e. D /\ j e. ZZ ) -> ( ( w + ( k x. T ) ) + ( j x. T ) ) e. D ) <-> ( ( ph /\ ( w + ( k x. T ) ) e. D /\ -u k e. ZZ ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D ) ) )
384	269	3anbi2d	|- ( x = ( w + ( k x. T ) ) -> ( ( ph /\ x e. D /\ j e. ZZ ) <-> ( ph /\ ( w + ( k x. T ) ) e. D /\ j e. ZZ ) ) )
385		oveq1	|- ( x = ( w + ( k x. T ) ) -> ( x + ( j x. T ) ) = ( ( w + ( k x. T ) ) + ( j x. T ) ) )
386	385	eleq1d	|- ( x = ( w + ( k x. T ) ) -> ( ( x + ( j x. T ) ) e. D <-> ( ( w + ( k x. T ) ) + ( j x. T ) ) e. D ) )
387	384 386	imbi12d	|- ( x = ( w + ( k x. T ) ) -> ( ( ( ph /\ x e. D /\ j e. ZZ ) -> ( x + ( j x. T ) ) e. D ) <-> ( ( ph /\ ( w + ( k x. T ) ) e. D /\ j e. ZZ ) -> ( ( w + ( k x. T ) ) + ( j x. T ) ) e. D ) ) )
388	268 387 287	vtocl	|- ( ( ph /\ ( w + ( k x. T ) ) e. D /\ j e. ZZ ) -> ( ( w + ( k x. T ) ) + ( j x. T ) ) e. D )
389	274 383 388	vtocl	|- ( ( ph /\ ( w + ( k x. T ) ) e. D /\ -u k e. ZZ ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D )
390	211 379 267 389	syl3anc	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( w + ( k x. T ) ) + ( -u k x. T ) ) e. D )
391	375 390	eqeltrd	|- ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> w e. D )
392	391	ralrimiva	|- ( ch -> A. w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w e. D )
393	392 293	sylibr	|- ( ch -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ D )
394	393	ad2antrr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ D )
395	192	ad2antrr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* )
396	343	adantr	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
397	352 395 354 361 396	eliood	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
398	394 397	sseldd	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x e. D )
399	363 398	elind	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x e. ( ( X (,) +oo ) i^i D ) )
400		elun1	|- ( x e. ( ( X (,) +oo ) i^i D ) -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
401	399 400	syl	|- ( ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) /\ -. x = X ) -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
402	351 401	pm2.61dan	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
403	344 402	elind	|- ( ( ch /\ x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
404	301	adantr	|- ( ( ch /\ x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> X e. RR* )
405	192	adantr	|- ( ( ch /\ x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* )
406		elinel1	|- ( x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) -> x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
407		elioore	|- ( x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> x e. RR )
408	406 407	syl	|- ( x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) -> x e. RR )
409	408	rexrd	|- ( x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) -> x e. RR* )
410	409	adantl	|- ( ( ch /\ x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> x e. RR* )
411		elinel2	|- ( x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
412	237	adantr	|- ( ( ch /\ x = X ) -> X e. RR )
413	95	eqcomd	|- ( x = X -> X = x )
414	413	adantl	|- ( ( ch /\ x = X ) -> X = x )
415	412 414	eqled	|- ( ( ch /\ x = X ) -> X <_ x )
416	415	adantlr	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ x = X ) -> X <_ x )
417		simpll	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ -. x = X ) -> ch )
418		simplr	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ -. x = X ) -> x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) )
419		id	|- ( -. x = X -> -. x = X )
420		velsn	|- ( x e. { X } <-> x = X )
421	419 420	sylnibr	|- ( -. x = X -> -. x e. { X } )
422	421	adantl	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ -. x = X ) -> -. x e. { X } )
423		elunnel2	|- ( ( x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) /\ -. x e. { X } ) -> x e. ( ( X (,) +oo ) i^i D ) )
424	418 422 423	syl2anc	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ -. x = X ) -> x e. ( ( X (,) +oo ) i^i D ) )
425		elinel1	|- ( x e. ( ( X (,) +oo ) i^i D ) -> x e. ( X (,) +oo ) )
426	424 425	syl	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ -. x = X ) -> x e. ( X (,) +oo ) )
427	237	adantr	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> X e. RR )
428		elioore	|- ( x e. ( X (,) +oo ) -> x e. RR )
429	428	adantl	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> x e. RR )
430	301	adantr	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> X e. RR* )
431	179	a1i	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> +oo e. RR* )
432		simpr	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> x e. ( X (,) +oo ) )
433		ioogtlb	|- ( ( X e. RR* /\ +oo e. RR* /\ x e. ( X (,) +oo ) ) -> X < x )
434	430 431 432 433	syl3anc	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> X < x )
435	427 429 434	ltled	|- ( ( ch /\ x e. ( X (,) +oo ) ) -> X <_ x )
436	417 426 435	syl2anc	|- ( ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) /\ -. x = X ) -> X <_ x )
437	416 436	pm2.61dan	|- ( ( ch /\ x e. ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) -> X <_ x )
438	411 437	sylan2	|- ( ( ch /\ x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> X <_ x )
439	333	a1i	|- ( ( ch /\ x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> -oo e. RR* )
440	192	adantr	|- ( ( ch /\ x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* )
441		simpr	|- ( ( ch /\ x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
442		iooltub	|- ( ( -oo e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) e. RR* /\ x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
443	439 440 441 442	syl3anc	|- ( ( ch /\ x e. ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
444	406 443	sylan2	|- ( ( ch /\ x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> x < ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
445	404 405 410 438 444	elicod	|- ( ( ch /\ x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
446	403 445	impbida	|- ( ch -> ( x e. ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) <-> x e. ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) )
447	446	eqrdv	|- ( ch -> ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) = ( ( -oo (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) i^i ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
448		ioossre	|- ( X (,) +oo ) C_ RR
449		ssinss1	|- ( ( X (,) +oo ) C_ RR -> ( ( X (,) +oo ) i^i D ) C_ RR )
450	448 449	mp1i	|- ( ch -> ( ( X (,) +oo ) i^i D ) C_ RR )
451	237	snssd	|- ( ch -> { X } C_ RR )
452	450 451	unssd	|- ( ch -> ( ( ( X (,) +oo ) i^i D ) u. { X } ) C_ RR )
453		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
454	299 453	rerest	|- ( ( ( ( X (,) +oo ) i^i D ) u. { X } ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
455	452 454	syl	|- ( ch -> ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
456	332 447 455	3eltr4d	|- ( ch -> ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) )
457		isopn3i	|- ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) e. Top /\ ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) e. ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) ` ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) = ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
458	325 456 457	syl2anc	|- ( ch -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) ` ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) = ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
459	317 458	eqtr2d	|- ( ch -> ( X [,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) ` ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) u. { X } ) ) )
460	314 459	eleqtrd	|- ( ch -> X e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( ( X (,) +oo ) i^i D ) u. { X } ) ) ) ` ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) u. { X } ) ) )
461	178 295 298 299 300 460	limcres	|- ( ch -> ( ( ( F |` ( ( X (,) +oo ) i^i D ) ) |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) = ( ( F |` ( ( X (,) +oo ) i^i D ) ) limCC X ) )
462	295	resabs1d	|- ( ch -> ( ( F |` ( ( X (,) +oo ) i^i D ) ) |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) = ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) )
463	462	oveq1d	|- ( ch -> ( ( ( F |` ( ( X (,) +oo ) i^i D ) ) |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) = ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) )
464	173	a1i	|- ( ph -> RR C_ CC )
465	8 464	fssd	|- ( ph -> F : D --> CC )
466	218	feq2d	|- ( ph -> ( F : dom F --> CC <-> F : D --> CC ) )
467	465 466	mpbird	|- ( ph -> F : dom F --> CC )
468	160 467	syl	|- ( ch -> F : dom F --> CC )
469	468	adantr	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> F : dom F --> CC )
470	368	a1i	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ CC )
471	393 167	sseqtrrd	|- ( ch -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ dom F )
472	471	adantr	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) C_ dom F )
473	261	adantr	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> ( k x. T ) e. CC )
474		eqid	|- { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } = { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) }
475		eqeq1	|- ( z = w -> ( z = ( x + ( k x. T ) ) <-> w = ( x + ( k x. T ) ) ) )
476	475	rexbidv	|- ( z = w -> ( E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) <-> E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w = ( x + ( k x. T ) ) ) )
477	476	elrab	|- ( w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } <-> ( w e. CC /\ E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w = ( x + ( k x. T ) ) ) )
478	477	simprbi	|- ( w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } -> E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w = ( x + ( k x. T ) ) )
479	478	adantl	|- ( ( ch /\ w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) -> E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w = ( x + ( k x. T ) ) )
480		nfv	|- F/ x ch
481		nfre1	|- F/ x E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) )
482		nfcv	|- F/_ x CC
483	481 482	nfrabw	|- F/_ x { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) }
484	483	nfcri	|- F/ x w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) }
485	480 484	nfan	|- F/ x ( ch /\ w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } )
486		nfv	|- F/ x w e. D
487		simp3	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) /\ w = ( x + ( k x. T ) ) ) -> w = ( x + ( k x. T ) ) )
488		eleq1	|- ( w = x -> ( w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) <-> x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) )
489	488	anbi2d	|- ( w = x -> ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) <-> ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) ) )
490		oveq1	|- ( w = x -> ( w + ( k x. T ) ) = ( x + ( k x. T ) ) )
491	490	eleq1d	|- ( w = x -> ( ( w + ( k x. T ) ) e. D <-> ( x + ( k x. T ) ) e. D ) )
492	489 491	imbi12d	|- ( w = x -> ( ( ( ch /\ w e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( w + ( k x. T ) ) e. D ) <-> ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( x + ( k x. T ) ) e. D ) ) )
493	492 266	chvarvv	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( x + ( k x. T ) ) e. D )
494	493	3adant3	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) /\ w = ( x + ( k x. T ) ) ) -> ( x + ( k x. T ) ) e. D )
495	487 494	eqeltrd	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) /\ w = ( x + ( k x. T ) ) ) -> w e. D )
496	495	3exp	|- ( ch -> ( x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> ( w = ( x + ( k x. T ) ) -> w e. D ) ) )
497	496	adantr	|- ( ( ch /\ w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) -> ( x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) -> ( w = ( x + ( k x. T ) ) -> w e. D ) ) )
498	485 486 497	rexlimd	|- ( ( ch /\ w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) -> ( E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) w = ( x + ( k x. T ) ) -> w e. D ) )
499	479 498	mpd	|- ( ( ch /\ w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) -> w e. D )
500	499	ralrimiva	|- ( ch -> A. w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } w e. D )
501		dfss3	|- ( { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } C_ D <-> A. w e. { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } w e. D )
502	500 501	sylibr	|- ( ch -> { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } C_ D )
503	502 167	sseqtrrd	|- ( ch -> { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } C_ dom F )
504	503	adantr	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } C_ dom F )
505	160	adantr	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ph )
506	393	sselda	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> x e. D )
507	187	adantr	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> k e. ZZ )
508	505 506 507 10	syl3anc	|- ( ( ch /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
509	508	adantlr	|- ( ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) /\ x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
510		simpr	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) )
511	469 470 472 473 474 504 509 510	limcperiod	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> w e. ( ( F |` { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) limCC ( X + ( k x. T ) ) ) )
512	262	eqcomd	|- ( ch -> ( Q ` ( i + 1 ) ) = ( ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) + ( k x. T ) ) )
513	240 512	oveq12d	|- ( ch -> ( y (,) ( Q ` ( i + 1 ) ) ) = ( ( X + ( k x. T ) ) (,) ( ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) + ( k x. T ) ) ) )
514	237 191 190	iooshift	|- ( ch -> ( ( X + ( k x. T ) ) (,) ( ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) + ( k x. T ) ) ) = { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } )
515	513 514	eqtr2d	|- ( ch -> { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } = ( y (,) ( Q ` ( i + 1 ) ) ) )
516	515	reseq2d	|- ( ch -> ( F |` { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) = ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) )
517	516 241	oveq12d	|- ( ch -> ( ( F |` { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) limCC ( X + ( k x. T ) ) ) = ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
518	517	adantr	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> ( ( F |` { z e. CC | E. x e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) z = ( x + ( k x. T ) ) } ) limCC ( X + ( k x. T ) ) ) = ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
519	511 518	eleqtrd	|- ( ( ch /\ w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) ) -> w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
520	468	adantr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> F : dom F --> CC )
521		ioosscn	|- ( y (,) ( Q ` ( i + 1 ) ) ) C_ CC
522	521	a1i	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> ( y (,) ( Q ` ( i + 1 ) ) ) C_ CC )
523		icogelb	|- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ y )
524	227 229 242 523	syl3anc	|- ( ch -> ( Q ` i ) <_ y )
525		iooss1	|- ( ( ( Q ` i ) e. RR* /\ ( Q ` i ) <_ y ) -> ( y (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
526	227 524 525	syl2anc	|- ( ch -> ( y (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
527	526 221	sstrd	|- ( ch -> ( y (,) ( Q ` ( i + 1 ) ) ) C_ D )
528	527 167	sseqtrrd	|- ( ch -> ( y (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
529	528	adantr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> ( y (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
530	364	negcld	|- ( ch -> -u k e. CC )
531	530 199	mulcld	|- ( ch -> ( -u k x. T ) e. CC )
532	531	adantr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> ( -u k x. T ) e. CC )
533		eqid	|- { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } = { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) }
534		eqeq1	|- ( z = w -> ( z = ( x + ( -u k x. T ) ) <-> w = ( x + ( -u k x. T ) ) ) )
535	534	rexbidv	|- ( z = w -> ( E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) <-> E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) w = ( x + ( -u k x. T ) ) ) )
536	535	elrab	|- ( w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } <-> ( w e. CC /\ E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) w = ( x + ( -u k x. T ) ) ) )
537	536	simprbi	|- ( w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } -> E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) w = ( x + ( -u k x. T ) ) )
538	537	adantl	|- ( ( ch /\ w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) -> E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) w = ( x + ( -u k x. T ) ) )
539		nfre1	|- F/ x E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) )
540	539 482	nfrabw	|- F/_ x { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) }
541	540	nfcri	|- F/ x w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) }
542	480 541	nfan	|- F/ x ( ch /\ w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } )
543		simp3	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) /\ w = ( x + ( -u k x. T ) ) ) -> w = ( x + ( -u k x. T ) ) )
544	160	adantr	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
545	527	sselda	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> x e. D )
546	187	adantr	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> k e. ZZ )
547	546	znegcld	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> -u k e. ZZ )
548	544 545 547 288	syl3anc	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> ( x + ( -u k x. T ) ) e. D )
549	548	3adant3	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) /\ w = ( x + ( -u k x. T ) ) ) -> ( x + ( -u k x. T ) ) e. D )
550	543 549	eqeltrd	|- ( ( ch /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) /\ w = ( x + ( -u k x. T ) ) ) -> w e. D )
551	550	3exp	|- ( ch -> ( x e. ( y (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( x + ( -u k x. T ) ) -> w e. D ) ) )
552	551	adantr	|- ( ( ch /\ w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) -> ( x e. ( y (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( x + ( -u k x. T ) ) -> w e. D ) ) )
553	542 486 552	rexlimd	|- ( ( ch /\ w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) -> ( E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) w = ( x + ( -u k x. T ) ) -> w e. D ) )
554	538 553	mpd	|- ( ( ch /\ w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) -> w e. D )
555	554	ralrimiva	|- ( ch -> A. w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } w e. D )
556		dfss3	|- ( { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } C_ D <-> A. w e. { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } w e. D )
557	555 556	sylibr	|- ( ch -> { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } C_ D )
558	557 167	sseqtrrd	|- ( ch -> { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } C_ dom F )
559	558	adantr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } C_ dom F )
560	160	ad2antrr	|- ( ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
561	545	adantlr	|- ( ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> x e. D )
562	547	adantlr	|- ( ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> -u k e. ZZ )
563	278	fveq2d	|- ( j = -u k -> ( F ` ( x + ( j x. T ) ) ) = ( F ` ( x + ( -u k x. T ) ) ) )
564	563	eqeq1d	|- ( j = -u k -> ( ( F ` ( x + ( j x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( -u k x. T ) ) ) = ( F ` x ) ) )
565	276 564	imbi12d	|- ( j = -u k -> ( ( ( ph /\ x e. D /\ j e. ZZ ) -> ( F ` ( x + ( j x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ -u k e. ZZ ) -> ( F ` ( x + ( -u k x. T ) ) ) = ( F ` x ) ) ) )
566	284	fveq2d	|- ( k = j -> ( F ` ( x + ( k x. T ) ) ) = ( F ` ( x + ( j x. T ) ) ) )
567	566	eqeq1d	|- ( k = j -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( j x. T ) ) ) = ( F ` x ) ) )
568	282 567	imbi12d	|- ( k = j -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ j e. ZZ ) -> ( F ` ( x + ( j x. T ) ) ) = ( F ` x ) ) ) )
569	568 10	chvarvv	|- ( ( ph /\ x e. D /\ j e. ZZ ) -> ( F ` ( x + ( j x. T ) ) ) = ( F ` x ) )
570	274 565 569	vtocl	|- ( ( ph /\ x e. D /\ -u k e. ZZ ) -> ( F ` ( x + ( -u k x. T ) ) ) = ( F ` x ) )
571	560 561 562 570	syl3anc	|- ( ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) /\ x e. ( y (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( x + ( -u k x. T ) ) ) = ( F ` x ) )
572		simpr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
573	520 522 529 532 533 559 571 572	limcperiod	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> w e. ( ( F |` { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) limCC ( y + ( -u k x. T ) ) ) )
574	365	oveq2d	|- ( ch -> ( y + ( -u k x. T ) ) = ( y + -u ( k x. T ) ) )
575	309	recnd	|- ( ch -> y e. CC )
576	575 261	negsubd	|- ( ch -> ( y + -u ( k x. T ) ) = ( y - ( k x. T ) ) )
577	306	eqcomd	|- ( ch -> ( y - ( k x. T ) ) = X )
578	574 576 577	3eqtrd	|- ( ch -> ( y + ( -u k x. T ) ) = X )
579	578	eqcomd	|- ( ch -> X = ( y + ( -u k x. T ) ) )
580	365	oveq2d	|- ( ch -> ( ( Q ` ( i + 1 ) ) + ( -u k x. T ) ) = ( ( Q ` ( i + 1 ) ) + -u ( k x. T ) ) )
581	260 261	negsubd	|- ( ch -> ( ( Q ` ( i + 1 ) ) + -u ( k x. T ) ) = ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) )
582	580 581	eqtr2d	|- ( ch -> ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) = ( ( Q ` ( i + 1 ) ) + ( -u k x. T ) ) )
583	579 582	oveq12d	|- ( ch -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) = ( ( y + ( -u k x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( -u k x. T ) ) ) )
584	188	renegcld	|- ( ch -> -u k e. RR )
585	584 189	remulcld	|- ( ch -> ( -u k x. T ) e. RR )
586	309 186 585	iooshift	|- ( ch -> ( ( y + ( -u k x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( -u k x. T ) ) ) = { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } )
587	583 586	eqtr2d	|- ( ch -> { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } = ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
588	587	adantr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } = ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) )
589	588	reseq2d	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> ( F |` { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) = ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) )
590	578	adantr	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> ( y + ( -u k x. T ) ) = X )
591	589 590	oveq12d	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> ( ( F |` { z e. CC | E. x e. ( y (,) ( Q ` ( i + 1 ) ) ) z = ( x + ( -u k x. T ) ) } ) limCC ( y + ( -u k x. T ) ) ) = ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) )
592	573 591	eleqtrd	|- ( ( ch /\ w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) -> w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) )
593	519 592	impbida	|- ( ch -> ( w e. ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) <-> w e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) ) )
594	593	eqrdv	|- ( ch -> ( ( F |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) = ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
595	463 594	eqtrd	|- ( ch -> ( ( ( F |` ( ( X (,) +oo ) i^i D ) ) |` ( X (,) ( ( Q ` ( i + 1 ) ) - ( k x. T ) ) ) ) limCC X ) = ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
596	171 461 595	3eqtr2d	|- ( ch -> ( ( F |` ( X (,) +oo ) ) limCC X ) = ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
597	160 181 81	syl2anc	|- ( ch -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
598	160 181 11	syl2anc	|- ( ch -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
599	160 181 12	syl2anc	|- ( ch -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
600		eqid	|- if ( y = ( Q ` i ) , R , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` y ) ) = if ( y = ( Q ` i ) , R , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` y ) )
601		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
602	226 186 597 598 599 309 186 311 526 600 601	fourierdlem32	|- ( ch -> if ( y = ( Q ` i ) , R , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` y ) ) e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
603	526	resabs1d	|- ( ch -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( y (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) )
604	603	oveq1d	|- ( ch -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) = ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
605	602 604	eleqtrd	|- ( ch -> if ( y = ( Q ` i ) , R , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` y ) ) e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) )
606		ne0i	|- ( if ( y = ( Q ` i ) , R , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` y ) ) e. ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) -> ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) =/= (/) )
607	605 606	syl	|- ( ch -> ( ( F |` ( y (,) ( Q ` ( i + 1 ) ) ) ) limCC y ) =/= (/) )
608	596 607	eqnetrd	|- ( ch -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
609	16 608	sylbir	|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ y = ( X + ( k x. T ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
610	155 156 157 609	syl21anc	|- ( ( ph /\ ( i e. ( 0 ..^ M ) /\ k e. ZZ ) /\ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
611	610	3exp	|- ( ph -> ( ( i e. ( 0 ..^ M ) /\ k e. ZZ ) -> ( ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) ) )
612	611	adantr	|- ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( ( i e. ( 0 ..^ M ) /\ k e. ZZ ) -> ( ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) ) )
613	146 151 612	rexlim2d	|- ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )
614	143 613	mpd	|- ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
615	136 142 614	vtocl	|- ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( ( E ` X ) - T ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( ( E ` X ) - T ) = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
616	17 135 615	syl2anc	|- ( ( ph /\ ( E ` X ) = B ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
617		iocssre	|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
618	66 2 617	syl2anc	|- ( ph -> ( A (,] B ) C_ RR )
619		ovex	|- ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
620	14	fvmpt2	|- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
621	619 620	mpan2	|- ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
622	621	oveq2d	|- ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
623	622	mpteq2ia	|- ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
624	15 623	eqtri	|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
625	1 2 3 5 624	fourierdlem4	|- ( ph -> E : RR --> ( A (,] B ) )
626	625 13	ffvelrnd	|- ( ph -> ( E ` X ) e. ( A (,] B ) )
627	618 626	sseldd	|- ( ph -> ( E ` X ) e. RR )
628	627	adantr	|- ( ( ph /\ ( E ` X ) =/= B ) -> ( E ` X ) e. RR )
629		simpl	|- ( ( ph /\ ( E ` X ) =/= B ) -> ph )
630		simpr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
631		ffn	|- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
632	48 631	syl	|- ( ph -> Q Fn ( 0 ... M ) )
633	632	ad2antrr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
634		fvelrnb	|- ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
635	633 634	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 ) ) )
636	630 635	mpbid	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
637		1zzd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
638		elfzelz	|- ( j e. ( 0 ... M ) -> j e. ZZ )
639	638	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
640	639	zred	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
641		elfzle1	|- ( j e. ( 0 ... M ) -> 0 <_ j )
642	641	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ j )
643		id	|- ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
644	643	eqcomd	|- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
645	644	ad2antlr	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
646		fveq2	|- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
647	646	adantl	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
648	45	simprld	|- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
649	648	simpld	|- ( ph -> ( Q ` 0 ) = A )
650	649	ad2antrr	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
651	645 647 650	3eqtrd	|- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
652	651	adantllr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
653	652	adantllr	|- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
654	1	adantr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
655	66	adantr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
656	2	rexrd	|- ( ph -> B e. RR* )
657	656	adantr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
658		simpr	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
659		iocgtlb	|- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
660	655 657 658 659	syl3anc	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
661	654 660	gtned	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
662	661	neneqd	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
663	662	ad3antrrr	|- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> -. ( E ` X ) = A )
664	653 663	pm2.65da	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
665	664	neqned	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
666	640 642 665	ne0gt0d	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
667		0zd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
668		zltp1le	|- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
669	667 639 668	syl2anc	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
670	666 669	mpbid	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
671	85 670	eqbrtrid	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
672		eluz2	|- ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
673	637 639 671 672	syl3anbrc	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( ZZ>= ` 1 ) )
674		nnuz	|- NN = ( ZZ>= ` 1 )
675	673 674	eleqtrrdi	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
676		nnm1nn0	|- ( j e. NN -> ( j - 1 ) e. NN0 )
677	675 676	syl	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. NN0 )
678	677 50	eleqtrdi	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
679	19	ad3antrrr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
680		peano2zm	|- ( j e. ZZ -> ( j - 1 ) e. ZZ )
681	638 680	syl	|- ( j e. ( 0 ... M ) -> ( j - 1 ) e. ZZ )
682	681	zred	|- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
683	638	zred	|- ( j e. ( 0 ... M ) -> j e. RR )
684		elfzel2	|- ( j e. ( 0 ... M ) -> M e. ZZ )
685	684	zred	|- ( j e. ( 0 ... M ) -> M e. RR )
686	683	ltm1d	|- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
687		elfzle2	|- ( j e. ( 0 ... M ) -> j <_ M )
688	682 683 685 686 687	ltletrd	|- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
689	688	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
690		elfzo2	|- ( ( j - 1 ) e. ( 0 ..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
691	678 679 689 690	syl3anbrc	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ..^ M ) )
692	48	ad3antrrr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
693	639 680	syl	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
694	667 679 693	3jca	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) )
695	677	nn0ge0d	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
696	682 685 688	ltled	|- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
697	696	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
698	694 695 697	jca32	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
699		elfz2	|- ( ( j - 1 ) e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
700	698 699	sylibr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
701	692 700	ffvelrnd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
702	701	rexrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
703	48	ffvelrnda	|- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
704	703	rexrd	|- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
705	704	adantlr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
706	705	adantr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
707	618	sselda	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
708	707	rexrd	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
709	708	ad2antrr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
710		simplll	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
711		ovex	|- ( j - 1 ) e. _V
712		eleq1	|- ( i = ( j - 1 ) -> ( i e. ( 0 ..^ M ) <-> ( j - 1 ) e. ( 0 ..^ M ) ) )
713	712	anbi2d	|- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) ) )
714		fveq2	|- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
715		oveq1	|- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
716	715	fveq2d	|- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
717	714 716	breq12d	|- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
718	713 717	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 ) ) ) ) )
719	711 718 81	vtocl	|- ( ( ph /\ ( j - 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
720	710 691 719	syl2anc	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
721	638	zcnd	|- ( j e. ( 0 ... M ) -> j e. CC )
722		1cnd	|- ( j e. ( 0 ... M ) -> 1 e. CC )
723	721 722	npcand	|- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
724	723	eqcomd	|- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
725	724	fveq2d	|- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
726	725	eqcomd	|- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
727	726	ad2antlr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
728	720 727	breqtrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
729		simpr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
730	728 729	breqtrd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
731	627	leidd	|- ( ph -> ( E ` X ) <_ ( E ` X ) )
732	731	ad2antrr	|- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
733	644	adantl	|- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
734	732 733	breqtrd	|- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
735	734	adantllr	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
736	702 706 709 730 735	eliocd	|- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) )
737	725	oveq2d	|- ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
738	737	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 ) ) ) )
739	736 738	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 ) ) ) )
740	714 716	oveq12d	|- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
741	740	eleq2d	|- ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
742	741	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 ) ) ) )
743	691 739 742	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 ) ) ) )
744	743	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 ) ) ) ) )
745	744	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 ) ) ) ) )
746	745	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 ) ) ) ) )
747	636 746	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 ) ) ) )
748	6	ad2antrr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
749	48	ad2antrr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
750		iocssicc	|- ( A (,] B ) C_ ( A [,] B )
751	649	eqcomd	|- ( ph -> A = ( Q ` 0 ) )
752	648	simprd	|- ( ph -> ( Q ` M ) = B )
753	752	eqcomd	|- ( ph -> B = ( Q ` M ) )
754	751 753	oveq12d	|- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
755	750 754	sseqtrid	|- ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
756	755	sselda	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
757	756	adantr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
758		simpr	|- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
759		fveq2	|- ( k = j -> ( Q ` k ) = ( Q ` j ) )
760	759	breq1d	|- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
761	760	cbvrabv	|- { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) }
762	761	supeq1i	|- sup ( { k e. ( 0 ..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
763	748 749 757 758 762	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 ) ) ) )
764		ioossioc	|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
765	764	sseli	|- ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
766	765	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 ) ) ) ) )
767	766	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 ) ) ) ) )
768	763 767	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 ) ) ) )
769	747 768	pm2.61dan	|- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
770	626 769	mpdan	|- ( ph -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
771		fveq2	|- ( i = j -> ( Q ` i ) = ( Q ` j ) )
772		oveq1	|- ( i = j -> ( i + 1 ) = ( j + 1 ) )
773	772	fveq2d	|- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
774	771 773	oveq12d	|- ( i = j -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) )
775	774	eleq2d	|- ( i = j -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) )
776	775	cbvrexvw	|- ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> E. j e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) )
777	770 776	sylib	|- ( ph -> E. j e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) )
778	777	adantr	|- ( ( ph /\ ( E ` X ) =/= B ) -> E. j e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) )
779		elfzonn0	|- ( j e. ( 0 ..^ M ) -> j e. NN0 )
780		1nn0	|- 1 e. NN0
781	780	a1i	|- ( j e. ( 0 ..^ M ) -> 1 e. NN0 )
782	779 781	nn0addcld	|- ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. NN0 )
783	782 50	eleqtrdi	|- ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( ZZ>= ` 0 ) )
784	783	adantr	|- ( ( j e. ( 0 ..^ M ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) e. ( ZZ>= ` 0 ) )
785	784	3ad2antl2	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) e. ( ZZ>= ` 0 ) )
786	19	ad2antrr	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> M e. ZZ )
787	786	3ad2antl1	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> M e. ZZ )
788	779	nn0red	|- ( j e. ( 0 ..^ M ) -> j e. RR )
789	788	adantr	|- ( ( j e. ( 0 ..^ M ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> j e. RR )
790	789	3ad2antl2	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> j e. RR )
791		1red	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> 1 e. RR )
792	790 791	readdcld	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) e. RR )
793	787	zred	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> M e. RR )
794		elfzop1le2	|- ( j e. ( 0 ..^ M ) -> ( j + 1 ) <_ M )
795	794	adantr	|- ( ( j e. ( 0 ..^ M ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) <_ M )
796	795	3ad2antl2	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) <_ M )
797		simplr	|- ( ( ( ph /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> ( E ` X ) = ( Q ` ( j + 1 ) ) )
798		fveq2	|- ( M = ( j + 1 ) -> ( Q ` M ) = ( Q ` ( j + 1 ) ) )
799	798	eqcomd	|- ( M = ( j + 1 ) -> ( Q ` ( j + 1 ) ) = ( Q ` M ) )
800	799	adantl	|- ( ( ( ph /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> ( Q ` ( j + 1 ) ) = ( Q ` M ) )
801	752	ad2antrr	|- ( ( ( ph /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> ( Q ` M ) = B )
802	797 800 801	3eqtrd	|- ( ( ( ph /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> ( E ` X ) = B )
803	802	adantllr	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> ( E ` X ) = B )
804		simpllr	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> ( E ` X ) =/= B )
805	804	neneqd	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) /\ M = ( j + 1 ) ) -> -. ( E ` X ) = B )
806	803 805	pm2.65da	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> -. M = ( j + 1 ) )
807	806	neqned	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> M =/= ( j + 1 ) )
808	807	3ad2antl1	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> M =/= ( j + 1 ) )
809	792 793 796 808	leneltd	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) < M )
810		elfzo2	|- ( ( j + 1 ) e. ( 0 ..^ M ) <-> ( ( j + 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j + 1 ) < M ) )
811	785 787 809 810	syl3anbrc	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( j + 1 ) e. ( 0 ..^ M ) )
812	48	adantr	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
813		fzofzp1	|- ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
814	813	adantl	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
815	812 814	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
816	815	rexrd	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
817	816	adantlr	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
818	817	3adant3	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
819	818	adantr	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
820		simpl1l	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ph )
821	820 48	syl	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
822		fzofzp1	|- ( ( j + 1 ) e. ( 0 ..^ M ) -> ( ( j + 1 ) + 1 ) e. ( 0 ... M ) )
823	811 822	syl	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( ( j + 1 ) + 1 ) e. ( 0 ... M ) )
824	821 823	ffvelrnd	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( ( j + 1 ) + 1 ) ) e. RR )
825	824	rexrd	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( ( j + 1 ) + 1 ) ) e. RR* )
826	627	rexrd	|- ( ph -> ( E ` X ) e. RR* )
827	826	ad2antrr	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. RR* )
828	827	3ad2antl1	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. RR* )
829	815	leidd	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) <_ ( Q ` ( j + 1 ) ) )
830	829	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) <_ ( Q ` ( j + 1 ) ) )
831		id	|- ( ( E ` X ) = ( Q ` ( j + 1 ) ) -> ( E ` X ) = ( Q ` ( j + 1 ) ) )
832	831	eqcomd	|- ( ( E ` X ) = ( Q ` ( j + 1 ) ) -> ( Q ` ( j + 1 ) ) = ( E ` X ) )
833	832	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) = ( E ` X ) )
834	830 833	breqtrd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) <_ ( E ` X ) )
835	834	adantllr	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) <_ ( E ` X ) )
836	835	3adantl3	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) <_ ( E ` X ) )
837		simpr	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) = ( Q ` ( j + 1 ) ) )
838		simpr	|- ( ( ( ph /\ ( j + 1 ) e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) = ( Q ` ( j + 1 ) ) )
839		ovex	|- ( j + 1 ) e. _V
840		eleq1	|- ( i = ( j + 1 ) -> ( i e. ( 0 ..^ M ) <-> ( j + 1 ) e. ( 0 ..^ M ) ) )
841	840	anbi2d	|- ( i = ( j + 1 ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( j + 1 ) e. ( 0 ..^ M ) ) ) )
842		fveq2	|- ( i = ( j + 1 ) -> ( Q ` i ) = ( Q ` ( j + 1 ) ) )
843		oveq1	|- ( i = ( j + 1 ) -> ( i + 1 ) = ( ( j + 1 ) + 1 ) )
844	843	fveq2d	|- ( i = ( j + 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j + 1 ) + 1 ) ) )
845	842 844	breq12d	|- ( i = ( j + 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j + 1 ) ) < ( Q ` ( ( j + 1 ) + 1 ) ) ) )
846	841 845	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 ) ) ) ) )
847	839 846 81	vtocl	|- ( ( ph /\ ( j + 1 ) e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) < ( Q ` ( ( j + 1 ) + 1 ) ) )
848	847	adantr	|- ( ( ( ph /\ ( j + 1 ) e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) < ( Q ` ( ( j + 1 ) + 1 ) ) )
849	838 848	eqbrtrd	|- ( ( ( ph /\ ( j + 1 ) e. ( 0 ..^ M ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) < ( Q ` ( ( j + 1 ) + 1 ) ) )
850	820 811 837 849	syl21anc	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) < ( Q ` ( ( j + 1 ) + 1 ) ) )
851	819 825 828 836 850	elicod	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` ( j + 1 ) ) [,) ( Q ` ( ( j + 1 ) + 1 ) ) ) )
852	842 844	oveq12d	|- ( i = ( j + 1 ) -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j + 1 ) ) [,) ( Q ` ( ( j + 1 ) + 1 ) ) ) )
853	852	eleq2d	|- ( i = ( j + 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j + 1 ) ) [,) ( Q ` ( ( j + 1 ) + 1 ) ) ) ) )
854	853	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 ) ) ) )
855	811 851 854	syl2anc	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
856		simpl2	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> j e. ( 0 ..^ M ) )
857		id	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) )
858	857	3adant1r	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) )
859		elfzofz	|- ( j e. ( 0 ..^ M ) -> j e. ( 0 ... M ) )
860	859	adantl	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ... M ) )
861	812 860	ffvelrnd	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) e. RR )
862	861	rexrd	|- ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) e. RR* )
863	862	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` j ) e. RR* )
864	863	3adantl3	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` j ) e. RR* )
865	816	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
866	865	3adantl3	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
867	826	adantr	|- ( ( ph /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. RR* )
868	867	3ad2antl1	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. RR* )
869	861	3adant3	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` j ) e. RR )
870	627	3ad2ant1	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( E ` X ) e. RR )
871	862	3adant3	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` j ) e. RR* )
872	816	3adant3	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
873		simp3	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) )
874		iocgtlb	|- ( ( ( Q ` j ) e. RR* /\ ( Q ` ( j + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` j ) < ( E ` X ) )
875	871 872 873 874	syl3anc	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` j ) < ( E ` X ) )
876	869 870 875	ltled	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( Q ` j ) <_ ( E ` X ) )
877	876	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` j ) <_ ( E ` X ) )
878	870	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. RR )
879	815	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR )
880	879	3adantl3	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR )
881		iocleub	|- ( ( ( Q ` j ) e. RR* /\ ( Q ` ( j + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( j + 1 ) ) )
882	871 872 873 881	syl3anc	|- ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( j + 1 ) ) )
883	882	adantr	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) <_ ( Q ` ( j + 1 ) ) )
884		neqne	|- ( -. ( E ` X ) = ( Q ` ( j + 1 ) ) -> ( E ` X ) =/= ( Q ` ( j + 1 ) ) )
885	884	necomd	|- ( -. ( E ` X ) = ( Q ` ( j + 1 ) ) -> ( Q ` ( j + 1 ) ) =/= ( E ` X ) )
886	885	adantl	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( Q ` ( j + 1 ) ) =/= ( E ` X ) )
887	878 880 883 886	leneltd	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) < ( Q ` ( j + 1 ) ) )
888	864 866 868 877 887	elicod	|- ( ( ( ph /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
889	858 888	sylan	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
890	771 773	oveq12d	|- ( i = j -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
891	890	eleq2d	|- ( i = j -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) ) )
892	891	rspcev	|- ( ( j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
893	856 889 892	syl2anc	|- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) /\ -. ( E ` X ) = ( Q ` ( j + 1 ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
894	855 893	pm2.61dan	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
895	894	rexlimdv3a	|- ( ( ph /\ ( E ` X ) =/= B ) -> ( E. j e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` j ) (,] ( Q ` ( j + 1 ) ) ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
896	778 895	mpd	|- ( ( ph /\ ( E ` X ) =/= B ) -> E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
897		simpr	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
898		oveq1	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
899	898	oveq2d	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( X + ( k x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
900	899	eqeq2d	|- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( E ` X ) = ( X + ( k x. T ) ) <-> ( E ` X ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
901	900	rspcev	|- ( ( ( |_ ` ( ( B - X ) / T ) ) e. ZZ /\ ( E ` X ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) -> E. k e. ZZ ( E ` X ) = ( X + ( k x. T ) ) )
902	105 113 901	syl2anc	|- ( ph -> E. k e. ZZ ( E ` X ) = ( X + ( k x. T ) ) )
903	902	ad2antrr	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> E. k e. ZZ ( E ` X ) = ( X + ( k x. T ) ) )
904		r19.42v	|- ( E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) <-> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ E. k e. ZZ ( E ` X ) = ( X + ( k x. T ) ) ) )
905	897 903 904	sylanbrc	|- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) )
906	905	ex	|- ( ( ph /\ ( E ` X ) =/= B ) -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) )
907	906	reximdv	|- ( ( ph /\ ( E ` X ) =/= B ) -> ( E. i e. ( 0 ..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) )
908	896 907	mpd	|- ( ( ph /\ ( E ` X ) =/= B ) -> E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) )
909	629 908	jca	|- ( ( ph /\ ( E ` X ) =/= B ) -> ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) )
910		eleq1	|- ( y = ( E ` X ) -> ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
911		eqeq1	|- ( y = ( E ` X ) -> ( y = ( X + ( k x. T ) ) <-> ( E ` X ) = ( X + ( k x. T ) ) ) )
912	910 911	anbi12d	|- ( y = ( E ` X ) -> ( ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) <-> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) )
913	912	2rexbidv	|- ( y = ( E ` X ) -> ( E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) <-> E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) )
914	913	anbi2d	|- ( y = ( E ` X ) -> ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) <-> ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) ) )
915	914	imbi1d	|- ( y = ( E ` X ) -> ( ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( y e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ y = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) <-> ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) ) )
916	915 614	vtoclg	|- ( ( E ` X ) e. RR -> ( ( ph /\ E. i e. ( 0 ..^ M ) E. k e. ZZ ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) /\ ( E ` X ) = ( X + ( k x. T ) ) ) ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )
917	628 909 916	sylc	|- ( ( ph /\ ( E ` X ) =/= B ) -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
918	616 917	pm2.61dane	|- ( ph -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )