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