Theorem fourierdlem48 40371

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

Hypotheses

Ref	Expression
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 ) ) ) ) lim CC ( 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

Ref	Expression
fourierdlem48	|- ( ph -> ( ( F |` ( X (,) +oo ) ) lim CC X ) =/= (/) )

Distinct variable groups:   x, k   A, i, x   A, m, p, i   B, i, k, x   B, m, p   D, k, x   i, E, k, y   i, F, k, x, y   i, M, k   m, M, p   y, M   Q, i, k, x   Q, p   y, Q   T, i, k, x, y   i, X, k, x, y   x, Z   ch, x   ph, i, k, x, y

Allowed substitution hints:   ph( m, p)   ch( y, i, k, m, p)   A( y, k)   B( y)   D( y, i, m, p)   P( x, y, i, k, m, p)   Q( m)   R( x, y, i, k, m, p)   T( m, p)   E( x, m, p)   F( m, p)   M( x)   X( m, p)   Z( y, i, k, m, p)

Proof of Theorem fourierdlem48

Dummy variables j w z are mutually distinct and distinct from all other variables.

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   |` cres 5116   Rel wrel 5119   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   (,)cioo 12175   (,]cioc 12176   [,)cico 12177   [,]cicc 12178   ...cfz 12326  ..^cfzo 12465   |_cfl 12591   ↾_t crest 16081   TopOpenctopn 16082   topGenctg 16098  ℂ_fldccnfld 19746   Topctop 20698   intcnt 20821   -cn->ccncf 22679   lim CC climc 23626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-plusg 15954  df-mulr 15955  df-starv 15956  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-rest 16083  df-topn 16084  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-ntr 20824  df-cn 21031  df-cnp 21032  df-xms 22125  df-ms 22126  df-cncf 22681  df-limc 23630

This theorem is referenced by:  fourierdlem94  40417  fourierdlem113  40436