Theorem fourierdlem49 38019

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:   A, i, m, p   x, A, i   B, i, k   B, m, p   x, B, k   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 6318	. . . . . . . . . 10 |- ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
7		fourierdlem49.z	. . . . . . . . . . 11 |- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
8	7	fvmpt2 5957	. . . . . . . . . 10 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
9	6, 8	mpan2 677	. . . . . . . . 9 |- ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
10	9	oveq2d 6306	. . . . . . . 8 |- ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
11	10	mpteq2ia 4485	. . . . . . 7 |- ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
12	5, 11	eqtri 2473	. . . . . 6 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13	1, 2, 3, 4, 12	fourierdlem4 37973	. . . . 5 |- ( ph -> E : RR --> ( A (,] B ) )
14		fourierdlem49.x	. . . . 5 |- ( ph -> X e. RR )
15	13, 14	ffvelrnd 6023	. . . 4 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
16		simpr 463	. . . . . . 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 37971	. . . . . . . . . . . . . 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 214	. . . . . . . . . . . 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 461	. . . . . . . . . . 11 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
24		elmapi 7493	. . . . . . . . . . 11 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
25	23, 24	syl 17	. . . . . . . . . 10 |- ( ph -> Q : ( 0 ... M ) --> RR )
26		ffn 5728	. . . . . . . . . 10 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
27	25, 26	syl 17	. . . . . . . . 9 |- ( ph -> Q Fn ( 0 ... M ) )
28	27	ad2antrr 732	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
29		fvelrnb 5912	. . . . . . . 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 214	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
32		1zzd 10968	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
33		elfzelz 11800	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> j e. ZZ )
34	33	ad2antlr 733	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
35		1e0p1 11079	. . . . . . . . . . . . . . . . 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 11040	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
38		elfzle1 11802	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 0 <_ j )
39	38	ad2antlr 733	. . . . . . . . . . . . . . . . . 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 2457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
42	41	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
43		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
44	43	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
45	22	simprld 765	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
46	45	simpld 461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( Q ` 0 ) = A )
47	46	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
48	42, 44, 47	3eqtrd 2489	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
49	48	adantllr 725	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
50	49	adantllr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
51	1	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
52	1	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A e. RR* )
53	52	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
54	2	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> B e. RR* )
55	54	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
56		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
57		iocgtlb 37599	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
58	53, 55, 56, 57	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
59	51, 58	gtned 9770	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
60	59	neneqd 2629	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
61	60	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 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 580	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
63	62	neqned 2631	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
64	37, 39, 63	ne0gt0d 9772	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
65		0zd 10949	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
66		zltp1le 10986	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
67	65, 34, 66	syl2anc 667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
68	64, 67	mpbid 214	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
69	36, 68	eqbrtrd 4423	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
70		eluz2 11165	. . . . . . . . . . . . . . 15 |- ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
71	32, 34, 69, 70	syl3anbrc 1192	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( ZZ>= ` 1 ) )
72		nnuz 11194	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
73	71, 72	syl6eleqr 2540	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
74		nnm1nn0 10911	. . . . . . . . . . . . 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 11193	. . . . . . . . . . . . 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 2531	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
79	18	nnzd 11039	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
80	79	ad3antrrr 736	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
81		peano2zm 10980	. . . . . . . . . . . . . . 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 11040	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
84	33	zred 11040	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j e. RR )
85		elfzel2 11798	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> M e. ZZ )
86	85	zred 11040	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> M e. RR )
87	84	ltm1d 10539	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
88		elfzle2 11803	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j <_ M )
89	83, 84, 86, 87, 88	ltletrd 9795	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
90	89	ad2antlr 733	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
91		elfzo2 11923	. . . . . . . . . . 11 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
92	78, 80, 90, 91	syl3anbrc 1192	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0..^ M ) )
93	25	ad3antrrr 736	. . . . . . . . . . . . . 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 1188	. . . . . . . . . . . . . . . 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 10928	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
97	83, 86, 89	ltled 9783	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
98	97	ad2antlr 733	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
99	95, 96, 98	jca32 538	. . . . . . . . . . . . . . 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 11791	. . . . . . . . . . . . . . 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 216	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
102	93, 101	ffvelrnd 6023	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
103	102	rexrd 9690	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
104	25	ffvelrnda 6022	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
105	104	rexrd 9690	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
106	105	adantlr 721	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
107	106	adantr 467	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
108		iocssre 11714	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
109	52, 2, 108	syl2anc 667	. . . . . . . . . . . . . . 15 |- ( ph -> ( A (,] B ) C_ RR )
110	109	sselda 3432	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
111	110	rexrd 9690	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
112	111	ad2antrr 732	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
113		simplll 768	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
114		ovex 6318	. . . . . . . . . . . . . . . 16 |- ( j - 1 ) e. _V
115		eleq1 2517	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
116	115	anbi2d 710	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
117		fveq2 5865	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
118		oveq1 6297	. . . . . . . . . . . . . . . . . . 19 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
119	118	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
120	117, 119	breq12d 4415	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
121	116, 120	imbi12d 322	. . . . . . . . . . . . . . . 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 767	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
123	122	r19.21bi 2757	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
124	114, 121, 123	vtocl 3100	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
125	113, 92, 124	syl2anc 667	. . . . . . . . . . . . . 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 11041	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> j e. CC )
127		1cnd 9659	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 1 e. CC )
128	126, 127	npcand 9990	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
129	128	eqcomd 2457	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
130	129	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
131	130	eqcomd 2457	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
132	131	ad2antlr 733	. . . . . . . . . . . . . 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 4427	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
134		simpr 463	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
135	133, 134	breqtrd 4427	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
136	109, 15	sseldd 3433	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E ` X ) e. RR )
137	136	leidd 10180	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
138	137	ad2antrr 732	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
139	41	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
140	138, 139	breqtrd 4427	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
141	140	adantllr 725	. . . . . . . . . . . 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 37605	. . . . . . . . . . 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 6306	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
144	143	ad2antlr 733	. . . . . . . . . . 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 2531	. . . . . . . . . 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 6308	. . . . . . . . . . . 12 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
147	146	eleq2d 2514	. . . . . . . . . . 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 3150	. . . . . . . . . 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 667	. . . . . . . . 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 436	. . . . . . . 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 721	. . . . . . 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 2879	. . . . . 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 732	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
155	25	ad2antrr 732	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
156		iocssicc 11722	. . . . . . . . . 10 |- ( A (,] B ) C_ ( A [,] B )
157	46	eqcomd 2457	. . . . . . . . . . 11 |- ( ph -> A = ( Q ` 0 ) )
158	45	simprd 465	. . . . . . . . . . . 12 |- ( ph -> ( Q ` M ) = B )
159	158	eqcomd 2457	. . . . . . . . . . 11 |- ( ph -> B = ( Q ` M ) )
160	157, 159	oveq12d 6308	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
161	156, 160	syl5sseq 3480	. . . . . . . . 9 |- ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
162	161	sselda 3432	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
163	162	adantr 467	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
164		simpr 463	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
165		fveq2 5865	. . . . . . . . . 10 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
166	165	breq1d 4412	. . . . . . . . 9 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
167	166	cbvrabv 3044	. . . . . . . 8 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
168	167	supeq1i 7961	. . . . . . 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 37994	. . . . . 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 37588	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
171	170	sseli 3428	. . . . . . . 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 2862	. . . . . 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 800	. . . 4 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
176	15, 175	mpdan 674	. . 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 5732	. . . . . . . . . . 11 |- ( F : D --> RR -> Rel F )
179	177, 178	syl 17	. . . . . . . . . 10 |- ( ph -> Rel F )
180		resindm 5149	. . . . . . . . . . 11 |- ( Rel F -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( -oo (,) ( E ` X ) ) ) )
181	180	eqcomd 2457	. . . . . . . . . 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 5733	. . . . . . . . . . . 12 |- ( F : D --> RR -> dom F = D )
184	177, 183	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = D )
185	184	ineq2d 3634	. . . . . . . . . 10 |- ( ph -> ( ( -oo (,) ( E ` X ) ) i^i dom F ) = ( ( -oo (,) ( E ` X ) ) i^i D ) )
186	185	reseq2d 5105	. . . . . . . . 9 |- ( ph -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
187	182, 186	eqtrd 2485	. . . . . . . 8 |- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
188	187	3ad2ant1 1029	. . . . . . 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 6305	. . . . . 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 9596	. . . . . . . . . . 11 |- RR C_ CC
191	190	a1i 11	. . . . . . . . . 10 |- ( ph -> RR C_ CC )
192	177, 191	fssd 5738	. . . . . . . . 9 |- ( ph -> F : D --> CC )
193	192	3ad2ant1 1029	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> F : D --> CC )
194		inss2 3653	. . . . . . . . 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 5750	. . . . . . 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 11414	. . . . . . . . . 10 |- -oo e. RR*
198	197	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo e. RR* )
199	25	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
200		elfzofz 11935	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
201	200	adantl 468	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
202	199, 201	ffvelrnd 6023	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
203	202	rexrd 9690	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
204	202	mnfltd 11426	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo < ( Q ` i ) )
205	198, 203, 204	xrltled 37484	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo <_ ( Q ` i ) )
206		iooss1 11671	. . . . . . . . . 10 |- ( ( -oo e. RR* /\ -oo <_ ( Q ` i ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
207	197, 205, 206	sylancr 669	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
208	207	3adant3 1028	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
209		fzofzp1 12008	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
210	209	adantl 468	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
211	199, 210	ffvelrnd 6023	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
212	211	3adant3 1028	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
213	212	rexrd 9690	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
214	202	3adant3 1028	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
215	214	rexrd 9690	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
216		simp3 1010	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
217		iocleub 37600	. . . . . . . . . . 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 1268	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
219		iooss2 11672	. . . . . . . . . 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 667	. . . . . . . . 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 21925	. . . . . . . . . . . . 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 5733	. . . . . . . . . . . . 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 5126	. . . . . . . . . . . 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 216	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
227	184	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom F = D )
228	226, 227	sseqtrd 3468	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
229	228	3adant3 1028	. . . . . . . . 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 3442	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
231	208, 230	ssind 3656	. . . . . . 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 3442	. . . . . . . . 9 |- ( ph -> D C_ CC )
234	233	3ad2ant1 1029	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D C_ CC )
235	194, 234	syl5ss 3443	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ CC )
236		eqid 2451	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
237		eqid 2451	. . . . . . 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 1029	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
239	238	rexrd 9690	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR* )
240		iocgtlb 37599	. . . . . . . . . 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 1268	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
242	238	leidd 10180	. . . . . . . . 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 37605	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( E ` X ) ) )
244		snunioo2 37606	. . . . . . . . . . 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 1268	. . . . . . . . . 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 5869	. . . . . . . . 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 21804	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) e. Top
248		ovex 6318	. . . . . . . . . . . . 13 |- ( -oo (,) ( E ` X ) ) e. _V
249	248	inex1 4544	. . . . . . . . . . . 12 |- ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V
250		snex 4641	. . . . . . . . . . . 12 |- { ( E ` X ) } e. _V
251	249, 250	unex 6589	. . . . . . . . . . 11 |- ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V
252		resttop 20176	. . . . . . . . . . 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 678	. . . . . . . . . 10 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top
254		retop 21782	. . . . . . . . . . . . 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 21786	. . . . . . . . . . . . 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 15327	. . . . . . . . . . . 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 1268	. . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x = ( E ` X ) )
262		pnfxr 11412	. . . . . . . . . . . . . . . . . . . 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 11423	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < +oo )
265	215, 263, 238, 241, 264	eliood 37595	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) +oo ) )
266		snidg 3994	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( E ` X ) e. RR -> ( E ` X ) e. { ( E ` X ) } )
267		elun2 3602	. . . . . . . . . . . . . . . . . . . . 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 1029	. . . . . . . . . . . . . . . . . 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 3618	. . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
278	136	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( E ` X ) e. RR )
279	278	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR )
280		iocssre 11714	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
281	277, 279, 280	syl2anc 667	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
282		simpr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
283	281, 282	sseldd 3433	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
284	283	3adantl3 1166	. . . . . . . . . . . . . . . . 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 9690	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR* )
286		iocgtlb 37599	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
287	277, 285, 282, 286	syl3anc 1268	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
288	287	3adantl3 1166	. . . . . . . . . . . . . . . . 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 11423	. . . . . . . . . . . . . . . . 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 37595	. . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR* )
294	283	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
295	294	mnfltd 11426	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo < x )
296	136	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
297		iocleub 37600	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
298	277, 285, 282, 297	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
299	298	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x <_ ( E ` X ) )
300		neqne 37374	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. x = ( E ` X ) -> x =/= ( E ` X ) )
301	300	necomd 2679	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = ( E ` X ) -> ( E ` X ) =/= x )
302	301	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) =/= x )
303	294, 296, 299, 302	leneltd 9789	. . . . . . . . . . . . . . . . . . 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 37595	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
305	304	3adantll3 37365	. . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . 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 37365	. . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . 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 9795	. . . . . . . . . . . . . . . . . . 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 37595	. . . . . . . . . . . . . . . . . 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 3433	. . . . . . . . . . . . . . . . 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 3618	. . . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . 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 3618	. . . . . . . . . . . . . 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 800	. . . . . . . . . . . . 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 467	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . 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 3619	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
326		elioore 11666	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR )
327	326	rexrd 9690	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . 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 37592	. . . . . . . . . . . . . . . 16 |- ( ( ( Q ` i ) e. RR* /\ +oo e. RR* /\ x e. ( ( Q ` i ) (,) +oo ) ) -> ( Q ` i ) < x )
334	330, 331, 332, 333	syl3anc 1268	. . . . . . . . . . . . . . 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 1166	. . . . . . . . . . . . . 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 3620	. . . . . . . . . . . . . . . 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 3993	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { ( E ` X ) } -> x = ( E ` X ) )
338	337	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x = ( E ` X ) )
339	137	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { ( E ` X ) } ) -> ( E ` X ) <_ ( E ` X ) )
340	338, 339	eqbrtrd 4423	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
341	340	adantlr 721	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
342		simpll 760	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> ph )
343		elunnel2 37360	. . . . . . . . . . . . . . . . . . . 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 720	. . . . . . . . . . . . . . . . . . 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 3619	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( -oo (,) ( E ` X ) ) )
346		elioore 11666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -oo (,) ( E ` X ) ) -> x e. RR )
347	346	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. RR )
348	136	adantr 467	. . . . . . . . . . . . . . . . . . . . 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 9690	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR* )
351		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. ( -oo (,) ( E ` X ) ) )
352		iooltub 37610	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( -oo e. RR* /\ ( E ` X ) e. RR* /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
353	349, 350, 351, 352	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
354	347, 348, 353	ltled 9783	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x <_ ( E ` X ) )
355	345, 354	sylan2 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( ( -oo (,) ( E ` X ) ) i^i D ) ) -> x <_ ( E ` X ) )
356	342, 344, 355	syl2anc 667	. . . . . . . . . . . . . . . . . 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 800	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
358	357	adantlr 721	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
359	336, 358	sylan2 477	. . . . . . . . . . . . . . 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 1166	. . . . . . . . . . . . . 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 37605	. . . . . . . . . . . . 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 843	. . . . . . . . . . . 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 2449	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X