Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem49 Structured version   Unicode version

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.
StepHypRef 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
87a1i 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
) )
109fvmpt2 5964 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
)  e.  _V )  ->  ( Z `  x
)  =  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )
116, 8, 10syl2anc 661 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( Z `  x )  =  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )
1211oveq2d 6311 . . . . . . . 8  |-  ( x  e.  RR  ->  (
x  +  ( Z `
 x ) )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
1312mpteq2ia 4535 . . . . . . 7  |-  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
145, 13eqtri 2496 . . . . . 6  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
151, 2, 3, 4, 14fourierdlem4 31734 . . . . 5  |-  ( ph  ->  E : RR --> ( A (,] B ) )
16 fourierdlem49.x . . . . 5  |-  ( ph  ->  X  e.  RR )
1715, 16ffvelrnd 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 ) ) ) } )
2221fourierdlem2 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 ) ) ) ) ) )
2320, 22syl 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 ) ) ) ) ) )
2419, 23mpbid 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 ) ) ) ) )
2524simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
26 elmapi 7452 . . . . . . . . . . . 12  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
2725, 26syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
28 ffn 5737 . . . . . . . . . . 11  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
2927, 28syl 16 . . . . . . . . . 10  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
3029ad2antrr 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 ) ) )
3230, 31syl 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 ) ) )
3318, 32mpbid 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
3534a1i 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 )
3736ad2antlr 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 )
3938a1i 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
4140a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  e.  RR )
4237zred 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 )
4443ad2antlr 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 ) )
4645eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Q `  j )  =  ( E `  X )  ->  ( E `  X )  =  ( Q `  j ) )
4746ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( E `  X )  =  ( Q `  j ) )
48 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
4948adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( Q `  j )  =  ( Q `  0 ) )
5024simprld 31320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
5150simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( Q `  0
)  =  A )
5251ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( Q ` 
0 )  =  A )
5347, 49, 523eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( E `  X )  =  A )
5453adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( E `  X )  =  A )
5554adantllr 718 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( E `  X
)  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `
 j )  =  ( E `  X
) )  /\  j  =  0 )  -> 
( E `  X
)  =  A )
561adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  A  e.  RR )
571rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A  e.  RR* )
5857adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  A  e.  RR* )
592rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  RR* )
6059adantr 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
) )
6358, 60, 61, 62syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  A  <  ( E `  X ) )
6456, 63gtned 9731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  =/=  A
)
6564neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  -.  ( E `  X )  =  A )
6665adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  j  e.  ( 0 ... M
) )  ->  -.  ( E `  X )  =  A )
6766ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( E `  X
)  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `
 j )  =  ( E `  X
) )  /\  j  =  0 )  ->  -.  ( E `  X
)  =  A )
6855, 67pm2.65da 576 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  -.  j  =  0 )
6968neqned 2670 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  =/=  0 )
7041, 42, 44, 69leneltd 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
7271a1i 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 ) )
7472, 37, 73syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  <  j  <->  ( 0  +  1 )  <_ 
j ) )
7570, 74mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  +  1 )  <_ 
j )
7639, 75eqbrtrd 4473 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  <_  j )
7735, 37, 763jca 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 ) )
7977, 78sylibr 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 )
8180eqcomi 2480 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= ` 
1 )  =  NN
8281a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( ZZ>= ` 
1 )  =  NN )
8379, 82eleqtrd 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 )
8583, 84syl 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 )
8786a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  NN0  =  (
ZZ>= `  0 ) )
8885, 87eleqtrd 2557 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( ZZ>= `  0 )
)
8920nnzd 10977 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ZZ )
9089ad3antrrr 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 )
9236, 91syl 16 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  ZZ )
9392zred 10978 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  RR )
9436zred 10978 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
95 elfzel2 11698 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
9695zred 10978 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  M  e.  RR )
9794ltm1d 10490 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  j )
98 elfzle2 11702 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
9993, 94, 96, 97, 98ltletrd 9753 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  M )
10099ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( j  -  1 )  <  M )
101100adantllr 718 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  < 
M )
10288, 90, 1013jca 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 ) )
104102, 103sylibr 212 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0..^ M ) )
10527ad3antrrr 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  Q :
( 0 ... M
) --> RR )
10637, 91syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ZZ )
10772, 90, 1063jca 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 ) )
10885nn0ge0d 10867 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  ( j  -  1 ) )
10993, 96, 99ltled 9744 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <_  M )
110109ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  <_  M )
111107, 108, 110jca32 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
) ) )
113111, 112sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0 ... M
) )
114105, 113ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR )
115114rexrd 9655 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR* )
11627ffvelrnda 6032 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR )
117116rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
118117adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
119118adantr 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 )
12157, 2, 120syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A (,] B
)  C_  RR )
122121, 17sseldd 3510 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E `  X
)  e.  RR )
123122adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  RR )
124123rexrd 9655 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  RR* )
125124ad2antrr 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 ) ) )
129128anbi2d 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 ) )
132131fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
133130, 132breq12d 4466 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
134129, 133imbi12d 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 ) ) ) ) )
13524simprrd 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 ) ) )
138135, 136, 137syl2an 477 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
139134, 138vtoclg 3176 . . . . . . . . . . . . . . . . 17  |-  ( ( j  -  1 )  e.  _V  ->  (
( ph  /\  (
j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( ( j  - 
1 )  +  1 ) ) ) )
140127, 139ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
141126, 104, 140syl2anc 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
143142, 94sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
144 ax-1cn 9562 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
145144a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  1  e.  CC )
146143, 145npcand 9946 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  (
( j  -  1 )  +  1 )  =  j )
147146eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  j  =  ( ( j  -  1 )  +  1 ) )
148147fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  j )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
149148eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
150149ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  =  ( Q `  j ) )
151141, 150breqtrd 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 ) )
153151, 152breqtrd 4477 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( E `  X )
)
154122leidd 10131 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E `  X
)  <_  ( E `  X ) )
155154ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( E `  X
)  <_  ( E `  X ) )
15646adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( E `  X
)  =  ( Q `
 j ) )
157155, 156breqtrd 4477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( E `  X
)  <_  ( Q `  j ) )
158157adantllr 718 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
159115, 119, 125, 153, 158eliocd 31430 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 j ) ) )
160148oveq2d 6311 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( Q `  (
j  -  1 ) ) (,] ( Q `
 j ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
161160ad2antlr 726 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( ( Q `  ( j  -  1 ) ) (,] ( Q `  j )
)  =  ( ( Q `  ( j  -  1 ) ) (,] ( Q `  ( ( j  - 
1 )  +  1 ) ) ) )
162161adantllr 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 ) ) ) )
163159, 162eleqtrd 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 ) ) ) )
164130, 132oveq12d 6313 . . . . . . . . . . . . 13  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
165164eleq2d 2537 . . . . . . . . . . . 12  |-  ( i  =  ( j  - 
1 )  ->  (
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  <->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) ) )
166165rspcev 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 ) ) ) )
167104, 163, 166syl2anc 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 ) ) ) )
168167ex 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 ) ) ) ) )
169168adantlr 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 ) ) ) ) )
170169rexlimdva 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 ) ) ) ) )
17133, 170mpd 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 ) ) ) )
17220ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  M  e.  NN )
17327ad2antrr 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 )
175174a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( A (,] B
)  C_  ( A [,] B ) )
17651eqcomd 2475 . . . . . . . . . . . . 13  |-  ( ph  ->  A  =  ( Q `
 0 ) )
17750simprd 463 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  =  B )
178177eqcomd 2475 . . . . . . . . . . . . 13  |-  ( ph  ->  B  =  ( Q `
 M ) )
179176, 178oveq12d 6313 . . . . . . . . . . . 12  |-  ( ph  ->  ( A [,] B
)  =  ( ( Q `  0 ) [,] ( Q `  M ) ) )
180175, 179sseqtrd 3545 . . . . . . . . . . 11  |-  ( ph  ->  ( A (,] B
)  C_  ( ( Q `  0 ) [,] ( Q `  M
) ) )
181180adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( A (,] B )  C_  (
( Q `  0
) [,] ( Q `
 M ) ) )
182181, 61sseldd 3510 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  ( ( Q `  0
) [,] ( Q `
 M ) ) )
183182adantr 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 ) )
186185breq1d 4463 . . . . . . . . . 10  |-  ( k  =  j  ->  (
( Q `  k
)  <  ( E `  X )  <->  ( Q `  j )  <  ( E `  X )
) )
187186cbvrabv 3117 . . . . . . . . 9  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
( E `  X
) }  =  {
j  e.  ( 0..^ M )  |  ( Q `  j )  <  ( E `  X ) }
188187supeq1i 7919 . . . . . . . 8  |-  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  ( E `  X ) } ,  RR ,  <  )  =  sup ( { j  e.  ( 0..^ M )  |  ( Q `
 j )  < 
( E `  X
) } ,  RR ,  <  )
189172, 173, 183, 184, 188fourierdlem25 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 ) ) ) )
192190, 191sseldi 3507 . . . . . . . . 9  |-  ( ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
193192a1i 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 ) ) ) ) )
194193reximdva 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 ) ) ) ) )
195189, 194mpd 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 ) ) ) )
196171, 195pm2.61dan 789 . . . . 5  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
197196ex 434 . . . 4  |-  ( ph  ->  ( ( E `  X )  e.  ( A (,] B )  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) ) )
19817, 197mpd 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 )
201199, 200syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Rel  F )
202 resindm 5324 . . . . . . . . . . . 12  |-  ( Rel 
F  ->  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  dom  F
) )  =  ( F  |`  ( -oo (,) ( E `  X
) ) ) )
203202eqcomd 2475 . . . . . . . . . . 11  |-  ( Rel 
F  ->  ( F  |`  ( -oo (,) ( E `  X )
) )  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i 
dom  F ) ) )
204201, 203syl 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 )
206199, 205syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  dom  F  =  D )
207206ineq2d 3705 . . . . . . . . . . 11  |-  ( ph  ->  ( ( -oo (,) ( E `  X ) )  i^i  dom  F
)  =  ( ( -oo (,) ( E `
 X ) )  i^i  D ) )
208207reseq2d 5279 . . . . . . . . . 10  |-  ( ph  ->  ( F  |`  (
( -oo (,) ( E `
 X ) )  i^i  dom  F )
)  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  D ) ) )
209204, 208eqtrd 2508 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( -oo (,) ( E `  X ) ) )  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  D ) ) )
2102093ad2ant1 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 ) ) )
211210oveq1d 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 ) ) )
212142a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  CC )
213199, 212fssd 5746 . . . . . . . . . . 11  |-  ( ph  ->  F : D --> CC )
2142133ad2ant1 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
216215a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( -oo (,) ( E `  X ) )  i^i  D ) 
C_  D )
217214, 216fssresd 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*
219218a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  e.  RR* )
22027adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
221 elfzofz 11823 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
222221adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
223220, 222ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
224223rexrd 9655 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
225223mnfltd 31391 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <  ( Q `
 i ) )
226219, 224, 225xrltled 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 ) ) )
228219, 226, 227syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( E `  X
) )  C_  ( -oo (,) ( E `  X ) ) )
2292283adant3 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
) )
231230adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
232220, 231ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2332323adant3 1016 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
234233rexrd 9655 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
2352233adant3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
236235rexrd 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 ) ) )
239236, 234, 237, 238syl3anc 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 ) ) ) )
241234, 239, 240syl2anc 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 ) ) ) )
245242, 243, 2443syl 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 ) ) ) )
247245, 246sylibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
248206adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  F  =  D )
249247, 248sseqtrd 3545 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
2502493adant3 1016 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
251241, 250sstrd 3519 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( E `  X )
)  C_  D )
252229, 251ssind 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 )
254253, 212sstrd 3519 . . . . . . . . . . 11  |-  ( ph  ->  D  C_  CC )
2552543ad2ant1 1017 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  D  C_  CC )
256216, 255sstrd 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 ) } ) )
259122adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( E `  X )  e.  RR )
2602593adant3 1016 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR )
261260rexrd 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
) )
263236, 234, 237, 262syl3anc 1228 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( E `  X ) )
264260leidd 10131 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( E `  X ) )
265236, 261, 261, 263, 264eliocd 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 ) ) )
267236, 261, 263, 266syl3anc 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 )
) )
268267fveq2d 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 ) ) ) )
269257cnfldtop 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 )
272270, 271ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( -oo (,) ( E `
 X ) )  i^i  D )  e. 
_V
273 snex 4694 . . . . . . . . . . . . . . 15  |-  { ( E `  X ) }  e.  _V
274272, 273unex 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 )
276269, 274, 275mp2an 672 . . . . . . . . . . . . 13  |-  ( (
TopOpen ` fld )t  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  e. 
Top
277276a1i 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*
280279a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> +oo  e.  RR* )
281260ltpnfd 31380 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  < +oo )
282236, 280, 260, 263, 281eliood 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 ) } ) )
285283, 284syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( E `  X )  e.  RR  ->  ( E `  X )  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )
286122, 285syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( E `  X
)  e.  ( ( ( -oo (,) ( E `  X )
)  i^i  D )  u.  { ( E `  X ) } ) )
2872863ad2ant1 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 ) } ) )
288282, 287jca 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 ) } ) ) )
290288, 289sylibr 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 ) } ) ) )
291290adantr 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 ) } ) ) )
292278, 291eqeltrd 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 ) } ) ) )
293292adantlr 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 ) } ) ) )
294236adantr 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* )
295279a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  -> +oo  e.  RR* )
296224adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  e.  RR* )
297259adantr 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 )
299296, 297, 298syl2anc 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 )
) )
301299, 300sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  RR )
3023013adantl3 1154 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  RR )
303297rexrd 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 )
305296, 303, 300, 304syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  <  x )
3063053adantl3 1154 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  <  x )
307302ltpnfd 31380 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  < +oo )
308294, 295, 302, 306, 307eliood 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 ) )
309308adantr 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 ) )
310218a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  -> -oo  e.  RR* )
311303adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  ( E `  X )  e.  RR* )
312301adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  e.  RR )
313312mnfltd 31391 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  -> -oo  <  x
)
314297adantr 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
) )
316296, 303, 300, 315syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  <_  ( E `  X
) )
317316adantr 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 ) )
319318necomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  x  =  ( E `
 X )  -> 
( E `  X
)  =/=  x )
320319adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  ( E `  X )  =/=  x
)
321312, 314, 317, 320leneltd 31394 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  <  ( E `  X ) )
322310, 311, 312, 313, 321eliood 31418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  e.  ( -oo (,) ( E `
 X ) ) )
3233223adantll3 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
) ) )
324250ad2antrr 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 )
325294adantr 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* )
326234ad2antrr 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* )
327302adantr 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 )
328306adantr 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 )
329260ad2antrr 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 )
330233ad2antrr 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 )
3313213adantll3 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 ) )
332239ad2antrr 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 ) ) )
333327, 329, 330, 331, 332ltletrd 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 ) ) )
334325, 326, 327, 328, 333eliood 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 ) ) ) )
335324, 334sseldd 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 )
336323, 335jca 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 ) )
338336, 337sylibr 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 ) } ) )
340338, 339syl 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 ) } ) )
341309, 340jca 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 ) } ) ) )
343341, 342sylibr 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 ) } ) ) )
344293, 343pm2.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 ) } ) ) )
345236adantr 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* )
346261adantr 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* )
347342simplbi 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 )
349348rexrd 9655 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( Q `
 i ) (,) +oo )  ->  x  e. 
RR* )
350347, 349syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( ( ( Q `  i ) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  ->  x  e.  RR* )
351350adantl 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* )
352224adantr 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* )
353279a1i 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* )
354347adantl 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 )
356352, 353, 354, 355syl3anc 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 )
3573563adantl3 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 ) ) )
359342simprbi 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 ) } ) )
360359adantl 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 ) )
362361adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  { ( E `  X
) } )  ->  x  =  ( E `  X ) )
363154adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  { ( E `  X
) } )  -> 
( E `  X
)  <_  ( E `  X ) )
364362, 363eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  { ( E `  X
) } )  ->  x  <_  ( E `  X ) )
365364adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( (