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

Theorem fourierdlem49 37306
Description: The given periodic function  F has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem49.a  |-  ( ph  ->  A  e.  RR )
fourierdlem49.b  |-  ( ph  ->  B  e.  RR )
fourierdlem49.altb  |-  ( ph  ->  A  <  B )
fourierdlem49.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem49.t  |-  T  =  ( B  -  A
)
fourierdlem49.m  |-  ( ph  ->  M  e.  NN )
fourierdlem49.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem49.d  |-  ( ph  ->  D  C_  RR )
fourierdlem49.f  |-  ( ph  ->  F : D --> RR )
fourierdlem49.dper  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T
) )  e.  D
)
fourierdlem49.per  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( F `  ( x  +  (
k  x.  T ) ) )  =  ( F `  x ) )
fourierdlem49.cn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem49.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem49.x  |-  ( ph  ->  X  e.  RR )
fourierdlem49.z  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
fourierdlem49.e  |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )
Assertion
Ref Expression
fourierdlem49  |-  ( ph  ->  ( ( F  |`  ( -oo (,) X ) ) lim CC  X )  =/=  (/) )
Distinct variable groups:    A, i, m, p    x, A, i    B, i, k    B, m, p    x, B, k    D, k, x    i, E, k, x    i, F, k, x    i, M, k    m, M, p   
x, M    Q, i,
k    Q, p    x, Q    T, k, x    i, X, k, x    k, Z, x    ph, i, k, x
Allowed substitution hints:    ph( m, p)    A( k)    D( i, m, p)    P( x, i, k, m, p)    Q( m)    T( i, m, p)    E( m, p)    F( m, p)    L( x, i, k, m, p)    X( m, p)    Z( i, m, p)

Proof of Theorem fourierdlem49
Dummy variables  j 
y  z are mutually distinct and distinct from all other variables.
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 ovex 6306 . . . . . . . . . 10  |-  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e. 
_V
7 fourierdlem49.z . . . . . . . . . . 11  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
87fvmpt2 5941 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
)  e.  _V )  ->  ( Z `  x
)  =  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )
96, 8mpan2 669 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( Z `  x )  =  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )
109oveq2d 6294 . . . . . . . 8  |-  ( x  e.  RR  ->  (
x  +  ( Z `
 x ) )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
1110mpteq2ia 4477 . . . . . . 7  |-  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
125, 11eqtri 2431 . . . . . 6  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
131, 2, 3, 4, 12fourierdlem4 37261 . . . . 5  |-  ( ph  ->  E : RR --> ( A (,] B ) )
14 fourierdlem49.x . . . . 5  |-  ( ph  ->  X  e.  RR )
1513, 14ffvelrnd 6010 . . . 4  |-  ( ph  ->  ( E `  X
)  e.  ( A (,] B ) )
16 simpr 459 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  ( E `  X )  e.  ran  Q )  -> 
( E `  X
)  e.  ran  Q
)
17 fourierdlem49.q . . . . . . . . . . . . 13  |-  ( ph  ->  Q  e.  ( P `
 M ) )
18 fourierdlem49.m . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  NN )
19 fourierdlem49.p . . . . . . . . . . . . . . 15  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
2019fourierdlem2 37259 . . . . . . . . . . . . . 14  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
2118, 20syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
2217, 21mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
2322simpld 457 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
24 elmapi 7478 . . . . . . . . . . 11  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
2523, 24syl 17 . . . . . . . . . 10  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
26 ffn 5714 . . . . . . . . . 10  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
2725, 26syl 17 . . . . . . . . 9  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
2827ad2antrr 724 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  ( E `  X )  e.  ran  Q )  ->  Q  Fn  ( 0 ... M ) )
29 fvelrnb 5896 . . . . . . . 8  |-  ( Q  Fn  ( 0 ... M )  ->  (
( E `  X
)  e.  ran  Q  <->  E. j  e.  ( 0 ... M ) ( Q `  j )  =  ( E `  X ) ) )
3028, 29syl 17 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  ( E `  X )  e.  ran  Q )  -> 
( ( E `  X )  e.  ran  Q  <->  E. j  e.  (
0 ... M ) ( Q `  j )  =  ( E `  X ) ) )
3116, 30mpbid 210 . . . . . 6  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  ( E `  X )  e.  ran  Q )  ->  E. j  e.  (
0 ... M ) ( Q `  j )  =  ( E `  X ) )
32 1zzd 10936 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  e.  ZZ )
33 elfzelz 11742 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
3433ad2antlr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  ZZ )
35 1e0p1 11047 . . . . . . . . . . . . . . . . 17  |-  1  =  ( 0  +  1 )
3635a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  =  ( 0  +  1 ) )
3734zred 11008 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  RR )
38 elfzle1 11743 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
3938ad2antlr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  j )
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Q `  j )  =  ( E `  X )  ->  ( Q `  j )  =  ( E `  X ) )
4140eqcomd 2410 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Q `  j )  =  ( E `  X )  ->  ( E `  X )  =  ( Q `  j ) )
4241ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( E `  X )  =  ( Q `  j ) )
43 fveq2 5849 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
4443adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( Q `  j )  =  ( Q `  0 ) )
4522simprld 757 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
4645simpld 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( Q `  0
)  =  A )
4746ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( Q ` 
0 )  =  A )
4842, 44, 473eqtrd 2447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( E `  X )  =  A )
4948adantllr 717 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  ( Q `  j )  =  ( E `  X ) )  /\  j  =  0 )  ->  ( E `  X )  =  A )
5049adantllr 717 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( E `  X
)  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `
 j )  =  ( E `  X
) )  /\  j  =  0 )  -> 
( E `  X
)  =  A )
511adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  A  e.  RR )
521rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  e.  RR* )
5352adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  A  e.  RR* )
542rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  RR* )
5554adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  B  e.  RR* )
56 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  ( A (,] B ) )
57 iocgtlb 36904 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 X )  e.  ( A (,] B
) )  ->  A  <  ( E `  X
) )
5853, 55, 56, 57syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  A  <  ( E `  X ) )
5951, 58gtned 9752 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  =/=  A
)
6059neneqd 2605 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  -.  ( E `  X )  =  A )
6160ad3antrrr 728 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( E `  X
)  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `
 j )  =  ( E `  X
) )  /\  j  =  0 )  ->  -.  ( E `  X
)  =  A )
6250, 61pm2.65da 574 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  -.  j  =  0 )
6362neqned 2606 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  =/=  0 )
6437, 39, 63ne0gt0d 9754 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <  j )
65 0zd 10917 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  e.  ZZ )
66 zltp1le 10954 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  ZZ  /\  j  e.  ZZ )  ->  ( 0  <  j  <->  ( 0  +  1 )  <_  j ) )
6765, 34, 66syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  <  j  <->  ( 0  +  1 )  <_ 
j ) )
6864, 67mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  +  1 )  <_ 
j )
6936, 68eqbrtrd 4415 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  <_  j )
70 eluz2 11133 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  j  e.  ZZ  /\  1  <_ 
j ) )
7132, 34, 69, 70syl3anbrc 1181 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  ( ZZ>= `  1 )
)
72 nnuz 11162 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
7371, 72syl6eleqr 2501 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  NN )
74 nnm1nn0 10878 . . . . . . . . . . . . 13  |-  ( j  e.  NN  ->  (
j  -  1 )  e.  NN0 )
7573, 74syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e. 
NN0 )
76 nn0uz 11161 . . . . . . . . . . . . 13  |-  NN0  =  ( ZZ>= `  0 )
7776a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  NN0  =  (
ZZ>= `  0 ) )
7875, 77eleqtrd 2492 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( ZZ>= `  0 )
)
7918nnzd 11007 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ZZ )
8079ad3antrrr 728 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  M  e.  ZZ )
81 peano2zm 10948 . . . . . . . . . . . . . . 15  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
8233, 81syl 17 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  ZZ )
8382zred 11008 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  RR )
8433zred 11008 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
85 elfzel2 11740 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
8685zred 11008 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  M  e.  RR )
8784ltm1d 10518 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  j )
88 elfzle2 11744 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
8983, 84, 86, 87, 88ltletrd 9776 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  M )
9089ad2antlr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  < 
M )
91 elfzo2 11862 . . . . . . . . . . 11  |-  ( ( j  -  1 )  e.  ( 0..^ M )  <->  ( ( j  -  1 )  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  ( j  -  1 )  <  M ) )
9278, 80, 90, 91syl3anbrc 1181 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0..^ M ) )
9325ad3antrrr 728 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  Q :
( 0 ... M
) --> RR )
9434, 81syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ZZ )
9565, 80, 943jca 1177 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  ( j  -  1 )  e.  ZZ ) )
9675nn0ge0d 10896 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  ( j  -  1 ) )
9783, 86, 89ltled 9765 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <_  M )
9897ad2antlr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  <_  M )
9995, 96, 98jca32 533 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
100 elfz2 11733 . . . . . . . . . . . . . . 15  |-  ( ( j  -  1 )  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
10199, 100sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0 ... M
) )
10293, 101ffvelrnd 6010 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR )
103102rexrd 9673 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR* )
10425ffvelrnda 6009 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR )
105104rexrd 9673 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
106105adantlr 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
107106adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  e.  RR* )
108 iocssre 11658 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
10952, 2, 108syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A (,] B
)  C_  RR )
110109sselda 3442 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  RR )
111110rexrd 9673 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  RR* )
112111ad2antrr 724 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  RR* )
113 simplll 760 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ph )
114 ovex 6306 . . . . . . . . . . . . . . . 16  |-  ( j  -  1 )  e. 
_V
115 eleq1 2474 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  - 
1 )  ->  (
i  e.  ( 0..^ M )  <->  ( j  -  1 )  e.  ( 0..^ M ) ) )
116115anbi2d 702 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  ( j  -  1 )  e.  ( 0..^ M ) ) ) )
117 fveq2 5849 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  i )  =  ( Q `  ( j  -  1 ) ) )
118 oveq1 6285 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  ( j  - 
1 )  ->  (
i  +  1 )  =  ( ( j  -  1 )  +  1 ) )
119118fveq2d 5853 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
120117, 119breq12d 4408 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
121116, 120imbi12d 318 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  ( j  - 
1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) ) )
12222simprrd 759 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
123122r19.21bi 2773 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
124114, 121, 123vtocl 3111 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
125113, 92, 124syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
12633zcnd 11009 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
127 1cnd 9642 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  1  e.  CC )
128126, 127npcand 9971 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
( j  -  1 )  +  1 )  =  j )
129128eqcomd 2410 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  j  =  ( ( j  -  1 )  +  1 ) )
130129fveq2d 5853 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  j )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
131130eqcomd 2410 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
132131ad2antlr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  =  ( Q `  j ) )
133125, 132breqtrd 4419 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  j )
)
134 simpr 459 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
135133, 134breqtrd 4419 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( E `  X )
)
136109, 15sseldd 3443 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E `  X
)  e.  RR )
137136leidd 10159 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E `  X
)  <_  ( E `  X ) )
138137ad2antrr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( E `  X
)  <_  ( E `  X ) )
13941adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( E `  X
)  =  ( Q `
 j ) )
140138, 139breqtrd 4419 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  ( Q `  j )  =  ( E `  X ) )  -> 
( E `  X
)  <_  ( Q `  j ) )
141140adantllr 717 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
142103, 107, 112, 135, 141eliocd 36911 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 j ) ) )
143130oveq2d 6294 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
( Q `  (
j  -  1 ) ) (,] ( Q `
 j ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
144143ad2antlr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( ( Q `  ( j  -  1 ) ) (,] ( Q `  j ) )  =  ( ( Q `  ( j  -  1 ) ) (,] ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
145142, 144eleqtrd 2492 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) )
146117, 119oveq12d 6296 . . . . . . . . . . . 12  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
147146eleq2d 2472 . . . . . . . . . . 11  |-  ( i  =  ( j  - 
1 )  ->  (
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  <->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) ) )
148147rspcev 3160 . . . . . . . . . 10  |-  ( ( ( j  -  1 )  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  ( j  -  1 ) ) (,] ( Q `  ( (
j  -  1 )  +  1 ) ) ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
14992, 145, 148syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  j  e.  ( 0 ... M ) )  /\  ( Q `  j )  =  ( E `  X ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
150149ex 432 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  j  e.  ( 0 ... M
) )  ->  (
( Q `  j
)  =  ( E `
 X )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) ) )
151150adantlr 713 . . . . . . 7  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  ( E `  X )  e.  ran  Q )  /\  j  e.  ( 0 ... M ) )  ->  ( ( Q `  j )  =  ( E `  X )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) ) )
152151rexlimdva 2896 . . . . . 6  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  ( E `  X )  e.  ran  Q )  -> 
( E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X )  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) ) )
15331, 152mpd 15 . . . . 5  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
15418ad2antrr 724 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  M  e.  NN )
15525ad2antrr 724 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  Q : ( 0 ... M ) --> RR )
156 iocssicc 11666 . . . . . . . . . 10  |-  ( A (,] B )  C_  ( A [,] B )
15746eqcomd 2410 . . . . . . . . . . 11  |-  ( ph  ->  A  =  ( Q `
 0 ) )
15845simprd 461 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  M
)  =  B )
159158eqcomd 2410 . . . . . . . . . . 11  |-  ( ph  ->  B  =  ( Q `
 M ) )
160157, 159oveq12d 6296 . . . . . . . . . 10  |-  ( ph  ->  ( A [,] B
)  =  ( ( Q `  0 ) [,] ( Q `  M ) ) )
161156, 160syl5sseq 3490 . . . . . . . . 9  |-  ( ph  ->  ( A (,] B
)  C_  ( ( Q `  0 ) [,] ( Q `  M
) ) )
162161sselda 3442 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  ( E `  X )  e.  ( ( Q `  0
) [,] ( Q `
 M ) ) )
163162adantr 463 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  ( E `  X )  e.  ( ( Q `  0
) [,] ( Q `
 M ) ) )
164 simpr 459 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  -.  ( E `  X )  e.  ran  Q )
165 fveq2 5849 . . . . . . . . . 10  |-  ( k  =  j  ->  ( Q `  k )  =  ( Q `  j ) )
166165breq1d 4405 . . . . . . . . 9  |-  ( k  =  j  ->  (
( Q `  k
)  <  ( E `  X )  <->  ( Q `  j )  <  ( E `  X )
) )
167166cbvrabv 3058 . . . . . . . 8  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
( E `  X
) }  =  {
j  e.  ( 0..^ M )  |  ( Q `  j )  <  ( E `  X ) }
168167supeq1i 7940 . . . . . . 7  |-  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  ( E `  X ) } ,  RR ,  <  )  =  sup ( { j  e.  ( 0..^ M )  |  ( Q `
 j )  < 
( E `  X
) } ,  RR ,  <  )
169154, 155, 163, 164, 168fourierdlem25 37282 . . . . . 6  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
170 ioossioc 36893 . . . . . . . . 9  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )
171170sseli 3438 . . . . . . . 8  |-  ( ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
172171a1i 11 . . . . . . 7  |-  ( ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B ) )  /\  -.  ( E `  X
)  e.  ran  Q
)  /\  i  e.  ( 0..^ M ) )  ->  ( ( E `
 X )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) ) )
173172reximdva 2879 . . . . . 6  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  ( E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) ) )
174169, 173mpd 15 . . . . 5  |-  ( ( ( ph  /\  ( E `  X )  e.  ( A (,] B
) )  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
175153, 174pm2.61dan 792 . . . 4  |-  ( (
ph  /\  ( E `  X )  e.  ( A (,] B ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
17615, 175mpdan 666 . . 3  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
177 fourierdlem49.f . . . . . . . . . . 11  |-  ( ph  ->  F : D --> RR )
178 frel 5717 . . . . . . . . . . 11  |-  ( F : D --> RR  ->  Rel 
F )
179177, 178syl 17 . . . . . . . . . 10  |-  ( ph  ->  Rel  F )
180 resindm 5138 . . . . . . . . . . 11  |-  ( Rel 
F  ->  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  dom  F
) )  =  ( F  |`  ( -oo (,) ( E `  X
) ) ) )
181180eqcomd 2410 . . . . . . . . . 10  |-  ( Rel 
F  ->  ( F  |`  ( -oo (,) ( E `  X )
) )  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i 
dom  F ) ) )
182179, 181syl 17 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( -oo (,) ( E `  X ) ) )  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  dom  F
) ) )
183 fdm 5718 . . . . . . . . . . . 12  |-  ( F : D --> RR  ->  dom 
F  =  D )
184177, 183syl 17 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  D )
185184ineq2d 3641 . . . . . . . . . 10  |-  ( ph  ->  ( ( -oo (,) ( E `  X ) )  i^i  dom  F
)  =  ( ( -oo (,) ( E `
 X ) )  i^i  D ) )
186185reseq2d 5094 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  (
( -oo (,) ( E `
 X ) )  i^i  dom  F )
)  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  D ) ) )
187182, 186eqtrd 2443 . . . . . . . 8  |-  ( ph  ->  ( F  |`  ( -oo (,) ( E `  X ) ) )  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  D ) ) )
1881873ad2ant1 1018 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( F  |`  ( -oo (,) ( E `  X ) ) )  =  ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  D ) ) )
189188oveq1d 6293 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F  |`  ( -oo (,) ( E `
 X ) ) ) lim CC  ( E `
 X ) )  =  ( ( F  |`  ( ( -oo (,) ( E `  X ) )  i^i  D ) ) lim CC  ( E `
 X ) ) )
190 ax-resscn 9579 . . . . . . . . . . 11  |-  RR  C_  CC
191190a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
192177, 191fssd 5723 . . . . . . . . 9  |-  ( ph  ->  F : D --> CC )
1931923ad2ant1 1018 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  F : D --> CC )
194 inss2 3660 . . . . . . . . 9  |-  ( ( -oo (,) ( E `
 X ) )  i^i  D )  C_  D
195194a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( -oo (,) ( E `  X ) )  i^i  D ) 
C_  D )
196193, 195fssresd 5735 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( F  |`  (
( -oo (,) ( E `
 X ) )  i^i  D ) ) : ( ( -oo (,) ( E `  X
) )  i^i  D
) --> CC )
197 mnfxr 11376 . . . . . . . . . 10  |- -oo  e.  RR*
198197a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  e.  RR* )
19925adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
200 elfzofz 11874 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
201200adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
202199, 201ffvelrnd 6010 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
203202rexrd 9673 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
204202mnfltd 36861 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <  ( Q `
 i ) )
205198, 203, 204xrltled 36830 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <_  ( Q `
 i ) )
206 iooss1 11617 . . . . . . . . . 10  |-  ( ( -oo  e.  RR*  /\ -oo  <_  ( Q `  i
) )  ->  (
( Q `  i
) (,) ( E `
 X ) ) 
C_  ( -oo (,) ( E `  X ) ) )
207197, 205, 206sylancr 661 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( E `  X
) )  C_  ( -oo (,) ( E `  X ) ) )
2082073adant3 1017 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( E `  X )
)  C_  ( -oo (,) ( E `  X
) ) )
209 fzofzp1 11946 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
210209adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
211199, 210ffvelrnd 6010 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2122113adant3 1017 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
213212rexrd 9673 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
2142023adant3 1017 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
215214rexrd 9673 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR* )
216 simp3 999 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
217 iocleub 36905 . . . . . . . . . . 11  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  ->  ( E `  X )  <_  ( Q `  (
i  +  1 ) ) )
218215, 213, 216, 217syl3anc 1230 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( Q `  ( i  +  1 ) ) )
219 iooss2 11618 . . . . . . . . . 10  |-  ( ( ( Q `  (
i  +  1 ) )  e.  RR*  /\  ( E `  X )  <_  ( Q `  (
i  +  1 ) ) )  ->  (
( Q `  i
) (,) ( E `
 X ) ) 
C_  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
220213, 218, 219syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( E `  X )
)  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
221 fourierdlem49.cn . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
222 cncff 21689 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
223 fdm 5718 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
224221, 222, 2233syl 18 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
225 ssdmres 5115 . . . . . . . . . . . 12  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  F  <->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
226224, 225sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
227184adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  F  =  D )
228226, 227sseqtrd 3478 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
2292283adant3 1017 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
230220, 229sstrd 3452 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( E `  X )
)  C_  D )
231208, 230ssind 3663 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( E `  X )
)  C_  ( ( -oo (,) ( E `  X ) )  i^i 
D ) )
232 fourierdlem49.d . . . . . . . . . 10  |-  ( ph  ->  D  C_  RR )
233232, 191sstrd 3452 . . . . . . . . 9  |-  ( ph  ->  D  C_  CC )
2342333ad2ant1 1018 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  D  C_  CC )
235194, 234syl5ss 3453 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( -oo (,) ( E `  X ) )  i^i  D ) 
C_  CC )
236 eqid 2402 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
237 eqid 2402 . . . . . . 7  |-  ( (
TopOpen ` fld )t  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  =  ( ( TopOpen ` fld )t  ( ( ( -oo (,) ( E `
 X ) )  i^i  D )  u. 
{ ( E `  X ) } ) )
2381363ad2ant1 1018 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR )
239238rexrd 9673 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR* )
240 iocgtlb 36904 . . . . . . . . . 10  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( E `  X
) )
241215, 213, 216, 240syl3anc 1230 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( E `  X ) )
242238leidd 10159 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( E `  X ) )
243215, 239, 239, 241, 242eliocd 36911 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,] ( E `  X ) ) )
244 snunioo2 36912 . . . . . . . . . . 11  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( E `  X )  e.  RR*  /\  ( Q `
 i )  < 
( E `  X
) )  ->  (
( ( Q `  i ) (,) ( E `  X )
)  u.  { ( E `  X ) } )  =  ( ( Q `  i
) (,] ( E `
 X ) ) )
245215, 239, 241, 244syl3anc 1230 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i ) (,) ( E `  X
) )  u.  {
( E `  X
) } )  =  ( ( Q `  i ) (,] ( E `  X )
) )
246245fveq2d 5853 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( int `  (
( TopOpen ` fld )t  ( ( ( -oo (,) ( E `
 X ) )  i^i  D )  u. 
{ ( E `  X ) } ) ) ) `  (
( ( Q `  i ) (,) ( E `  X )
)  u.  { ( E `  X ) } ) )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( ( -oo (,) ( E `
 X ) )  i^i  D )  u. 
{ ( E `  X ) } ) ) ) `  (
( Q `  i
) (,] ( E `
 X ) ) ) )
247236cnfldtop 21583 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  e.  Top
248 ovex 6306 . . . . . . . . . . . . 13  |-  ( -oo (,) ( E `  X
) )  e.  _V
249248inex1 4535 . . . . . . . . . . . 12  |-  ( ( -oo (,) ( E `
 X ) )  i^i  D )  e. 
_V
250 snex 4632 . . . . . . . . . . . 12  |-  { ( E `  X ) }  e.  _V
251249, 250unex 6580 . . . . . . . . . . 11  |-  ( ( ( -oo (,) ( E `  X )
)  i^i  D )  u.  { ( E `  X ) } )  e.  _V
252 resttop 19954 . . . . . . . . . . 11  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } )  e.  _V )  ->  ( ( TopOpen ` fld )t  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) )  e.  Top )
253247, 251, 252mp2an 670 . . . . . . . . . 10  |-  ( (
TopOpen ` fld )t  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  e. 
Top
254 retop 21560 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Top
255254a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( topGen `  ran  (,) )  e.  Top )
256251a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } )  e.  _V )
257 iooretop 21565 . . . . . . . . . . . . 13  |-  ( ( Q `  i ) (,) +oo )  e.  ( topGen `  ran  (,) )
258257a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) +oo )  e.  ( topGen ` 
ran  (,) ) )
259 elrestr 15043 . . . . . . . . . . . 12  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( ( -oo (,) ( E `  X )
)  i^i  D )  u.  { ( E `  X ) } )  e.  _V  /\  (
( Q `  i
) (,) +oo )  e.  ( topGen `  ran  (,) )
)  ->  ( (
( Q `  i
) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  e.  ( ( topGen `  ran  (,) )t  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) ) )
260255, 256, 258, 259syl3anc 1230 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) )  e.  ( ( topGen `  ran  (,) )t  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )
261 simpr 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  =  ( E `  X
) )  ->  x  =  ( E `  X ) )
262 pnfxr 11374 . . . . . . . . . . . . . . . . . . . 20  |- +oo  e.  RR*
263262a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> +oo  e.  RR* )
264238ltpnfd 36852 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  < +oo )
265215, 263, 238, 241, 264eliood 36900 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,) +oo ) )
266 snidg 3998 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E `  X )  e.  RR  ->  ( E `  X )  e.  { ( E `  X ) } )
267 elun2 3611 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E `  X )  e.  { ( E `
 X ) }  ->  ( E `  X )  e.  ( ( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) )
268266, 267syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E `  X )  e.  RR  ->  ( E `  X )  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )
269136, 268syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( E `  X
)  e.  ( ( ( -oo (,) ( E `  X )
)  i^i  D )  u.  { ( E `  X ) } ) )
2702693ad2ant1 1018 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( ( -oo (,) ( E `  X )
)  i^i  D )  u.  { ( E `  X ) } ) )
271265, 270elind 3627 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( ( Q `  i
) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) ) )
272271adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  =  ( E `  X
) )  ->  ( E `  X )  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )
273261, 272eqeltrd 2490 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  =  ( E `  X
) )  ->  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )
274273adantlr 713 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  x  =  ( E `  X ) )  ->  x  e.  ( (
( Q `  i
) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) ) )
275215adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  e.  RR* )
276262a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  -> +oo  e.  RR* )
277203adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  e.  RR* )
278136adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( E `  X )  e.  RR )
279278adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( E `  X )  e.  RR )
280 iocssre 11658 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( E `  X )  e.  RR )  ->  (
( Q `  i
) (,] ( E `
 X ) ) 
C_  RR )
281277, 279, 280syl2anc 659 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  (
( Q `  i
) (,] ( E `
 X ) ) 
C_  RR )
282 simpr 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )
283281, 282sseldd 3443 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  RR )
2842833adantl3 1155 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  RR )
285279rexrd 9673 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( E `  X )  e.  RR* )
286 iocgtlb 36904 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( E `  X )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  <  x )
287277, 285, 282, 286syl3anc 1230 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  <  x )
2882873adantl3 1155 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  ( Q `  i )  <  x )
289284ltpnfd 36852 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  < +oo )
290275, 276, 284, 288, 289eliood 36900 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  ( ( Q `  i ) (,) +oo ) )
291290adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  ( ( Q `  i ) (,) +oo ) )
292197a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  -> -oo  e.  RR* )
293285adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  ( E `  X )  e.  RR* )
294283adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  e.  RR )
295294mnfltd 36861 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  -> -oo  <  x
)
296136ad3antrrr 728 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  ( E `  X )  e.  RR )
297 iocleub 36905 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( E `  X )  e.  RR*  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  <_  ( E `  X
) )
298277, 285, 282, 297syl3anc 1230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  <_  ( E `  X
) )
299298adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  <_  ( E `  X ) )
300 neqne 36810 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  x  =  ( E `
 X )  ->  x  =/=  ( E `  X ) )
301300necomd 2674 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  x  =  ( E `
 X )  -> 
( E `  X
)  =/=  x )
302301adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  ( E `  X )  =/=  x
)
303294, 296, 299, 302leneltd 36864 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  <  ( E `  X ) )
304292, 293, 294, 295, 303eliood 36900 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )  /\  -.  x  =  ( E `  X )
)  ->  x  e.  ( -oo (,) ( E `
 X ) ) )
3053043adantll3 36800 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  ( -oo (,) ( E `  X
) ) )
306229ad2antrr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
307275adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( Q `  i
)  e.  RR* )
308213ad2antrr 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
309284adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  RR )
310288adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( Q `  i
)  <  x )
311238ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( E `  X
)  e.  RR )
312212ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
3133033adantll3 36800 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  <  ( E `  X ) )
314218ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  -> 
( E `  X
)  <_  ( Q `  ( i  +  1 ) ) )
315309, 311, 312, 313, 314ltletrd 9776 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  <  ( Q `  ( i  +  1 ) ) )
316307, 308, 309, 310, 315eliood 36900 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
317306, 316sseldd 3443 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  D )
318305, 317elind 3627 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  ( ( -oo (,) ( E `  X ) )  i^i 
D ) )
319 elun1 3610 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( -oo (,) ( E `  X
) )  i^i  D
)  ->  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )
320318, 319syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  ( (
( -oo (,) ( E `
 X ) )  i^i  D )  u. 
{ ( E `  X ) } ) )
321291, 320elind 3627 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  /\  -.  x  =  ( E `  X ) )  ->  x  e.  ( (
( Q `  i
) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) ) )
322274, 321pm2.61dan 792 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( Q `  i ) (,] ( E `  X )
) )  ->  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )
323215adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  -> 
( Q `  i
)  e.  RR* )
324239adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  -> 
( E `  X
)  e.  RR* )
325 elinel1 3628 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( ( Q `  i ) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  ->  x  e.  ( ( Q `  i ) (,) +oo ) )
326 elioore 11612 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( Q `
 i ) (,) +oo )  ->  x  e.  RR )
327326rexrd 9673 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( Q `
 i ) (,) +oo )  ->  x  e. 
RR* )
328325, 327syl 17 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( ( ( Q `  i ) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  ->  x  e.  RR* )
329328adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  ->  x  e.  RR* )
330203adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  -> 
( Q `  i
)  e.  RR* )
331262a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  -> +oo  e.  RR* )
332325adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  ->  x  e.  ( ( Q `  i ) (,) +oo ) )
333 ioogtlb 36897 . . . . . . . . . . . . . . . 16  |-  ( ( ( Q `  i
)  e.  RR*  /\ +oo  e.  RR*  /\  x  e.  ( ( Q `  i ) (,) +oo ) )  ->  ( Q `  i )  <  x )
334330, 331, 332, 333syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  -> 
( Q `  i
)  <  x )
3353343adantl3 1155 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  -> 
( Q `  i
)  <  x )
336 elinel2 3629 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( ( Q `  i ) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  ->  x  e.  ( (
( -oo (,) ( E `
 X ) )  i^i  D )  u. 
{ ( E `  X ) } ) )
337 elsni 3997 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  { ( E `
 X ) }  ->  x  =  ( E `  X ) )
338337adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  { ( E `  X
) } )  ->  x  =  ( E `  X ) )
339137adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  { ( E `  X
) } )  -> 
( E `  X
)  <_  ( E `  X ) )
340338, 339eqbrtrd 4415 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  { ( E `  X
) } )  ->  x  <_  ( E `  X ) )
341340adantlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  /\  x  e.  { ( E `  X ) } )  ->  x  <_  ( E `  X
) )
342 simpll 752 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  /\  -.  x  e.  { ( E `  X ) } )  ->  ph )
343 elunnel2 36795 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( ( ( -oo (,) ( E `  X )
)  i^i  D )  u.  { ( E `  X ) } )  /\  -.  x  e. 
{ ( E `  X ) } )  ->  x  e.  ( ( -oo (,) ( E `  X )
)  i^i  D )
)
344343adantll 712 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  /\  -.  x  e.  { ( E `  X ) } )  ->  x  e.  ( ( -oo (,) ( E `  X ) )  i^i  D ) )
345 elinel1 3628 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( -oo (,) ( E `  X
) )  i^i  D
)  ->  x  e.  ( -oo (,) ( E `
 X ) ) )
346 elioore 11612 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( -oo (,) ( E `  X ) )  ->  x  e.  RR )
347346adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  ->  x  e.  RR )
348136adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  ->  ( E `  X )  e.  RR )
349197a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  -> -oo  e.  RR* )
350348rexrd 9673 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  ->  ( E `  X )  e.  RR* )
351 simpr 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  ->  x  e.  ( -oo (,) ( E `
 X ) ) )
352 iooltub 36916 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( -oo  e.  RR*  /\  ( E `  X )  e.  RR*  /\  x  e.  ( -oo (,) ( E `  X )
) )  ->  x  <  ( E `  X
) )
353349, 350, 351, 352syl3anc 1230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  ->  x  <  ( E `  X ) )
354347, 348, 353ltled 9765 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( -oo (,) ( E `
 X ) ) )  ->  x  <_  ( E `  X ) )
355345, 354sylan2 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( -oo (,) ( E `  X ) )  i^i  D ) )  ->  x  <_  ( E `  X ) )
356342, 344, 355syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  /\  -.  x  e.  { ( E `  X ) } )  ->  x  <_  ( E `  X
) )
357341, 356pm2.61dan 792 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  ->  x  <_  ( E `  X ) )
358357adantlr 713 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) )  ->  x  <_  ( E `  X ) )
359336, 358sylan2 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  ->  x  <_  ( E `  X ) )
3603593adantl3 1155 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  ->  x  <_  ( E `  X ) )
361323, 324, 329, 335, 360eliocd 36911 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  x  e.  ( ( ( Q `
 i ) (,) +oo )  i^i  (
( ( -oo (,) ( E `  X ) )  i^i  D )  u.  { ( E `
 X ) } ) ) )  ->  x  e.  ( ( Q `  i ) (,] ( E `  X
) ) )
362322, 361impbida 833 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( x  e.  ( ( Q `  i
) (,] ( E `
 X ) )  <-> 
x  e.  ( ( ( Q `  i
) (,) +oo )  i^i  ( ( ( -oo (,) ( E `  X
) )  i^i  D
)  u.  { ( E `  X ) } ) ) ) )
363362eqrdv 2399 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,] ( E `  X )