Theorem fourierdlem49 31779

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		id 22	. . . . . . . . . 10 |- ( x e. RR -> x e. RR )
7		ovex 6320	. . . . . . . . . . 11 |- ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V
8	7	a1i 11	. . . . . . . . . 10 |- ( x e. RR -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V )
9		fourierdlem49.z	. . . . . . . . . . 11 |- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
10	9	fvmpt2 5964	. . . . . . . . . 10 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. _V ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
11	6, 8, 10	syl2anc 661	. . . . . . . . 9 |- ( x e. RR -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
12	11	oveq2d 6311	. . . . . . . 8 |- ( x e. RR -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13	12	mpteq2ia 4535	. . . . . . 7 |- ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
14	5, 13	eqtri 2496	. . . . . 6 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
15	1, 2, 3, 4, 14	fourierdlem4 31734	. . . . 5 |- ( ph -> E : RR --> ( A (,] B ) )
16		fourierdlem49.x	. . . . 5 |- ( ph -> X e. RR )
17	15, 16	ffvelrnd 6033	. . . 4 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
18		simpr 461	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
19		fourierdlem49.q	. . . . . . . . . . . . . 14 |- ( ph -> Q e. ( P ` M ) )
20		fourierdlem49.m	. . . . . . . . . . . . . . 15 |- ( ph -> M e. NN )
21		fourierdlem49.p	. . . . . . . . . . . . . . . 16 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
22	21	fourierdlem2 31732	. . . . . . . . . . . . . . 15 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
23	20, 22	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
24	19, 23	mpbid 210	. . . . . . . . . . . . 13 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
25	24	simpld 459	. . . . . . . . . . . 12 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
26		elmapi 7452	. . . . . . . . . . . 12 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
27	25, 26	syl 16	. . . . . . . . . . 11 |- ( ph -> Q : ( 0 ... M ) --> RR )
28		ffn 5737	. . . . . . . . . . 11 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
29	27, 28	syl 16	. . . . . . . . . 10 |- ( ph -> Q Fn ( 0 ... M ) )
30	29	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
31		fvelrnb 5921	. . . . . . . . 9 |- ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
32	30, 31	syl 16	. . . . . . . 8 |- ( ( ( 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 ) ) )
33	18, 32	mpbid 210	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
34		1z 10906	. . . . . . . . . . . . . . . . . . 19 |- 1 e. ZZ
35	34	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
36		elfzelz 11700	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> j e. ZZ )
37	36	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
38		1e0p1 11016	. . . . . . . . . . . . . . . . . . . 20 |- 1 = ( 0 + 1 )
39	38	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 = ( 0 + 1 ) )
40		0re 9608	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. RR
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. RR )
42	37	zred 10978	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
43		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. ( 0 ... M ) -> 0 <_ j )
44	43	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ j )
45		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
46	45	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
47	46	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = ( Q ` j ) )
48		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
49	48	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
50	24	simprld 31320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
51	50	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( Q ` 0 ) = A )
52	51	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( Q ` 0 ) = A )
53	47, 49, 52	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
54	53	adantllr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
55	54	adantllr 718	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> ( E ` X ) = A )
56	1	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR )
57	1	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> A e. RR* )
58	57	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A e. RR* )
59	2	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> B e. RR* )
60	59	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> B e. RR* )
61		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( A (,] B ) )
62		iocgtlb 31422	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
63	58, 60, 61, 62	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
64	56, 63	gtned 9731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) =/= A )
65	64	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> -. ( E ` X ) = A )
66	65	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> -. ( E ` X ) = A )
67	66	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) /\ j = 0 ) -> -. ( E ` X ) = A )
68	55, 67	pm2.65da 576	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> -. j = 0 )
69	68	neqned 2670	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j =/= 0 )
70	41, 42, 44, 69	leneltd 31394	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
71		0z 10887	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. ZZ
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
73		zltp1le 10924	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
74	72, 37, 73	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> ( 0 + 1 ) <_ j ) )
75	70, 74	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 + 1 ) <_ j )
76	39, 75	eqbrtrd 4473	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 <_ j )
77	35, 37, 76	3jca 1176	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
78		eluz2 11100	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ j e. ZZ /\ 1 <_ j ) )
79	77, 78	sylibr 212	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( ZZ>= ` 1 ) )
80		nnuz 11129	. . . . . . . . . . . . . . . . . 18 |- NN = ( ZZ>= ` 1 )
81	80	eqcomi 2480	. . . . . . . . . . . . . . . . 17 |- ( ZZ>= ` 1 ) = NN
82	81	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ZZ>= ` 1 ) = NN )
83	79, 82	eleqtrd 2557	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. NN )
84		nnm1nn0 10849	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( j - 1 ) e. NN0 )
85	83, 84	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. NN0 )
86		nn0uz 11128	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
87	86	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> NN0 = ( ZZ>= ` 0 ) )
88	85, 87	eleqtrd 2557	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
89	20	nnzd 10977	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
90	89	ad3antrrr 729	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
91		peano2zm 10918	. . . . . . . . . . . . . . . . . 18 |- ( j e. ZZ -> ( j - 1 ) e. ZZ )
92	36, 91	syl 16	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. ZZ )
93	92	zred 10978	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
94	36	zred 10978	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> j e. RR )
95		elfzel2 11698	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> M e. ZZ )
96	95	zred 10978	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> M e. RR )
97	94	ltm1d 10490	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
98		elfzle2 11702	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> j <_ M )
99	93, 94, 96, 97, 98	ltletrd 9753	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
100	99	ad2antlr 726	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
101	100	adantllr 718	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
102	88, 90, 101	3jca 1176	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
103		elfzo2 11812	. . . . . . . . . . . 12 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
104	102, 103	sylibr 212	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0..^ M ) )
105	27	ad3antrrr 729	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
106	37, 91	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
107	72, 90, 106	3jca 1176	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) )
108	85	nn0ge0d 10867	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
109	93, 96, 99	ltled 9744	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
110	109	ad2antlr 726	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
111	107, 108, 110	jca32 535	. . . . . . . . . . . . . . . 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 ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
112		elfz2 11691	. . . . . . . . . . . . . . . 16 |- ( ( j - 1 ) e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
113	111, 112	sylibr 212	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
114	105, 113	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
115	114	rexrd 9655	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
116	27	ffvelrnda 6032	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
117	116	rexrd 9655	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
118	117	adantlr 714	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
119	118	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
120		iocssre 11616	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
121	57, 2, 120	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A (,] B ) C_ RR )
122	121, 17	sseldd 3510	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E ` X ) e. RR )
123	122	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR )
124	123	rexrd 9655	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. RR* )
125	124	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
126		simplll 757	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
127		ovex 6320	. . . . . . . . . . . . . . . . 17 |- ( j - 1 ) e. _V
128		eleq1 2539	. . . . . . . . . . . . . . . . . . . 20 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
129	128	anbi2d 703	. . . . . . . . . . . . . . . . . . 19 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
130		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
131		oveq1 6302	. . . . . . . . . . . . . . . . . . . . 21 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
132	131	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
133	130, 132	breq12d 4466	. . . . . . . . . . . . . . . . . . 19 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
134	129, 133	imbi12d 320	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) )
135	24	simprrd 31328	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
136		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( 0..^ M ) -> i e. ( 0..^ M ) )
137		rspa 2834	. . . . . . . . . . . . . . . . . . 19 |- ( ( A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
138	135, 136, 137	syl2an 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
139	134, 138	vtoclg 3176	. . . . . . . . . . . . . . . . 17 |- ( ( j - 1 ) e. _V -> ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
140	127, 139	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
141	126, 104, 140	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
142		ax-resscn 9561	. . . . . . . . . . . . . . . . . . . . 21 |- RR C_ CC
143	142, 94	sseldi 3507	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 0 ... M ) -> j e. CC )
144		ax-1cn 9562	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. CC
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 0 ... M ) -> 1 e. CC )
146	143, 145	npcand 9946	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
147	146	eqcomd 2475	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
148	147	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
149	148	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
150	149	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
151	141, 150	breqtrd 4477	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
152		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
153	151, 152	breqtrd 4477	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
154	122	leidd 10131	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
155	154	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
156	46	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
157	155, 156	breqtrd 4477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
158	157	adantllr 718	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
159	115, 119, 125, 153, 158	eliocd 31430	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) )
160	148	oveq2d 6311	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
161	160	ad2antlr 726	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( Q ` ( j - 1 ) ) (,] ( Q ` j ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
162	161	adantllr 718	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
163	159, 162	eleqtrd 2557	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ j e. ( 0 ... M ) ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
164	130, 132	oveq12d 6313	. . . . . . . . . . . . 13 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
165	164	eleq2d 2537	. . . . . . . . . . . 12 |- ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
166	165	rspcev 3219	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
167	104, 163, 166	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
168	167	ex 434	. . . . . . . . 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 ) ) ) ) )
169	168	adantlr 714	. . . . . . . 8 |- ( ( ( ( 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 ) ) ) ) )
170	169	rexlimdva 2959	. . . . . . 7 |- ( ( ( 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 ) ) ) ) )
171	33, 170	mpd 15	. . . . . 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 ) ) ) )
172	20	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
173	27	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
174		iocssicc 11624	. . . . . . . . . . . . 13 |- ( A (,] B ) C_ ( A [,] B )
175	174	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( A (,] B ) C_ ( A [,] B ) )
176	51	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ph -> A = ( Q ` 0 ) )
177	50	simprd 463	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` M ) = B )
178	177	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ph -> B = ( Q ` M ) )
179	176, 178	oveq12d 6313	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
180	175, 179	sseqtrd 3545	. . . . . . . . . . 11 |- ( ph -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
181	180	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( A (,] B ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) ) )
182	181, 61	sseldd 3510	. . . . . . . . 9 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
183	182	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
184		simpr 461	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
185		fveq2 5872	. . . . . . . . . . 11 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
186	185	breq1d 4463	. . . . . . . . . 10 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
187	186	cbvrabv 3117	. . . . . . . . 9 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
188	187	supeq1i 7919	. . . . . . . 8 |- sup ( { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
189	172, 173, 183, 184, 188	fourierdlem25 31755	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
190		ioossioc 31411	. . . . . . . . . 10 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
191		id 22	. . . . . . . . . 10 |- ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
192	190, 191	sseldi 3507	. . . . . . . . 9 |- ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
193	192	a1i 11	. . . . . . . 8 |- ( ( ( ( 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 ) ) ) ) )
194	193	reximdva 2942	. . . . . . 7 |- ( ( ( 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 ) ) ) ) )
195	189, 194	mpd 15	. . . . . 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 ) ) ) )
196	171, 195	pm2.61dan 789	. . . . 5 |- ( ( ph /\ ( E ` X ) e. ( A (,] B ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
197	196	ex 434	. . . 4 |- ( ph -> ( ( E ` X ) e. ( A (,] B ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
198	17, 197	mpd 15	. . 3 |- ( ph -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
199		fourierdlem49.f	. . . . . . . . . . . 12 |- ( ph -> F : D --> RR )
200		frel 5740	. . . . . . . . . . . 12 |- ( F : D --> RR -> Rel F )
201	199, 200	syl 16	. . . . . . . . . . 11 |- ( ph -> Rel F )
202		resindm 5324	. . . . . . . . . . . 12 |- ( Rel F -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( -oo (,) ( E ` X ) ) ) )
203	202	eqcomd 2475	. . . . . . . . . . 11 |- ( Rel F -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) )
204	201, 203	syl 16	. . . . . . . . . 10 |- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) )
205		fdm 5741	. . . . . . . . . . . . 13 |- ( F : D --> RR -> dom F = D )
206	199, 205	syl 16	. . . . . . . . . . . 12 |- ( ph -> dom F = D )
207	206	ineq2d 3705	. . . . . . . . . . 11 |- ( ph -> ( ( -oo (,) ( E ` X ) ) i^i dom F ) = ( ( -oo (,) ( E ` X ) ) i^i D ) )
208	207	reseq2d 5279	. . . . . . . . . 10 |- ( ph -> ( F |` ( ( -oo (,) ( E ` X ) ) i^i dom F ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
209	204, 208	eqtrd 2508	. . . . . . . . 9 |- ( ph -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
210	209	3ad2ant1 1017	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( -oo (,) ( E ` X ) ) ) = ( F |` ( ( -oo (,) ( E ` X ) ) i^i D ) ) )
211	210	oveq1d 6310	. . . . . . 7 |- ( ( 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 ) ) )
212	142	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR C_ CC )
213	199, 212	fssd 5746	. . . . . . . . . . 11 |- ( ph -> F : D --> CC )
214	213	3ad2ant1 1017	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> F : D --> CC )
215		inss2 3724	. . . . . . . . . . 11 |- ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D
216	215	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ D )
217	214, 216	fssresd 5758	. . . . . . . . 9 |- ( ( 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 )
218		mnfxr 11335	. . . . . . . . . . . . 13 |- -oo e. RR*
219	218	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo e. RR* )
220	27	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
221		elfzofz 11823	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
222	221	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
223	220, 222	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
224	223	rexrd 9655	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
225	223	mnfltd 31391	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo < ( Q ` i ) )
226	219, 224, 225	xrltled 31356	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -oo <_ ( Q ` i ) )
227		iooss1 11576	. . . . . . . . . . . 12 |- ( ( -oo e. RR* /\ -oo <_ ( Q ` i ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
228	219, 226, 227	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
229	228	3adant3 1016	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( -oo (,) ( E ` X ) ) )
230		fzofzp1 11889	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
231	230	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
232	220, 231	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
233	232	3adant3 1016	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
234	233	rexrd 9655	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
235	223	3adant3 1016	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
236	235	rexrd 9655	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
237		simp3 998	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
238		iocleub 31423	. . . . . . . . . . . . 13 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
239	236, 234, 237, 238	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
240		iooss2 11577	. . . . . . . . . . . 12 |- ( ( ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) <_ ( Q ` ( i + 1 ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
241	234, 239, 240	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
242		fourierdlem49.cn	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
243		cncff 21265	. . . . . . . . . . . . . . 15 |- ( ( 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 )
244		fdm 5741	. . . . . . . . . . . . . . 15 |- ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
245	242, 243, 244	3syl 20	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
246		ssdmres 5301	. . . . . . . . . . . . . 14 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
247	245, 246	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
248	206	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom F = D )
249	247, 248	sseqtrd 3545	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
250	249	3adant3 1016	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
251	241, 250	sstrd 3519	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ D )
252	229, 251	ssind 3727	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( E ` X ) ) C_ ( ( -oo (,) ( E ` X ) ) i^i D ) )
253		fourierdlem49.d	. . . . . . . . . . . 12 |- ( ph -> D C_ RR )
254	253, 212	sstrd 3519	. . . . . . . . . . 11 |- ( ph -> D C_ CC )
255	254	3ad2ant1 1017	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> D C_ CC )
256	216, 255	sstrd 3519	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( -oo (,) ( E ` X ) ) i^i D ) C_ CC )
257		eqid 2467	. . . . . . . . 9 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
258		eqid 2467	. . . . . . . . 9 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
259	122	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( E ` X ) e. RR )
260	259	3adant3 1016	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
261	260	rexrd 9655	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR* )
262		iocgtlb 31422	. . . . . . . . . . . 12 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
263	236, 234, 237, 262	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
264	260	leidd 10131	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( E ` X ) )
265	236, 261, 261, 263, 264	eliocd 31430	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( E ` X ) ) )
266		snunioo2 31431	. . . . . . . . . . . . 13 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ ( Q ` i ) < ( E ` X ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
267	236, 261, 263, 266	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) (,) ( E ` X ) ) u. { ( E ` X ) } ) = ( ( Q ` i ) (,] ( E ` X ) ) )
268	267	fveq2d 5876	. . . . . . . . . . 11 |- ( ( 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 ) ) ) )
269	257	cnfldtop 21159	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. Top
270		ovex 6320	. . . . . . . . . . . . . . . 16 |- ( -oo (,) ( E ` X ) ) e. _V
271		inex1g 4596	. . . . . . . . . . . . . . . 16 |- ( ( -oo (,) ( E ` X ) ) e. _V -> ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V )
272	270, 271	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( -oo (,) ( E ` X ) ) i^i D ) e. _V
273		snex 4694	. . . . . . . . . . . . . . 15 |- { ( E ` X ) } e. _V
274	272, 273	unex 6593	. . . . . . . . . . . . . 14 |- ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) e. _V
275		resttop 19529	. . . . . . . . . . . . . 14 |- ( ( ( 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 )
276	269, 274, 275	mp2an 672	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top
277	276	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) e. Top )
278		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( E ` X ) ) -> x = ( E ` X ) )
279		pnfxr 11333	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- +oo e. RR*
280	279	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> +oo e. RR* )
281	260	ltpnfd 31380	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < +oo )
282	236, 280, 260, 263, 281	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) +oo ) )
283		snidg 4059	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( E ` X ) e. RR -> ( E ` X ) e. { ( E ` X ) } )
284		elun2 3677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( E ` X ) e. { ( E ` X ) } -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
285	283, 284	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( E ` X ) e. RR -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
286	122, 285	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
287	286	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) } ) )
288	282, 287	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) +oo ) /\ ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
289		elin 3692	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( E ` X ) e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) <-> ( ( E ` X ) e. ( ( Q ` i ) (,) +oo ) /\ ( E ` X ) e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
290	288, 289	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) } ) ) )
291	290	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) } ) ) )
292	278, 291	eqeltrd 2555	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) } ) ) )
293	292	adantlr 714	. . . . . . . . . . . . . . . . . 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 ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
294	236	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
295	279	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> +oo e. RR* )
296	224	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) e. RR* )
297	259	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR )
298		iocssre 11616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
299	296, 297, 298	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( ( Q ` i ) (,] ( E ` X ) ) C_ RR )
300		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,] ( E ` X ) ) )
301	299, 300	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
302	301	3adantl3 1154	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. RR )
303	297	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( E ` X ) e. RR* )
304		iocgtlb 31422	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
305	296, 303, 300, 304	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
306	305	3adantl3 1154	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> ( Q ` i ) < x )
307	302	ltpnfd 31380	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x < +oo )
308	294, 295, 302, 306, 307	eliood 31418	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
309	308	adantr 465	. . . . . . . . . . . . . . . . . . . 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. ( ( Q ` i ) (,) +oo ) )
310	218	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo e. RR* )
311	303	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR* )
312	301	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. RR )
313	312	mnfltd 31391	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> -oo < x )
314	297	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) e. RR )
315		iocleub 31423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( Q ` i ) e. RR* /\ ( E ` X ) e. RR* /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
316	296, 303, 300, 315	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) -> x <_ ( E ` X ) )
317	316	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x <_ ( E ` X ) )
318		neqne 31339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -. x = ( E ` X ) -> x =/= ( E ` X ) )
319	318	necomd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. x = ( E ` X ) -> ( E ` X ) =/= x )
320	319	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> ( E ` X ) =/= x )
321	312, 314, 317, 320	leneltd 31394	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x < ( E ` X ) )
322	310, 311, 312, 313, 321	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( Q ` i ) (,] ( E ` X ) ) ) /\ -. x = ( E ` X ) ) -> x e. ( -oo (,) ( E ` X ) ) )
323	322	3adantll3 31324	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) )
324	250	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 )
325	294	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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* )
326	234	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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* )
327	302	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 )
328	306	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 )
329	260	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 )
330	233	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 )
331	321	3adantll3 31324	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) )
332	239	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) ) )
333	327, 329, 330, 331, 332	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) )
334	325, 326, 327, 328, 333	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) )
335	324, 334	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 )
336	323, 335	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) /\ x e. D ) )
337		elin 3692	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) <-> ( x e. ( -oo (,) ( E ` X ) ) /\ x e. D ) )
338	336, 337	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) )
339		elun1 3676	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( ( -oo (,) ( E ` X ) ) i^i D ) -> x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
340	338, 339	syl 16	. . . . . . . . . . . . . . . . . . . 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. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) )
341	309, 340	jca 532	. . . . . . . . . . . . . . . . . . 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. ( ( Q ` i ) (,) +oo ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
342		elin 3692	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) <-> ( x e. ( ( Q ` i ) (,) +oo ) /\ x e. ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
343	341, 342	sylibr 212	. . . . . . . . . . . . . . . . . 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 ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) )
344	293, 343	pm2.61dan 789	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) } ) ) )
345	236	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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* )
346	261	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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* )
347	342	simplbi 460	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. ( ( Q ` i ) (,) +oo ) )
348		elioore 11571	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR )
349	348	rexrd 9655	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( ( Q ` i ) (,) +oo ) -> x e. RR* )
350	347, 349	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) -> x e. RR* )
351	350	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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* )
352	224	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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* )
353	279	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> +oo e. RR* )
354	347	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) )
355		ioogtlb 31415	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Q ` i ) e. RR* /\ +oo e. RR* /\ x e. ( ( Q ` i ) (,) +oo ) ) -> ( Q ` i ) < x )
356	352, 353, 354, 355	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( Q ` i ) < x )
357	356	3adantl3 1154	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 )
358		simpl 457	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( ( Q ` i ) (,) +oo ) i^i ( ( ( -oo (,) ( E ` X ) ) i^i D ) u. { ( E ` X ) } ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
359	342	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) } ) )
360	359	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ 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 ) } ) )
361		elsni 4058	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. { ( E ` X ) } -> x = ( E ` X ) )
362	361	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x = ( E ` X ) )
363	154	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. { ( E ` X ) } ) -> ( E ` X ) <_ ( E ` X ) )
364	362, 363	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. { ( E ` X ) } ) -> x <_ ( E ` X ) )
365	364	adantlr 714	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( (