Theorem fourierdlem48

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

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

Proof

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