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