Theorem fourierdlem49 37306

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 6306	. . . . . . . . . 10 |- ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
7		fourierdlem49.z	. . . . . . . . . . 11 |- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
8	7	fvmpt2 5941	. . . . . . . . . 10 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
9	6, 8	mpan2 669	. . . . . . . . 9 |- ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
10	9	oveq2d 6294	. . . . . . . 8 |- ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
11	10	mpteq2ia 4477	. . . . . . 7 |- ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
12	5, 11	eqtri 2431	. . . . . 6 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13	1, 2, 3, 4, 12	fourierdlem4 37261	. . . . 5 |- ( ph -> E : RR --> ( A (,] B ) )
14		fourierdlem49.x	. . . . 5 |- ( ph -> X e. RR )
15	13, 14	ffvelrnd 6010	. . . 4 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
16		simpr 459	. . . . . . 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 37259	. . . . . . . . . . . . . 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 210	. . . . . . . . . . . 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 457	. . . . . . . . . . 11 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
24		elmapi 7478	. . . . . . . . . . 11 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
25	23, 24	syl 17	. . . . . . . . . 10 |- ( ph -> Q : ( 0 ... M ) --> RR )
26		ffn 5714	. . . . . . . . . 10 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
27	25, 26	syl 17	. . . . . . . . 9 |- ( ph -> Q Fn ( 0 ... M ) )
28	27	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
29		fvelrnb 5896	. . . . . . . 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 210	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
32		1zzd 10936	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
33		elfzelz 11742	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> j e. ZZ )
34	33	ad2antlr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
35		1e0p1 11047	. . . . . . . . . . . . . . . . 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 11008	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
38		elfzle1 11743	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 0 <_ j )
39	38	ad2antlr 725	. . . . . . . . . . . . . . . . . 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 2410	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
42	41	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
43		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
44	43	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
45	22	simprld 757	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
46	45	simpld 457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( Q ` 0 ) = A )
47	46	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
48	42, 44, 47	3eqtrd 2447	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
49	48	adantllr 717	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
50	49	adantllr 717	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
51	1	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
52	1	rexrd 9673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A e. RR* )
53	52	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
54	2	rexrd 9673	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> B e. RR* )
55	54	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
56		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
57		iocgtlb 36904	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
58	53, 55, 56, 57	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
59	51, 58	gtned 9752	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
60	59	neneqd 2605	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
61	60	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 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 574	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
63	62	neqned 2606	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
64	37, 39, 63	ne0gt0d 9754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
65		0zd 10917	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
66		zltp1le 10954	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
67	65, 34, 66	syl2anc 659	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
68	64, 67	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
69	36, 68	eqbrtrd 4415	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
70		eluz2 11133	. . . . . . . . . . . . . . 15 |- ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
71	32, 34, 69, 70	syl3anbrc 1181	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( ZZ>= ` 1 ) )
72		nnuz 11162	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
73	71, 72	syl6eleqr 2501	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
74		nnm1nn0 10878	. . . . . . . . . . . . 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 11161	. . . . . . . . . . . . 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 2492	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
79	18	nnzd 11007	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
80	79	ad3antrrr 728	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
81		peano2zm 10948	. . . . . . . . . . . . . . 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 11008	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
84	33	zred 11008	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j e. RR )
85		elfzel2 11740	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> M e. ZZ )
86	85	zred 11008	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> M e. RR )
87	84	ltm1d 10518	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
88		elfzle2 11744	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j <_ M )
89	83, 84, 86, 87, 88	ltletrd 9776	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
90	89	ad2antlr 725	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
91		elfzo2 11862	. . . . . . . . . . 11 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
92	78, 80, 90, 91	syl3anbrc 1181	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0..^ M ) )
93	25	ad3antrrr 728	. . . . . . . . . . . . . 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 1177	. . . . . . . . . . . . . . . 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 10896	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
97	83, 86, 89	ltled 9765	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
98	97	ad2antlr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
99	95, 96, 98	jca32 533	. . . . . . . . . . . . . . 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 11733	. . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
102	93, 101	ffvelrnd 6010	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
103	102	rexrd 9673	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
104	25	ffvelrnda 6009	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
105	104	rexrd 9673	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
106	105	adantlr 713	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
107	106	adantr 463	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
108		iocssre 11658	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
109	52, 2, 108	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ph -> ( A (,] B ) C_ RR )
110	109	sselda 3442	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
111	110	rexrd 9673	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
112	111	ad2antrr 724	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
113		simplll 760	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
114		ovex 6306	. . . . . . . . . . . . . . . 16 |- ( j - 1 ) e. _V
115		eleq1 2474	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
116	115	anbi2d 702	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
117		fveq2 5849	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
118		oveq1 6285	. . . . . . . . . . . . . . . . . . 19 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
119	118	fveq2d 5853	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
120	117, 119	breq12d 4408	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
121	116, 120	imbi12d 318	. . . . . . . . . . . . . . . 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 759	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
123	122	r19.21bi 2773	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
124	114, 121, 123	vtocl 3111	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
125	113, 92, 124	syl2anc 659	. . . . . . . . . . . . . 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 11009	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> j e. CC )
127		1cnd 9642	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 1 e. CC )
128	126, 127	npcand 9971	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
129	128	eqcomd 2410	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
130	129	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
131	130	eqcomd 2410	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
132	131	ad2antlr 725	. . . . . . . . . . . . . 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 4419	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
134		simpr 459	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
135	133, 134	breqtrd 4419	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
136	109, 15	sseldd 3443	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E ` X ) e. RR )
137	136	leidd 10159	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
138	137	ad2antrr 724	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
139	41	adantl 464	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
140	138, 139	breqtrd 4419	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
141	140	adantllr 717	. . . . . . . . . . . 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 36911	. . . . . . . . . . 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 6294	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
144	143	ad2antlr 725	. . . . . . . . . . 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 2492	. . . . . . . . . 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 6296	. . . . . . . . . . . 12 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
147	146	eleq2d 2472	. . . . . . . . . . 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 3160	. . . . . . . . . 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 659	. . . . . . . . 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 432	. . . . . . . 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 713	. . . . . . 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 2896	. . . . . 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 724	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
155	25	ad2antrr 724	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
156		iocssicc 11666	. . . . . . . . . 10 |- ( A (,] B ) C_ ( A [,] B )
157	46	eqcomd 2410	. . . . . . . . . . 11 |- ( ph -> A = ( Q ` 0 ) )
158	45	simprd 461	. . . . . . . . . . . 12 |- ( ph -> ( Q ` M ) = B )
159	158	eqcomd 2410	. . . . . . . . . . 11 |- ( ph -> B = ( Q ` M ) )
160	157, 159	oveq12d 6296	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
161	156, 160	syl5sseq 3490	. . . . . . . . 9 |- ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
162	161	sselda 3442	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
163	162	adantr 463	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
164		simpr 459	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
165		fveq2 5849	. . . . . . . . . 10 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
166	165	breq1d 4405	. . . . . . . . 9 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
167	166	cbvrabv 3058	. . . . . . . 8 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
168	167	supeq1i 7940	. . . . . . 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 37282	. . . . . 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 36893	. . . . . . . . 9 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
171	170	sseli 3438	. . . . . . . 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 2879	. . . . . 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 792	. . . 4 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
176	15, 175	mpdan 666	. . 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 5717	. . . . . . . . . . 11 |- ( F : D --> RR -> Rel F )
179	177, 178	syl 17	. . . . . . . . . 10 |- ( ph -> Rel F )
180		resindm 5138	. . . . . . . . . . 11 |- ( Rel F -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( -oo (,) ( E ` X ) ) ) )
181	180	eqcomd 2410	. . . . . . . . . 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 5718	. . . . . . . . . . . 12 |- ( F : D --> RR -> dom F = D )
184	177, 183	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = D )
185	184	ineq2d 3641	. . . . . . . . . 10 |- ( ph -> ( ( -oo (,) ( E ` X ) ) i^i dom F ) = ( ( -oo (,) ( E ` X ) ) i^i D ) )
186	185	reseq2d 5094	. . . . . . . . 9 |- ( ph -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
187	182, 186	eqtrd 2443	. . . . . . . 8 |- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
188	187	3ad2ant1 1018	. . . . . . 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 6293	. . . . . 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 9579	. . . . . . . . . . 11 |- RR C_ CC
191	190	a1i 11	. . . . . . . . . 10 |- ( ph -> RR C_ CC )
192	177, 191	fssd 5723	. . . . . . . . 9 |- ( ph -> F : D --> CC )
193	192	3ad2ant1 1018	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> F : D --> CC )
194		inss2 3660	. . . . . . . . 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 5735	. . . . . . 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 11376	. . . . . . . . . 10 |- -oo e. RR*
198	197	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo e. RR* )
199	25	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
200		elfzofz 11874	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
201	200	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
202	199, 201	ffvelrnd 6010	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
203	202	rexrd 9673	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
204	202	mnfltd 36861	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo < ( Q ` i ) )
205	198, 203, 204	xrltled 36830	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo <_ ( Q ` i ) )
206		iooss1 11617	. . . . . . . . . 10 |- ( ( -oo e. RR* /\ -oo <_ ( Q ` i ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
207	197, 205, 206	sylancr 661	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
208	207	3adant3 1017	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
209		fzofzp1 11946	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
210	209	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
211	199, 210	ffvelrnd 6010	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
212	211	3adant3 1017	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
213	212	rexrd 9673	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
214	202	3adant3 1017	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
215	214	rexrd 9673	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
216		simp3 999	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
217		iocleub 36905	. . . . . . . . . . 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 1230	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
219		iooss2 11618	. . . . . . . . . 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 659	. . . . . . . . 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 21689	. . . . . . . . . . . . 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 5718	. . . . . . . . . . . . 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 5115	. . . . . . . . . . . 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 212	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
227	184	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom F = D )
228	226, 227	sseqtrd 3478	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
229	228	3adant3 1017	. . . . . . . . 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 3452	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
231	208, 230	ssind 3663	. . . . . . 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 3452	. . . . . . . . 9 |- ( ph -> D C_ CC )
234	233	3ad2ant1 1018	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D C_ CC )
235	194, 234	syl5ss 3453	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ CC )
236		eqid 2402	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
237		eqid 2402	. . . . . . 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 1018	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
239	238	rexrd 9673	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR* )
240		iocgtlb 36904	. . . . . . . . . 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 1230	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
242	238	leidd 10159	. . . . . . . . 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 36911	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( E ` X ) ) )
244		snunioo2 36912	. . . . . . . . . . 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 1230	. . . . . . . . . 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 5853	. . . . . . . . 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 21583	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) e. Top
248		ovex 6306	. . . . . . . . . . . . 13 |- ( -oo (,) ( E ` X ) ) e. _V
249	248	inex1 4535	. . . . . . . . . . . 12 |- ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V
250		snex 4632	. . . . . . . . . . . 12 |- { ( E ` X ) } e. _V
251	249, 250	unex 6580	. . . . . . . . . . 11 |- ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V
252		resttop 19954	. . . . . . . . . . 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 670	. . . . . . . . . 10 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top
254		retop 21560	. . . . . . . . . . . . 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 21565	. . . . . . . . . . . . 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 15043	. . . . . . . . . . . 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 1230	. . . . . . . . . . 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 459	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x = ( E ` X ) )
262		pnfxr 11374	. . . . . . . . . . . . . . . . . . . 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 36852	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < +oo )
265	215, 263, 238, 241, 264	eliood 36900	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) +oo ) )
266		snidg 3998	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( E ` X ) e. RR -> ( E ` X ) e. { ( E ` X ) } )
267		elun2 3611	. . . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 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 2490	. . . . . . . . . . . . . . 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 713	. . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
278	136	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( E ` X ) e. RR )
279	278	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR )
280		iocssre 11658	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
281	277, 279, 280	syl2anc 659	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
282		simpr 459	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
283	281, 282	sseldd 3443	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
284	283	3adantl3 1155	. . . . . . . . . . . . . . . . 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 9673	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR* )
286		iocgtlb 36904	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
287	277, 285, 282, 286	syl3anc 1230	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
288	287	3adantl3 1155	. . . . . . . . . . . . . . . . 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 36852	. . . . . . . . . . . . . . . . 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 36900	. . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR* )
294	283	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
295	294	mnfltd 36861	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo < x )
296	136	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
297		iocleub 36905	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
298	277, 285, 282, 297	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
299	298	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x <_ ( E ` X ) )
300		neqne 36810	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. x = ( E ` X ) -> x =/= ( E ` X ) )
301	300	necomd 2674	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = ( E ` X ) -> ( E ` X ) =/= x )
302	301	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) =/= x )
303	294, 296, 299, 302	leneltd 36864	. . . . . . . . . . . . . . . . . . 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 36900	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
305	304	3adantll3 36800	. . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . 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 36800	. . . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . . . . 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 9776	. . . . . . . . . . . . . . . . . . 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 36900	. . . . . . . . . . . . . . . . . 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 3443	. . . . . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . . . 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 3610	. . . . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . 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 792	. . . . . . . . . . . . 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 463	. . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . 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 3628	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
326		elioore 11612	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR )
327	326	rexrd 9673	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . 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 36897	. . . . . . . . . . . . . . . 16 |- ( ( ( Q ` i ) e. RR* /\ +oo e. RR* /\ x e. ( ( Q ` i ) (,) +oo ) ) -> ( Q ` i ) < x )
334	330, 331, 332, 333	syl3anc 1230	. . . . . . . . . . . . . . 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 1155	. . . . . . . . . . . . . 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 3629	. . . . . . . . . . . . . . . 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 3997	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { ( E ` X ) } -> x = ( E ` X ) )
338	337	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x = ( E ` X ) )
339	137	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. { ( E ` X ) } ) -> ( E ` X ) <_ ( E ` X ) )
340	338, 339	eqbrtrd 4415	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
341	340	adantlr 713	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
342		simpll 752	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) /\ -. x e. { ( E ` X ) } ) -> ph )
343		elunnel2 36795	. . . . . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . . . . . . 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 3628	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( -oo (,) ( E ` X ) ) )
346		elioore 11612	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -oo (,) ( E ` X ) ) -> x e. RR )
347	346	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. RR )
348	136	adantr 463	. . . . . . . . . . . . . . . . . . . . 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 9673	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> ( E ` X ) e. RR* )
351		simpr 459	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x e. ( -oo (,) ( E ` X ) ) )
352		iooltub 36916	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( -oo e. RR* /\ ( E ` X ) e. RR* /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
353	349, 350, 351, 352	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x < ( E ` X ) )
354	347, 348, 353	ltled 9765	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( -oo (,) ( E ` X ) ) ) -> x <_ ( E ` X ) )
355	345, 354	sylan2 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( ( -oo (,) ( E ` X ) ) i^i D ) ) -> x <_ ( E ` X ) )
356	342, 344, 355	syl2anc 659	. . . . . . . . . . . . . . . . . 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 792	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
358	357	adantlr 713	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x <_ ( E ` X ) )
359	336, 358	sylan2 472	. . . . . . . . . . . . . . 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 1155	. . . . . . . . . . . . . 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 36911	. . . . . . . . . . . . 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 833	. . . . . . . . . . . 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 2399	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,] ( E ` X )