Theorem fourierdlem49 40372

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

Hypotheses

Ref	Expression
fourierdlem49.a	|- ( ph -> A e. RR )
fourierdlem49.b	|- ( ph -> B e. RR )
fourierdlem49.altb	|- ( ph -> A < B )
fourierdlem49.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 ) ) ) } )
fourierdlem49.t	|- T = ( B - A )
fourierdlem49.m	|- ( ph -> M e. NN )
fourierdlem49.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem49.d	|- ( ph -> D C_ RR )
fourierdlem49.f	|- ( ph -> F : D --> RR )
fourierdlem49.dper	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
fourierdlem49.per	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
fourierdlem49.cn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem49.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
fourierdlem49.x	|- ( ph -> X e. RR )
fourierdlem49.z	|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
fourierdlem49.e	|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )

Assertion

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

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

Allowed substitution hints:   ph( m, p)   A( k)   D( i, m, p)   P( x, i, k, m, p)   Q( m)   T( i, m, p)   E( m, p)   F( m, p)   L( x, i, k, m, p)   X( m, p)   Z( i, m, p)

Proof of Theorem fourierdlem49

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

Step	Hyp	Ref	Expression
1		fourierdlem49.a	. . . . . 6 |- ( ph -> A e. RR )
2		fourierdlem49.b	. . . . . 6 |- ( ph -> B e. RR )
3		fourierdlem49.altb	. . . . . 6 |- ( ph -> A < B )
4		fourierdlem49.t	. . . . . 6 |- T = ( B - A )
5		fourierdlem49.e	. . . . . . 7 |- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
6		ovex 6678	. . . . . . . . . 10 |- ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
7		fourierdlem49.z	. . . . . . . . . . 11 |- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
8	7	fvmpt2 6291	. . . . . . . . . 10 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
9	6, 8	mpan2 707	. . . . . . . . 9 |- ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
10	9	oveq2d 6666	. . . . . . . 8 |- ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
11	10	mpteq2ia 4740	. . . . . . 7 |- ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
12	5, 11	eqtri 2644	. . . . . 6 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13	1, 2, 3, 4, 12	fourierdlem4 40328	. . . . 5 |- ( ph -> E : RR --> ( A (,] B ) )
14		fourierdlem49.x	. . . . 5 |- ( ph -> X e. RR )
15	13, 14	ffvelrnd 6360	. . . 4 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
16		simpr 477	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
17		fourierdlem49.q	. . . . . . . . . . . . 13 |- ( ph -> Q e. ( P ` M ) )
18		fourierdlem49.m	. . . . . . . . . . . . . 14 |- ( ph -> M e. NN )
19		fourierdlem49.p	. . . . . . . . . . . . . . 15 |- 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 ) ) ) } )
20	19	fourierdlem2 40326	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) ) )
21	18, 20	syl 17	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) ) )
22	17, 21	mpbid 222	. . . . . . . . . . . 12 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
23	22	simpld 475	. . . . . . . . . . 11 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
24		elmapi 7879	. . . . . . . . . . 11 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
25	23, 24	syl 17	. . . . . . . . . 10 |- ( ph -> Q : ( 0 ... M ) --> RR )
26		ffn 6045	. . . . . . . . . 10 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
27	25, 26	syl 17	. . . . . . . . 9 |- ( ph -> Q Fn ( 0 ... M ) )
28	27	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
29		fvelrnb 6243	. . . . . . . 8 |- ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
30	28, 29	syl 17	. . . . . . 7 |- ( ( ( 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 ) ) )
31	16, 30	mpbid 222	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
32		1zzd 11408	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
33		elfzelz 12342	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> j e. ZZ )
34	33	ad2antlr 763	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
35		1e0p1 11552	. . . . . . . . . . . . . . . . 17 |- 1 = ( 0 + 1 )
36	35	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 = ( 0 + 1 ) )
37	34	zred 11482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
38		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 0 <_ j )
39	38	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ j )
40		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
41	40	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
42	41	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
43		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
44	43	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
45	22	simprld 795	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
46	45	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( Q ` 0 ) = A )
47	46	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
48	42, 44, 47	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
49	48	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
50	49	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
51	1	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
52	1	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A e. RR* )
53	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
54	2	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> B e. RR* )
55	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
56		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
57		iocgtlb 39724	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
58	53, 55, 56, 57	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
59	51, 58	gtned 10172	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
60	59	neneqd 2799	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
61	60	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> -. ( E ` X ) = A )
62	50, 61	pm2.65da 600	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
63	62	neqned 2801	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
64	37, 39, 63	ne0gt0d 10174	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
65		0zd 11389	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
66		zltp1le 11427	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
67	65, 34, 66	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
68	64, 67	mpbid 222	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
69	36, 68	eqbrtrd 4675	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
70		eluz2 11693	. . . . . . . . . . . . . . 15 |- ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
71	32, 34, 69, 70	syl3anbrc 1246	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( ZZ>= ` 1 ) )
72		nnuz 11723	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
73	71, 72	syl6eleqr 2712	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
74		nnm1nn0 11334	. . . . . . . . . . . . 13 |- ( j e. NN -> ( j - 1 ) e. NN0 )
75	73, 74	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. NN0 )
76		nn0uz 11722	. . . . . . . . . . . . 13 |- NN0 = ( ZZ>= ` 0 )
77	76	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> NN0 = ( ZZ>= ` 0 ) )
78	75, 77	eleqtrd 2703	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
79	18	nnzd 11481	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
80	79	ad3antrrr 766	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
81		peano2zm 11420	. . . . . . . . . . . . . . 15 |- ( j e. ZZ -> ( j - 1 ) e. ZZ )
82	33, 81	syl 17	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. ZZ )
83	82	zred 11482	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
84	33	zred 11482	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j e. RR )
85		elfzel2 12340	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> M e. ZZ )
86	85	zred 11482	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> M e. RR )
87	84	ltm1d 10956	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
88		elfzle2 12345	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j <_ M )
89	83, 84, 86, 87, 88	ltletrd 10197	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
90	89	ad2antlr 763	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
91		elfzo2 12473	. . . . . . . . . . 11 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
92	78, 80, 90, 91	syl3anbrc 1246	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0..^ M ) )
93	25	ad3antrrr 766	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
94	34, 81	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
95	65, 80, 94	3jca 1242	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) )
96	75	nn0ge0d 11354	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
97	83, 86, 89	ltled 10185	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
98	97	ad2antlr 763	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
99	95, 96, 98	jca32 558	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
100		elfz2 12333	. . . . . . . . . . . . . . 15 |- ( ( j - 1 ) e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
101	99, 100	sylibr 224	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
102	93, 101	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
103	102	rexrd 10089	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
104	25	ffvelrnda 6359	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
105	104	rexrd 10089	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
106	105	adantlr 751	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
107	106	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
108		iocssre 12253	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
109	52, 2, 108	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ph -> ( A (,] B ) C_ RR )
110	109	sselda 3603	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
111	110	rexrd 10089	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
112	111	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
113		simplll 798	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
114		ovex 6678	. . . . . . . . . . . . . . . 16 |- ( j - 1 ) e. _V
115		eleq1 2689	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
116	115	anbi2d 740	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
117		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
118		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
119	118	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
120	117, 119	breq12d 4666	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
121	116, 120	imbi12d 334	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
122	22	simprrd 797	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
123	122	r19.21bi 2932	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
124	114, 121, 123	vtocl 3259	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
125	113, 92, 124	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
126	33	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> j e. CC )
127		1cnd 10056	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 1 e. CC )
128	126, 127	npcand 10396	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
129	128	eqcomd 2628	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
130	129	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
131	130	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
132	131	ad2antlr 763	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
133	125, 132	breqtrd 4679	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
134		simpr 477	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
135	133, 134	breqtrd 4679	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
136	109, 15	sseldd 3604	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E ` X ) e. RR )
137	136	leidd 10594	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
138	137	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
139	41	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
140	138, 139	breqtrd 4679	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
141	140	adantllr 755	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
142	103, 107, 112, 135, 141	eliocd 39730	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) )
143	130	oveq2d 6666	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
144	143	ad2antlr 763	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
145	142, 144	eleqtrd 2703	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
146	117, 119	oveq12d 6668	. . . . . . . . . . . 12 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
147	146	eleq2d 2687	. . . . . . . . . . 11 |- ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
148	147	rspcev 3309	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
149	92, 145, 148	syl2anc 693	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) )
150	149	ex 450	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) )
151	150	adantlr 751	. . . . . . 7 |- ( ( ( ( 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 ) ) ) ) )
152	151	rexlimdva 3031	. . . . . 6 |- ( ( ( 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 ) ) ) ) )
153	31, 152	mpd 15	. . . . 5 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
154	18	ad2antrr 762	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
155	25	ad2antrr 762	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
156		iocssicc 12261	. . . . . . . . . 10 |- ( A (,] B ) C_ ( A [,] B )
157	46	eqcomd 2628	. . . . . . . . . . 11 |- ( ph -> A = ( Q ` 0 ) )
158	45	simprd 479	. . . . . . . . . . . 12 |- ( ph -> ( Q ` M ) = B )
159	158	eqcomd 2628	. . . . . . . . . . 11 |- ( ph -> B = ( Q ` M ) )
160	157, 159	oveq12d 6668	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
161	156, 160	syl5sseq 3653	. . . . . . . . 9 |- ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
162	161	sselda 3603	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
163	162	adantr 481	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
164		simpr 477	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
165		fveq2 6191	. . . . . . . . . 10 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
166	165	breq1d 4663	. . . . . . . . 9 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
167	166	cbvrabv 3199	. . . . . . . 8 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
168	167	supeq1i 8353	. . . . . . 7 |- sup ( { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
169	154, 155, 163, 164, 168	fourierdlem25 40349	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
170		ioossioc 39713	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
171	170	sseli 3599	. . . . . . . 8 |- ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
172	171	a1i 11	. . . . . . 7 |- ( ( ( ( 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 ) ) ) ) )
173	172	reximdva 3017	. . . . . 6 |- ( ( ( 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 ) ) ) ) )
174	169, 173	mpd 15	. . . . 5 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
175	153, 174	pm2.61dan 832	. . . 4 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
176	15, 175	mpdan 702	. . 3 |- ( ph -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
177		fourierdlem49.f	. . . . . . . . . . 11 |- ( ph -> F : D --> RR )
178		frel 6050	. . . . . . . . . . 11 |- ( F : D --> RR -> Rel F )
179	177, 178	syl 17	. . . . . . . . . 10 |- ( ph -> Rel F )
180		resindm 5444	. . . . . . . . . . 11 |- ( Rel F -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( -oo (,) ( E ` X ) ) ) )
181	180	eqcomd 2628	. . . . . . . . . 10 |- ( Rel F -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) )
182	179, 181	syl 17	. . . . . . . . 9 |- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) )
183		fdm 6051	. . . . . . . . . . . 12 |- ( F : D --> RR -> dom F = D )
184	177, 183	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = D )
185	184	ineq2d 3814	. . . . . . . . . 10 |- ( ph -> ( ( -oo (,) ( E ` X ) ) i^i dom F ) = ( ( -oo (,) ( E ` X ) ) i^i D ) )
186	185	reseq2d 5396	. . . . . . . . 9 |- ( ph -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
187	182, 186	eqtrd 2656	. . . . . . . 8 |- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
188	187	3ad2ant1 1082	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
189	188	oveq1d 6665	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) = ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) lim CC ( E ` X ) ) )
190		ax-resscn 9993	. . . . . . . . . . 11 |- RR C_ CC
191	190	a1i 11	. . . . . . . . . 10 |- ( ph -> RR C_ CC )
192	177, 191	fssd 6057	. . . . . . . . 9 |- ( ph -> F : D --> CC )
193	192	3ad2ant1 1082	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> F : D --> CC )
194		inss2 3834	. . . . . . . . 9 |- ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D
195	194	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D )
196	193, 195	fssresd 6071	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) : ( ( -oo (,) ( E ` X ) ) i^i D ) --> CC )
197		mnfxr 10096	. . . . . . . . . 10 |- -oo e. RR*
198	197	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo e. RR* )
199	25	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
200		elfzofz 12485	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
201	200	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
202	199, 201	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
203	202	rexrd 10089	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
204	202	mnfltd 11958	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo < ( Q ` i ) )
205	198, 203, 204	xrltled 39486	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo <_ ( Q ` i ) )
206		iooss1 12210	. . . . . . . . . 10 |- ( ( -oo e. RR* /\ -oo <_ ( Q ` i ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
207	197, 205, 206	sylancr 695	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
208	207	3adant3 1081	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
209		fzofzp1 12565	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
210	209	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
211	199, 210	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
212	211	3adant3 1081	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
213	212	rexrd 10089	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
214	202	3adant3 1081	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
215	214	rexrd 10089	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
216		simp3 1063	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
217		iocleub 39725	. . . . . . . . . . 11 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
218	215, 213, 216, 217	syl3anc 1326	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
219		iooss2 12211	. . . . . . . . . 10 |- ( ( ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) <_ ( Q ` ( i + 1 ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
220	213, 218, 219	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
221		fourierdlem49.cn	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
222		cncff 22696	. . . . . . . . . . . . 13 |- ( ( 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 )
223		fdm 6051	. . . . . . . . . . . . 13 |- ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
224	221, 222, 223	3syl 18	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
225		ssdmres 5420	. . . . . . . . . . . 12 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
226	224, 225	sylibr 224	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
227	184	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom F = D )
228	226, 227	sseqtrd 3641	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
229	228	3adant3 1081	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
230	220, 229	sstrd 3613	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
231	208, 230	ssind 3837	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( -oo (,) ( E ` X ) ) i^i D ) )
232		fourierdlem49.d	. . . . . . . . . 10 |- ( ph -> D C_ RR )
233	232, 191	sstrd 3613	. . . . . . . . 9 |- ( ph -> D C_ CC )
234	233	3ad2ant1 1082	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D C_ CC )
235	194, 234	syl5ss 3614	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ CC )
236		eqid 2622	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
237		eqid 2622	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
238	136	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
239	238	rexrd 10089	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR* )
240		iocgtlb 39724	. . . . . . . . . 10 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
241	215, 213, 216, 240	syl3anc 1326	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
242	238	leidd 10594	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( E ` X ) )
243	215, 239, 239, 241, 242	eliocd 39730	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( E ` X ) ) )
244		snunioo2 39731	. . . . . . . . . . 11 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ ( Q ` i ) < ( E ` X ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
245	215, 239, 241, 244	syl3anc 1326	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
246	245	fveq2d 6195	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) )
247	236	cnfldtop 22587	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) e. Top
248		ovex 6678	. . . . . . . . . . . . 13 |- ( -oo (,) ( E ` X ) ) e. _V
249	248	inex1 4799	. . . . . . . . . . . 12 |- ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V
250		snex 4908	. . . . . . . . . . . 12 |- { ( E ` X ) } e. _V
251	249, 250	unex 6956	. . . . . . . . . . 11 |- ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V
252		resttop 20964	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top )
253	247, 251, 252	mp2an 708	. . . . . . . . . 10 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top
254		retop 22565	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) e. Top
255	254	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( topGen ` ran (,) ) e. Top )
256	251	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V )
257		iooretop 22569	. . . . . . . . . . . . 13 |- ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) )
258	257	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) ) )
259		elrestr 16089	. . . . . . . . . . . 12 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V /\ ( ( Q ` i ) (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
260	255, 256, 258, 259	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
261		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x = ( E ` X ) )
262		pnfxr 10092	. . . . . . . . . . . . . . . . . . . 20 |- +oo e. RR*
263	262	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> +oo e. RR* )
264	238	ltpnfd 11955	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < +oo )
265	215, 263, 238, 241, 264	eliood 39720	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) +oo ) )
266		snidg 4206	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( E ` X ) e. RR -> ( E ` X ) e. { ( E ` X ) } )
267		elun2 3781	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( E ` X ) e. { ( E ` X ) } -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
268	266, 267	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E ` X ) e. RR -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
269	136, 268	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
270	269	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
271	265, 270	elind 3798	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
272	271	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
273	261, 272	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
274	273	adantlr 751	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
275	215	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
276	262	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> +oo e. RR* )
277	203	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
278	136	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( E ` X ) e. RR )
279	278	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR )
280		iocssre 12253	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
281	277, 279, 280	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
282		simpr 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
283	281, 282	sseldd 3604	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
284	283	3adantl3 1219	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
285	279	rexrd 10089	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR* )
286		iocgtlb 39724	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
287	277, 285, 282, 286	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
288	287	3adantl3 1219	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
289	284	ltpnfd 11955	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x < +oo )
290	275, 276, 284, 288, 289	eliood 39720	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
291	290	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
292	197	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo e. RR* )
293	285	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR* )
294	283	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
295	294	mnfltd 11958	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo < x )
296	136	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
297		iocleub 39725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
298	277, 285, 282, 297	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
299	298	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x <_ ( E ` X ) )
300		neqne 2802	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. x = ( E ` X ) -> x =/= ( E ` X ) )
301	300	necomd 2849	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = ( E ` X ) -> ( E ` X ) =/= x )
302	301	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) =/= x )
303	294, 296, 299, 302	leneltd 10191	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
304	292, 293, 294, 295, 303	eliood 39720	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
305	304	3adantll3 39203	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
306	229	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
307	275	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` i ) e. RR* )
308	213	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
309	284	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
310	288	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` i ) < x )
311	238	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
312	212	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
313	303	3adantll3 39203	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
314	218	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
315	309, 311, 312, 313, 314	ltletrd 10197	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( Q ` ( i + 1 ) ) )
316	307, 308, 309, 310, 315	eliood 39720	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
317	306, 316	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. D )
318	305, 317	elind 3798	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
319		elun1 3780	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
320	318, 319	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
321	291, 320	elind 3798	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
322	274, 321	pm2.61dan 832	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
323	215	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) e. RR* )
324	239	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( E ` X ) e. RR* )
325		elinel1 3799	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
326		elioore 12205	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR )
327	326	rexrd 10089	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR* )
328	325, 327	syl 17	. . . . . . . . . . . . . . 15 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. RR* )
329	328	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. RR* )
330	203	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) e. RR* )
331	262	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> +oo e. RR* )
332	325	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
333		ioogtlb 39717	. . . . . . . . . . . . . . . 16 |- ( ( ( Q ` i ) e. RR* /\ +oo e. RR* /\ x e. ( ( Q ` i ) (,) +oo ) ) -> ( Q ` i ) < x )
334	330, 331, 332, 333	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
335	334	3adantl3 1219	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
336		elinel2 3800	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
337		elsni 4194	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { ( E ` X ) } -> x = ( E ` X ) )
338	337	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x = ( E ` X ) )
339	137	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { ( E ` X ) } ) -> ( E ` X ) <_ ( E ` X ) )
340	338, 339	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
341	340	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
342		simpll 790	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> ph )
343		elunnel2 39198	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) /\ -. x e. { ( E ` X ) } ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
344	343	adantll 750	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> x e. ( ( -oo (,) ( E ` X ) ) i^i D ) )
345		elinel1 3799	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( -oo (,) ( E ` X ) ) )
346		elioore 12205	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -oo (,) ( E ` X ) ) -> x e. RR )
347	346	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. RR )
348	136	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR )
349	197	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> -oo e. RR* )
350	348	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR* )
351		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. ( -oo (,) ( E ` X ) ) )
352		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( -oo e. RR* /\ ( E ` X ) e. RR* /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
353	349, 350, 351, 352	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
354	347, 348, 353	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x <_ ( E ` X ) )
355	345, 354	sylan2 491	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( ( -oo (,) ( E ` X ) ) i^i D ) ) -> x <_ ( E ` X ) )
356	342, 344, 355	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
357	341, 356	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
358	357	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
359	336, 358	sylan2 491	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x <_ ( E ` X ) )
360	359	3adantl3 1219	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x <_ ( E ` X ) )
361	323, 324, 329, 335, 360	eliocd 39730	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
362	322, 361	impbida 877	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( x e. ( ( Q ` i ) (,] ( E ` X ) ) <-> x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) )
363	362	eqrdv 2620	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) = ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
364		ioossre 12235	. . . . . . . . . . . . . 14 |- ( -oo (,) ( E ` X ) ) C_ RR
365		ssinss1 3841	. . . . . . . . . . . . . 14 |- ( ( -oo (,) ( E ` X ) ) C_ RR -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ RR )
366	364, 365	mp1i 13	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ RR )
367	238	snssd 4340	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { ( E ` X ) } C_ RR )
368	366, 367	unssd 3789	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) C_ RR )
369		eqid 2622	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
370	236, 369	tgiooss 39733	. . . . . . . . . . . 12 |- ( ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) C_ RR -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
371	368, 370	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
372	260, 363, 371	3eltr4d 2716	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) e. ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
373		isopn3i 20886	. . . . . . . . . 10 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top /\ ( ( Q ` i ) (,] ( E ` X ) ) e. ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) = ( ( Q ` i ) (,] ( E ` X ) ) )
374	253, 372, 373	sylancr 695	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( Q ` i ) (,] ( E ` X ) ) ) = ( ( Q ` i ) (,] ( E ` X ) ) )
375	246, 374	eqtr2d 2657	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) )
376	243, 375	eleqtrd 2703	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) ` ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) ) )
377	196, 231, 235, 236, 237, 376	limcres 23650	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) = ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) lim CC ( E ` X ) ) )
378	231	resabs1d 5428	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
379	378	oveq1d 6665	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
380	189, 377, 379	3eqtr2d 2662	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
381	184	feq2d 6031	. . . . . . . . . . . 12 |- ( ph -> ( F : dom F --> CC <-> F : D --> CC ) )
382	192, 381	mpbird 247	. . . . . . . . . . 11 |- ( ph -> F : dom F --> CC )
383	382	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> F : dom F --> CC )
384	383	3ad2antl1 1223	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> F : dom F --> CC )
385		ioosscn 39716	. . . . . . . . . 10 |- ( ( Q ` i ) (,) ( E ` X ) ) C_ CC
386	385	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ CC )
387	184	eqcomd 2628	. . . . . . . . . . . 12 |- ( ph -> D = dom F )
388	387	3ad2ant1 1082	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D = dom F )
389	230, 388	sseqtrd 3641	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ dom F )
390	389	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ dom F )
391	7	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
392		oveq2 6658	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> ( B - x ) = ( B - X ) )
393	392	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
394	393	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
395	394	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
396	395	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
397	2, 14	resubcld 10458	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B - X ) e. RR )
398	2, 1	resubcld 10458	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( B - A ) e. RR )
399	4, 398	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> T e. RR )
400	1, 2	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
401	3, 400	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 0 < ( B - A ) )
402	4	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B - A ) = T
403	402	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - A ) = T )
404	401, 403	breqtrd 4679	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> 0 < T )
405	404	gt0ne0d 10592	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> T =/= 0 )
406	397, 399, 405	redivcld 10853	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B - X ) / T ) e. RR )
407	406	flcld 12599	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
408	407	zred 11482	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
409	408, 399	remulcld 10070	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
410	391, 396, 14, 409	fvmptd 6288	. . . . . . . . . . . . . 14 |- ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
411	410, 409	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ph -> ( Z ` X ) e. RR )
412	411	recnd 10068	. . . . . . . . . . . 12 |- ( ph -> ( Z ` X ) e. CC )
413	412	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> ( Z ` X ) e. CC )
414	413	3ad2antl1 1223	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> ( Z ` X ) e. CC )
415	414	negcld 10379	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> -u ( Z ` X ) e. CC )
416		eqid 2622	. . . . . . . . 9 |- { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) }
417		ioosscn 39716	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ CC
418	417	sseli 3599	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. CC )
419	418	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. CC )
420	412	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. CC )
421	419, 420	pncand 10393	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = y )
422	421	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) - ( Z ` X ) ) )
423	422	3ad2antl1 1223	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) - ( Z ` X ) ) )
424	410	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
425	424	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
426	419, 420	addcld 10059	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. CC )
427	409	recnd 10068	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
428	427	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
429	426, 428	negsubd 10398	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
430	407	zcnd 11483	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
431	399	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> T e. CC )
432	430, 431	mulneg1d 10483	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
433	432	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
434	433	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
435	434	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
436	425, 429, 435	3eqtr2d 2662	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
437	436	3ad2antl1 1223	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
438	407	znegcld 11484	. . . . . . . . . . . . . . . . . 18 |- ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
439	438	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
440	439	3ad2antl1 1223	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
441		simpl1 1064	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
442	230	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
443	203	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR* )
444	136	rexrd 10089	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( E ` X ) e. RR* )
445	444	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) e. RR* )
446		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
447	446	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
448	411	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
449	447, 448	readdcld 10069	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
450	449	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
451	411	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Z ` X ) e. RR )
452	202, 451	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
453	452	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
454	453	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
455	14	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> X e. RR* )
456	455	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
457		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
458		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
459	454, 456, 457, 458	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
460	202	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
461	451	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
462	446	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
463	460, 461, 462	ltsubaddd 10623	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < y <-> ( Q ` i ) < ( y + ( Z ` X ) ) ) )
464	459, 463	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
465	14	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
466		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
467	454, 456, 457, 466	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
468	462, 465, 461, 467	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
469	5	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> E = ( x e. RR |-> ( x + ( Z ` x ) ) ) )
470		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = X -> x = X )
471		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = X -> ( Z ` x ) = ( Z ` X ) )
472	470, 471	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
473	472	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x = X ) -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
474	14, 411	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( X + ( Z ` X ) ) e. RR )
475	469, 473, 14, 474	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
476	475	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
477	476	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
478	468, 477	breqtrd 4679	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
479	443, 445, 450, 464, 478	eliood 39720	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( E ` X ) ) )
480	479	3adantl3 1219	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( E ` X ) ) )
481	442, 480	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. D )
482	441, 481, 440	3jca 1242	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
483		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
484	483	3anbi3d 1405	. . . . . . . . . . . . . . . . . 18 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
485		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
486	485	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
487	486	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
488	484, 487	imbi12d 334	. . . . . . . . . . . . . . . . 17 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) ) )
489		ovex 6678	. . . . . . . . . . . . . . . . . 18 |- ( y + ( Z ` X ) ) e. _V
490		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
491	490	3anbi2d 1404	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
492		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
493	492	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
494	491, 493	imbi12d 334	. . . . . . . . . . . . . . . . . 18 |- ( x = ( y + ( Z ` X ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) ) )
495		fourierdlem49.dper	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
496	489, 494, 495	vtocl 3259	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
497	488, 496	vtoclg 3266	. . . . . . . . . . . . . . . 16 |- ( -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
498	440, 482, 497	sylc 65	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
499	437, 498	eqeltrd 2701	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) - ( Z ` X ) ) e. D )
500	423, 499	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. D )
501	500	ralrimiva 2966	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
502		dfss3 3592	. . . . . . . . . . . 12 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D <-> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
503	501, 502	sylibr 224	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
504	202	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
505	412	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Z ` X ) e. CC )
506	504, 505	negsubd 10398	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + -u ( Z ` X ) ) = ( ( Q ` i ) - ( Z ` X ) ) )
507	506	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) = ( ( Q ` i ) + -u ( Z ` X ) ) )
508	475	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( E ` X ) + -u ( Z ` X ) ) = ( ( X + ( Z ` X ) ) + -u ( Z ` X ) ) )
509	474	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( X + ( Z ` X ) ) e. CC )
510	509, 412	negsubd 10398	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( X + ( Z ` X ) ) + -u ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
511	14	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> X e. CC )
512	511, 412	pncand 10393	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
513	508, 510, 512	3eqtrrd 2661	. . . . . . . . . . . . . . 15 |- ( ph -> X = ( ( E ` X ) + -u ( Z ` X ) ) )
514	513	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X = ( ( E ` X ) + -u ( Z ` X ) ) )
515	507, 514	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) = ( ( ( Q ` i ) + -u ( Z ` X ) ) (,) ( ( E ` X ) + -u ( Z ` X ) ) ) )
516	451	renegcld 10457	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -u ( Z ` X ) e. RR )
517	202, 278, 516	iooshift 39748	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + -u ( Z ` X ) ) (,) ( ( E ` X ) + -u ( Z ` X ) ) ) = { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } )
518	515, 517	eqtr2d 2657	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
519	518	3adant3 1081	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
520	184	3ad2ant1 1082	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> dom F = D )
521	503, 519, 520	3sstr4d 3648	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } C_ dom F )
522	521	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } C_ dom F )
523	410	negeqd 10275	. . . . . . . . . . . . . . . 16 |- ( ph -> -u ( Z ` X ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
524	523, 433	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ph -> -u ( Z ` X ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
525	524	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ph -> ( x + -u ( Z ` X ) ) = ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
526	525	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ph -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
527	526	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
528	527	3ad2antl1 1223	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
529	438	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
530	529	3ad2antl1 1223	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
531		simpl1 1064	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ph )
532	230	sselda 3603	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> x e. D )
533	531, 532, 530	3jca 1242	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
534	483	3anbi3d 1405	. . . . . . . . . . . . . 14 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
535	485	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
536	535	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
537	536	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
538	534, 537	imbi12d 334	. . . . . . . . . . . . 13 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
539		fourierdlem49.per	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
540	538, 539	vtoclg 3266	. . . . . . . . . . . 12 |- ( -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ x e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
541	530, 533, 540	sylc 65	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) )
542	528, 541	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` x ) )
543	542	adantlr 751	. . . . . . . . 9 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) /\ x e. ( ( Q ` i ) (,) ( E ` X ) ) ) -> ( F ` ( x + -u ( Z ` X ) ) ) = ( F ` x ) )
544		simpr 477	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
545	384, 386, 390, 415, 416, 522, 543, 544	limcperiod 39860	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> y e. ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) lim CC ( ( E ` X ) + -u ( Z ` X ) ) ) )
546	518	reseq2d 5396	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) = ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) )
547	514	eqcomd 2628	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( E ` X ) + -u ( Z ` X ) ) = X )
548	546, 547	oveq12d 6668	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) lim CC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
549	548	3adant3 1081	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) lim CC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
550	549	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( Q ` i ) (,) ( E ` X ) ) z = ( x + -u ( Z ` X ) ) } ) lim CC ( ( E ` X ) + -u ( Z ` X ) ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
551	545, 550	eleqtrd 2703	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) -> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
552	382	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> F : dom F --> CC )
553	552	3ad2antl1 1223	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> F : dom F --> CC )
554	417	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ CC )
555	503, 520	sseqtr4d 3642	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ dom F )
556	555	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ dom F )
557	412	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> ( Z ` X ) e. CC )
558	557	3ad2antl1 1223	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> ( Z ` X ) e. CC )
559		eqid 2622	. . . . . . . . 9 |- { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) }
560	504, 505	npcand 10396	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` i ) )
561	560	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) )
562	475	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
563	561, 562	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) = ( ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) (,) ( X + ( Z ` X ) ) ) )
564	14	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
565	452, 564, 451	iooshift 39748	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) + ( Z ` X ) ) (,) ( X + ( Z ` X ) ) ) = { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } )
566	563, 565	eqtr2d 2657	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = ( ( Q ` i ) (,) ( E ` X ) ) )
567	566	3adant3 1081	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } = ( ( Q ` i ) (,) ( E ` X ) ) )
568	230, 567, 520	3sstr4d 3648	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } C_ dom F )
569	568	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } C_ dom F )
570	410	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ph -> ( x + ( Z ` X ) ) = ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
571	570	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ph -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
572	571	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
573	572	3ad2antl1 1223	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
574	407	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
575	574	3ad2antl1 1223	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
576		simpl1 1064	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
577	503	sselda 3603	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. D )
578	576, 577, 575	3jca 1242	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
579		eleq1 2689	. . . . . . . . . . . . . . 15 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
580	579	3anbi3d 1405	. . . . . . . . . . . . . 14 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
581		oveq1 6657	. . . . . . . . . . . . . . . . 17 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
582	581	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( x + ( k x. T ) ) = ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
583	582	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) )
584	583	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) <-> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
585	580, 584	imbi12d 334	. . . . . . . . . . . . 13 |- ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) ) <-> ( ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) ) )
586	585, 539	vtoclg 3266	. . . . . . . . . . . 12 |- ( ( |_ ` ( ( B - X ) / T ) ) e. ZZ -> ( ( ph /\ x e. D /\ ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) ) )
587	575, 578, 586	sylc 65	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) ) = ( F ` x ) )
588	573, 587	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` x ) )
589	588	adantlr 751	. . . . . . . . 9 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( F ` ( x + ( Z ` X ) ) ) = ( F ` x ) )
590		simpr 477	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
591	553, 554, 556, 558, 559, 569, 589, 590	limcperiod 39860	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> y e. ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) lim CC ( X + ( Z ` X ) ) ) )
592	566	reseq2d 5396	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
593	476	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
594	592, 593	oveq12d 6668	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) lim CC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
595	594	3adant3 1081	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) lim CC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
596	595	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> ( ( F |` { z e. CC | E. x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) z = ( x + ( Z ` X ) ) } ) lim CC ( X + ( Z ` X ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
597	591, 596	eleqtrd 2703	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) -> y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
598	551, 597	impbida 877	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( y e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) <-> y e. ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) ) )
599	598	eqrdv 2620	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
600		resindm 5444	. . . . . . . . . . 11 |- ( Rel F -> ( F |` ( ( -oo (,) X ) i^i dom F ) ) = ( F |` ( -oo (,) X ) ) )
601	600	eqcomd 2628	. . . . . . . . . 10 |- ( Rel F -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i dom F ) ) )
602	179, 601	syl 17	. . . . . . . . 9 |- ( ph -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i dom F ) ) )
603	184	ineq2d 3814	. . . . . . . . . 10 |- ( ph -> ( ( -oo (,) X ) i^i dom F ) = ( ( -oo (,) X ) i^i D ) )
604	603	reseq2d 5396	. . . . . . . . 9 |- ( ph -> ( F |` ( ( -oo (,) X ) i^i dom F ) ) = ( F |` ( ( -oo (,) X ) i^i D ) ) )
605	602, 604	eqtrd 2656	. . . . . . . 8 |- ( ph -> ( F |` ( -oo (,) X ) ) = ( F |` ( ( -oo (,) X ) i^i D ) ) )
606	605	oveq1d 6665	. . . . . . 7 |- ( ph -> ( ( F |` ( -oo (,) X ) ) lim CC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) lim CC X ) )
607	606	3ad2ant1 1082	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) X ) ) lim CC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) lim CC X ) )
608		inss2 3834	. . . . . . . . . 10 |- ( ( -oo (,) X ) i^i D ) C_ D
609	608	a1i 11	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) X ) i^i D ) C_ D )
610	193, 609	fssresd 6071	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( -oo (,) X ) i^i D ) ) : ( ( -oo (,) X ) i^i D ) --> CC )
611	452	mnfltd 11958	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo < ( ( Q ` i ) - ( Z ` X ) ) )
612	198, 453, 611	xrltled 39486	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo <_ ( ( Q ` i ) - ( Z ` X ) ) )
613		iooss1 12210	. . . . . . . . . . 11 |- ( ( -oo e. RR* /\ -oo <_ ( ( Q ` i ) - ( Z ` X ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
614	197, 612, 613	sylancr 695	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
615	614	3adant3 1081	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( -oo (,) X ) )
616	615, 503	ssind 3837	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ ( ( -oo (,) X ) i^i D ) )
617	608, 234	syl5ss 3614	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) X ) i^i D ) C_ CC )
618		eqid 2622	. . . . . . . 8 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
619	453	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
620	455	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. RR* )
621	475	3ad2ant1 1082	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
622	241, 621	breqtrd 4679	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + ( Z ` X ) ) )
623	411	3ad2ant1 1082	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
624	14	3ad2ant1 1082	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
625	214, 623, 624	ltsubaddd 10623	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < X <-> ( Q ` i ) < ( X + ( Z ` X ) ) ) )
626	622, 625	mpbird 247	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
627	14	leidd 10594	. . . . . . . . . . 11 |- ( ph -> X <_ X )
628	627	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X <_ X )
629	619, 620, 620, 626, 628	eliocd 39730	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
630		snunioo2 39731	. . . . . . . . . . . 12 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ ( ( Q ` i ) - ( Z ` X ) ) < X ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
631	619, 620, 626, 630	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
632	631	fveq2d 6195	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) )
633		ovex 6678	. . . . . . . . . . . . . 14 |- ( -oo (,) X ) e. _V
634	633	inex1 4799	. . . . . . . . . . . . 13 |- ( ( -oo (,) X ) i^i D ) e. _V
635		snex 4908	. . . . . . . . . . . . 13 |- { X } e. _V
636	634, 635	unex 6956	. . . . . . . . . . . 12 |- ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V
637		resttop 20964	. . . . . . . . . . . 12 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top )
638	247, 636, 637	mp2an 708	. . . . . . . . . . 11 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top
639	636	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V )
640		iooretop 22569	. . . . . . . . . . . . . 14 |- ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) )
641	640	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) ) )
642		elrestr 16089	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( ( -oo (,) X ) i^i D ) u. { X } ) e. _V /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
643	255, 639, 641, 642	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
644	453	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
645	262	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> +oo e. RR* )
646	14	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> X e. RR )
647		iocssre 12253	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) C_ RR )
648	644, 646, 647	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) C_ RR )
649		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
650	648, 649	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. RR )
651	455	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> X e. RR* )
652		iocgtlb 39724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
653	644, 651, 649, 652	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
654	650	ltpnfd 11955	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x < +oo )
655	644, 645, 650, 653, 654	eliood 39720	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
656	655	3adantl3 1219	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
657		eqvisset 3211	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> X e. _V )
658		snidg 4206	. . . . . . . . . . . . . . . . . . . 20 |- ( X e. _V -> X e. { X } )
659	657, 658	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> X e. { X } )
660	470, 659	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 |- ( x = X -> x e. { X } )
661		elun2 3781	. . . . . . . . . . . . . . . . . 18 |- ( x e. { X } -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
662	660, 661	syl 17	. . . . . . . . . . . . . . . . 17 |- ( x = X -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
663	662	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ x = X ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
664		simpll 790	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
665	644	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
666	455	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X e. RR* )
667	650	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. RR )
668	653	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
669	14	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X e. RR )
670		iocleub 39725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x <_ X )
671	644, 651, 649, 670	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x <_ X )
672	671	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x <_ X )
673	470	eqcoms 2630	. . . . . . . . . . . . . . . . . . . . . 22 |- ( X = x -> x = X )
674	673	necon3bi 2820	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = X -> X =/= x )
675	674	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> X =/= x )
676	667, 669, 672, 675	leneltd 10191	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x < X )
677	665, 666, 667, 668, 676	eliood 39720	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
678	677	3adantll3 39203	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
679	616	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. ( ( -oo (,) X ) i^i D ) )
680		elun1 3780	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -oo (,) X ) i^i D ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
681	679, 680	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
682	664, 678, 681	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) /\ -. x = X ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
683	663, 682	pm2.61dan 832	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
684	656, 683	elind 3798	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) -> x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
685	619	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
686	620	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> X e. RR* )
687		elinel1 3799	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
688		elioore 12205	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) -> x e. RR )
689	687, 688	syl 17	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. RR )
690	689	rexrd 10089	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. RR* )
691	690	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. RR* )
692	453	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
693	262	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> +oo e. RR* )
694	687	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) )
695		ioogtlb 39717	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ +oo e. RR* /\ x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
696	692, 693, 694, 695	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
697	696	3adantl3 1219	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < x )
698		elinel2 3800	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) )
699		elsni 4194	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { X } -> x = X )
700	699	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { X } ) -> x = X )
701	627	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { X } ) -> X <_ X )
702	700, 701	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. { X } ) -> x <_ X )
703	702	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ x e. { X } ) -> x <_ X )
704		simpll 790	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> ph )
705		elunnel2 39198	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) /\ -. x e. { X } ) -> x e. ( ( -oo (,) X ) i^i D ) )
706	705	adantll 750	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x e. ( ( -oo (,) X ) i^i D ) )
707		elinel1 3799	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ( -oo (,) X ) i^i D ) -> x e. ( -oo (,) X ) )
708	706, 707	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x e. ( -oo (,) X ) )
709		elioore 12205	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( -oo (,) X ) -> x e. RR )
710	709	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> x e. RR )
711	14	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> X e. RR )
712	197	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> -oo e. RR* )
713	455	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> X e. RR* )
714		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> x e. ( -oo (,) X ) )
715		iooltub 39735	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -oo e. RR* /\ X e. RR* /\ x e. ( -oo (,) X ) ) -> x < X )
716	712, 713, 714, 715	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> x < X )
717	710, 711, 716	ltled 10185	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( -oo (,) X ) ) -> x <_ X )
718	704, 708, 717	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) /\ -. x e. { X } ) -> x <_ X )
719	703, 718	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) -> x <_ X )
720	698, 719	sylan2 491	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x <_ X )
721	720	3ad2antl1 1223	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x <_ X )
722	685, 686, 691, 697, 721	eliocd 39730	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
723	684, 722	impbida 877	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( x e. ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) <-> x e. ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) )
724	723	eqrdv 2620	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) = ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) +oo ) i^i ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
725	608, 232	syl5ss 3614	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( -oo (,) X ) i^i D ) C_ RR )
726	14	snssd 4340	. . . . . . . . . . . . . . 15 |- ( ph -> { X } C_ RR )
727	725, 726	unssd 3789	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR )
728	727	3ad2ant1 1082	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR )
729	236, 369	tgiooss 39733	. . . . . . . . . . . . 13 |- ( ( ( ( -oo (,) X ) i^i D ) u. { X } ) C_ RR -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
730	728, 729	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) = ( ( topGen ` ran (,) ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
731	643, 724, 730	3eltr4d 2716	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) e. ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) )
732		isopn3i 20886	. . . . . . . . . . 11 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) e. Top /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) e. ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
733	638, 731, 732	sylancr 695	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) )
734	632, 733	eqtr2d 2657	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,] X ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) )
735	629, 734	eleqtrd 2703	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> X e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) X ) i^i D ) u. { X } ) ) ) ` ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) u. { X } ) ) )
736	610, 616, 617, 236, 618, 735	limcres 23650	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) = ( ( F |` ( ( -oo (,) X ) i^i D ) ) lim CC X ) )
737	736	eqcomd 2628	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) X ) i^i D ) ) lim CC X ) = ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
738	616	resabs1d 5428	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) = ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) )
739	738	oveq1d 6665	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( -oo (,) X ) i^i D ) ) |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) = ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) )
740	607, 737, 739	3eqtrrd 2661	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) lim CC X ) = ( ( F |` ( -oo (,) X ) ) lim CC X ) )
741	380, 599, 740	3eqtrrd 2661	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) X ) ) lim CC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
742	741	rexlimdv3a 3033	. . 3 |- ( ph -> ( E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( -oo (,) X ) ) lim CC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) ) )
743	176, 742	mpd 15	. 2 |- ( ph -> ( ( F |` ( -oo (,) X ) ) lim CC X ) = ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
744	123	3adant3 1081	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
745	221	3adant3 1081	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
746		fourierdlem49.l	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
747	746	3adant3 1081	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
748		eqid 2622	. . . . . . . 8 |- if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) = if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) )
749		eqid 2622	. . . . . . . 8 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
750	214, 212, 744, 745, 747, 214, 238, 241, 220, 748, 749	fourierdlem33 40357	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
751	220	resabs1d 5428	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) = ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) )
752	751	oveq1d 6665	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) = ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
753	750, 752	eleqtrd 2703	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) )
754		ne0i 3921	. . . . . 6 |- ( if ( ( E ` X ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( E ` X ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) =/= (/) )
755	753, 754	syl 17	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( E ` X ) ) ) lim CC ( E ` X ) ) =/= (/) )
756	380, 755	eqnetrd 2861	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) =/= (/) )
757	756	rexlimdv3a 3033	. . 3 |- ( ph -> ( E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) =/= (/) ) )
758	176, 757	mpd 15	. 2 |- ( ph -> ( ( F |` ( -oo (,) ( E ` X ) ) ) lim CC ( E ` X ) ) =/= (/) )
759	743, 758	eqnetrd 2861	1 |- ( ph -> ( ( F |` ( -oo (,) X ) ) 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   [,]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-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