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

Theorem fourierdlem41 38123
Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem41.a  |-  ( ph  ->  A  e.  RR )
fourierdlem41.b  |-  ( ph  ->  B  e.  RR )
fourierdlem41.altb  |-  ( ph  ->  A  <  B )
fourierdlem41.t  |-  T  =  ( B  -  A
)
fourierdlem41.dper  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T
) )  e.  D
)
fourierdlem41.x  |-  ( ph  ->  X  e.  RR )
fourierdlem41.z  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
fourierdlem41.e  |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )
fourierdlem41.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 ) ) ) } )
fourierdlem41.m  |-  ( ph  ->  M  e.  NN )
fourierdlem41.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem41.qssd  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
Assertion
Ref Expression
fourierdlem41  |-  ( ph  ->  ( E. y  e.  RR  ( y  < 
X  /\  ( y (,) X )  C_  D
)  /\  E. y  e.  RR  ( X  < 
y  /\  ( X (,) y )  C_  D
) ) )
Distinct variable groups:    A, m, p    x, A    B, i,
k    B, m, p, i   
x, B, y, k    D, i, k, y    x, D    i, E, k, y   
i, M, k    m, M, p    y, M    Q, i, k    Q, p    y, Q    T, k, x, y   
i, X, k    x, X, y    k, Z, x, y    ph, i, k    ph, x, y
Allowed substitution hints:    ph( m, p)    A( y, i, k)    D( m, p)    P( x, y, i, k, m, p)    Q( x, m)    T( i, m, p)    E( x, m, p)    M( x)    X( m, p)    Z( i, m, p)

Proof of Theorem fourierdlem41
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 simpr 468 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  ( E `  X )  e.  ran  Q )
2 fourierdlem41.q . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
3 fourierdlem41.m . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
4 fourierdlem41.p . . . . . . . . . . . . 13  |-  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 ) ) ) } )
54fourierdlem2 38083 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) )
63, 5syl 17 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
72, 6mpbid 215 . . . . . . . . . 10  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
87simpld 466 . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
9 elmapi 7511 . . . . . . . . 9  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
10 ffn 5739 . . . . . . . . 9  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
118, 9, 103syl 18 . . . . . . . 8  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
1211adantr 472 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  Q  Fn  ( 0 ... M
) )
13 fvelrnb 5926 . . . . . . 7  |-  ( Q  Fn  ( 0 ... M )  ->  (
( E `  X
)  e.  ran  Q  <->  E. j  e.  ( 0 ... M ) ( Q `  j )  =  ( E `  X ) ) )
1412, 13syl 17 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  ( ( E `  X )  e.  ran  Q  <->  E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X ) ) )
151, 14mpbid 215 . . . . 5  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X ) )
16 0zd 10973 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  e.  ZZ )
17 elfzelz 11826 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
18173ad2ant2 1052 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  ZZ )
19 1zzd 10992 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  e.  ZZ )
2018, 19zsubcld 11068 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ZZ )
21 simpll 768 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  ->  ph )
22 elfzle1 11828 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
2322anim1i 578 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  <_ 
j  /\  -.  0  <  j ) )
24 0red 9662 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  e.  RR )
2517zred 11063 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
2625adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  e.  RR )
2724, 26eqleltd 9796 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  =  j  <->  ( 0  <_ 
j  /\  -.  0  <  j ) ) )
2823, 27mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  =  j )
2928eqcomd 2477 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  =  0 )
3029adantll 728 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
j  =  0 )
31 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
327simprld 773 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
3332simpld 466 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  =  A )
3431, 33sylan9eqr 2527 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  = 
0 )  ->  ( Q `  j )  =  A )
3521, 30, 34syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
( Q `  j
)  =  A )
36353adantl3 1188 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =  A )
37 simpr 468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR )
3938rexrd 9708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  RR* )
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
4140rexrd 9708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  RR* )
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  <  B )
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  =  ( B  -  A
)
44 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
4538, 40, 42, 43, 44fourierdlem4 38085 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) : RR --> ( A (,] B ) )
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) ) )
48 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
4940adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
5049, 48resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
5140, 38resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( B  -  A
)  e.  RR )
5243, 51syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  T  e.  RR )
5352adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
54 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  0  e.  RR )
5538, 40posdifd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
5642, 55mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  0  <  ( B  -  A ) )
5743eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( B  -  A )  =  T
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( B  -  A
)  =  T )
5956, 58breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  0  <  T )
6054, 59gtned 9787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  T  =/=  0 )
6160adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
6250, 53, 61redivcld 10457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
6362flcld 12067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
6463zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
6564, 53remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
6766fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  RR  /\  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
)  e.  RR )  ->  ( Z `  x )  =  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
6848, 65, 67syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( Z `
 x )  =  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
6968oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( Z `  x ) )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
7069mpteq2dva 4482 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7147, 70eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7271feq1d 5724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( E : RR --> ( A (,] B )  <-> 
( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) : RR --> ( A (,] B ) ) )
7345, 72mpbird 240 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  E : RR --> ( A (,] B ) )
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  RR )
7573, 74ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( E `  X
)  e.  ( A (,] B ) )
76 iocgtlb 37695 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 X )  e.  ( A (,] B
) )  ->  A  <  ( E `  X
) )
7739, 41, 75, 76syl3anc 1292 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  <  ( E `
 X ) )
7838, 77gtned 9787 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E `  X
)  =/=  A )
7978adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =/=  A
)
8037, 79eqnetrd 2710 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =/=  A
)
8180adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A
)
82813adantl2 1187 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A )
8382neneqd 2648 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  -.  ( Q `  j )  =  A )
8436, 83condan 811 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <  j )
85 zltlem1 11013 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  j  e.  ZZ )  ->  ( 0  <  j  <->  0  <_  ( j  - 
1 ) ) )
8616, 18, 85syl2anc 673 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  <  j  <->  0  <_  ( j  -  1 ) ) )
8784, 86mpbid 215 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  ( j  -  1 ) )
88 eluz2 11188 . . . . . . . . . . 11  |-  ( ( j  -  1 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( j  -  1 )  e.  ZZ  /\  0  <_ 
( j  -  1 ) ) )
8916, 20, 87, 88syl3anbrc 1214 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( ZZ>= `  0 )
)
90 elfzel2 11824 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
91903ad2ant2 1052 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  M  e.  ZZ )
92 1red 9676 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  1  e.  RR )
9325, 92resubcld 10068 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  RR )
9490zred 11063 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  M  e.  RR )
9525ltm1d 10561 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  j )
96 elfzle2 11829 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
9793, 25, 94, 95, 96ltletrd 9812 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  M )
98973ad2ant2 1052 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  < 
M )
99 elfzo2 11950 . . . . . . . . . 10  |-  ( ( j  -  1 )  e.  ( 0..^ M )  <->  ( ( j  -  1 )  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  ( j  -  1 )  <  M ) )
10089, 91, 98, 99syl3anbrc 1214 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0..^ M ) )
1018, 9syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
1021013ad2ant1 1051 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  Q :
( 0 ... M
) --> RR )
10316, 91, 203jca 1210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  ( j  -  1 )  e.  ZZ ) )
10493, 94, 97ltled 9800 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <_  M )
1051043ad2ant2 1052 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  <_  M )
106103, 87, 105jca32 544 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
107 elfz2 11817 . . . . . . . . . . . . 13  |-  ( ( j  -  1 )  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
108106, 107sylibr 217 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0 ... M
) )
109102, 108ffvelrnd 6038 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR )
110109rexrd 9708 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR* )
11125recnd 9687 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
112 1cnd 9677 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  1  e.  CC )
113111, 112npcand 10009 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( j  -  1 )  +  1 )  =  j )
114113fveq2d 5883 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
115114adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
116101ffvelrnda 6037 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR )
117116rexrd 9708 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
118115, 117eqeltrd 2549 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  e.  RR* )
1191183adant3 1050 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  e.  RR* )
120 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  x  =  X )
121 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  ( Z `  x )  =  ( Z `  X ) )
122120, 121oveq12d 6326 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
123122adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  X )  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
12466a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
125 oveq2 6316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
126125oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
127126fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
128127oveq1d 6323 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
129128adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  =  X )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
13040, 74resubcld 10068 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  -  X
)  e.  RR )
131130, 52, 60redivcld 10457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
132131flcld 12067 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
133132zred 11063 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
134133, 52remulcld 9689 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
135124, 129, 74, 134fvmptd 5969 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Z `  X
)  =  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
136135, 134eqeltrd 2549 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z `  X
)  e.  RR )
13774, 136readdcld 9688 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( Z `  X ) )  e.  RR )
13847, 123, 74, 137fvmptd 5969 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( Z `  X ) ) )
139138, 137eqeltrd 2549 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  X
)  e.  RR )
140139rexrd 9708 . . . . . . . . . . 11  |-  ( ph  ->  ( E `  X
)  e.  RR* )
1411403ad2ant1 1051 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  RR* )
142 simp1 1030 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ph )
143 ovex 6336 . . . . . . . . . . . . . 14  |-  ( j  -  1 )  e. 
_V
144 eleq1 2537 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  (
i  e.  ( 0..^ M )  <->  ( j  -  1 )  e.  ( 0..^ M ) ) )
145144anbi2d 718 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  - 
1 )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  ( j  -  1 )  e.  ( 0..^ M ) ) ) )
146 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  i )  =  ( Q `  ( j  -  1 ) ) )
147 oveq1 6315 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  (
i  +  1 )  =  ( ( j  -  1 )  +  1 ) )
148147fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
149146, 148breq12d 4408 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
150145, 149imbi12d 327 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) )
1517simprrd 775 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
152151r19.21bi 2776 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
153143, 150, 152vtocl 3086 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
154142, 100, 153syl2anc 673 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
1551143ad2ant2 1052 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  =  ( Q `  j ) )
156154, 155breqtrd 4420 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  j )
)
157 simp3 1032 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
158156, 157breqtrd 4420 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( E `  X )
)
159139leidd 10201 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  X
)  <_  ( E `  X ) )
160159adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( E `  X )
)
16137eqcomd 2477 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =  ( Q `  j ) )
162160, 161breqtrd 4420 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
1631623adant2 1049 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
164113eqcomd 2477 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  =  ( ( j  -  1 )  +  1 ) )
165164fveq2d 5883 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  j )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
1661653ad2ant2 1052 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( Q `  ( ( j  -  1 )  +  1 ) ) )
167163, 166breqtrd 4420 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  ( (
j  -  1 )  +  1 ) ) )
168110, 119, 141, 158, 167eliocd 37701 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) )
169146, 148oveq12d 6326 . . . . . . . . . . 11  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
170169eleq2d 2534 . . . . . . . . . 10  |-  ( i  =  ( j  - 
1 )  ->  (
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  <->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) ) )
171170rspcev 3136 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) )
172100, 168, 171syl2anc 673 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
1731723exp 1230 . . . . . . 7  |-  ( ph  ->  ( j  e.  ( 0 ... M )  ->  ( ( Q `
 j )  =  ( E `  X
)  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) ) ) )
174173adantr 472 . . . . . 6  |-  ( (
ph  /\  ( 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 ) ) ) ) ) )
175174rexlimdv 2870 . . . . 5  |-  ( (
ph  /\  ( 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 ) ) ) ) )
17615, 175mpd 15 . . . 4  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
1773adantr 472 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  M  e.  NN )
178101adantr 472 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  Q : ( 0 ... M ) --> RR )
179 iocssicc 11747 . . . . . . . 8  |-  ( ( Q `  0 ) (,] ( Q `  M ) )  C_  ( ( Q ` 
0 ) [,] ( Q `  M )
)
18032simprd 470 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  =  B )
18133, 180oveq12d 6326 . . . . . . . . 9  |-  ( ph  ->  ( ( Q ` 
0 ) (,] ( Q `  M )
)  =  ( A (,] B ) )
18275, 181eleqtrrd 2552 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) (,] ( Q `  M ) ) )
183179, 182sseldi 3416 . . . . . . 7  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
184183adantr 472 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  -> 
( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
185 simpr 468 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  -.  ( E `  X
)  e.  ran  Q
)
186 fveq2 5879 . . . . . . . . 9  |-  ( k  =  j  ->  ( Q `  k )  =  ( Q `  j ) )
187186breq1d 4405 . . . . . . . 8  |-  ( k  =  j  ->  (
( Q `  k
)  <  ( E `  X )  <->  ( Q `  j )  <  ( E `  X )
) )
188187cbvrabv 3030 . . . . . . 7  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
( E `  X
) }  =  {
j  e.  ( 0..^ M )  |  ( Q `  j )  <  ( E `  X ) }
189188supeq1i 7979 . . . . . 6  |-  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  ( E `  X ) } ,  RR ,  <  )  =  sup ( { j  e.  ( 0..^ M )  |  ( Q `
 j )  < 
( E `  X
) } ,  RR ,  <  )
190177, 178, 184, 185, 189fourierdlem25 38106 . . . . 5  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
191 ioossioc 37684 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )
192191a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  -.  ( E `  X )  e.  ran  Q )  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )
193192sseld 3417 . . . . . 6  |-  ( ( ( ph  /\  -.  ( 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 2858 . . . . 5  |-  ( (
ph  /\  -.  ( 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 ) ) ) ) )
195190, 194mpd 15 . . . 4  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
196176, 195pm2.61dan 808 . . 3  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
197101adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
198 elfzofz 11962 . . . . . . . . . 10  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
199198adantl 473 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
200197, 199ffvelrnd 6038 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
2012003adant3 1050 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
2021363ad2ant1 1051 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Z `  X
)  e.  RR )
203201, 202resubcld 10068 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  e.  RR )
2041393ad2ant1 1051 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR )
205201rexrd 9708 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR* )
206 fzofzp1 12037 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
207206adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
208197, 207ffvelrnd 6038 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
209208rexrd 9708 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
2102093adant3 1050 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
211 simp3 1032 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
212 iocgtlb 37695 . . . . . . . . 9  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( E `  X
) )
213205, 210, 211, 212syl3anc 1292 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( E `  X ) )
214201, 204, 202, 213ltsub1dd 10246 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  ( ( E `  X )  -  ( Z `  X ) ) )
215138oveq1d 6323 . . . . . . . . 9  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  ( ( X  +  ( Z `
 X ) )  -  ( Z `  X ) ) )
21674recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  X  e.  CC )
217136recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  ( Z `  X
)  e.  CC )
218216, 217pncand 10006 . . . . . . . . 9  |-  ( ph  ->  ( ( X  +  ( Z `  X ) )  -  ( Z `
 X ) )  =  X )
219215, 218eqtrd 2505 . . . . . . . 8  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  X )
2202193ad2ant1 1051 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( E `  X )  -  ( Z `  X )
)  =  X )
221214, 220breqtrd 4420 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  X )
222 elioore 11691 . . . . . . . . . . 11  |-  ( y  e.  ( ( ( Q `  i )  -  ( Z `  X ) ) (,) X )  ->  y  e.  RR )
223135oveq2d 6324 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  +  ( Z `  X ) )  =  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
224133recnd 9687 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  CC )
22552recnd 9687 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  CC )
226224, 225mulneg1d 10092 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )
227223, 226oveq12d 6326 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  =  ( ( y  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  +  -u (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
228227adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( Z `
 X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  =  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  +  -u ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
229 simpr 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
230134adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  RR )
231229, 230readdcld 9688 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  RR )
232231recnd 9687 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  CC )
233230recnd 9687 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  CC )
234232, 233negsubd 10011 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  +  -u ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  =  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  -  (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
235229recnd 9687 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
236235, 233pncand 10006 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  -  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  =  y )
237228, 234, 2363eqtrrd 2510 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
238222, 237sylan2 482 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
2392383ad2antl1 1192 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
240 simpl1 1033 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ph )
241 fourierdlem41.qssd . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
2422413adant3 1050 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
243242adantr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
244205adantr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  e.  RR* )
245210adantr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
246222adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
247136adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
248246, 247readdcld 9688 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  RR )
2492483ad2antl1 1192 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  RR )
250136adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Z `  X )  e.  RR )
251200, 250resubcld 10068 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR )
252251rexrd 9708 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR* )
253252adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  e. 
RR* )
25474rexrd 9708 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  RR* )
255254ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR* )
256 simpr 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )
257 ioogtlb 37688 . . . . . . . . . . . . . . 15  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR*  /\  X  e.  RR*  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  < 
y )
258253, 255, 256, 257syl3anc 1292 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  < 
y )
259200adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  e.  RR )
260136ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
261222adantl 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
262259, 260, 261ltsubaddd 10230 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( (
( Q `  i
)  -  ( Z `
 X ) )  <  y  <->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) ) )
263258, 262mpbid 215 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) )
2642633adantl3 1188 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) )
265240, 139syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( E `  X )  e.  RR )
266208adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2672663adantl3 1188 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
26874ad2antrr 740 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR )
269 iooltub 37706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR*  /\  X  e.  RR*  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
270253, 255, 256, 269syl3anc 1292 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
271261, 268, 260, 270ltadd1dd 10245 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( X  +  ( Z `  X ) ) )
272138eqcomd 2477 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  +  ( Z `  X ) )  =  ( E `
 X ) )
273272ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( X  +  ( Z `  X ) )  =  ( E `  X
) )
274271, 273breqtrd 4420 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( E `  X
) )
2752743adantl3 1188 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( E `  X
) )
276 iocleub 37696 . . . . . . . . . . . . . . 15  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  ->  ( E `  X )  <_  ( Q `  (
i  +  1 ) ) )
277205, 210, 211, 276syl3anc 1292 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( Q `  ( i  +  1 ) ) )
278277adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( E `  X )  <_  ( Q `  ( i  +  1 ) ) )
279249, 265, 267, 275, 278ltletrd 9812 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( Q `  (
i  +  1 ) ) )
280244, 245, 249, 264, 279eliood 37691 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
281243, 280sseldd 3419 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  D )
282240, 131syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( B  -  X )  /  T )  e.  RR )
283282flcld 12067 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( |_ `  ( ( B  -  X )  /  T
) )  e.  ZZ )
284283znegcld 11065 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  -u ( |_
`  ( ( B  -  X )  /  T ) )  e.  ZZ )
285 negex 9893 . . . . . . . . . . 11  |-  -u ( |_ `  ( ( B  -  X )  /  T ) )  e. 
_V
286 eleq1 2537 . . . . . . . . . . . . 13  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  e.  ZZ  <->  -u ( |_
`  ( ( B  -  X )  /  T ) )  e.  ZZ ) )
2872863anbi3d 1371 . . . . . . . . . . . 12  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( ph  /\  (
y  +  ( Z `
 X ) )  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  -u ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ ) ) )
288 oveq1 6315 . . . . . . . . . . . . . 14  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
289288oveq2d 6324 . . . . . . . . . . . . 13  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
290289eleq1d 2533 . . . . . . . . . . . 12  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( ( y  +  ( Z `  X
) )  +  ( k  x.  T ) )  e.  D  <->  ( (
y  +  ( Z `
 X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D ) )
291287, 290imbi12d 327 . . . . . . . . . . 11  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )  ->  ( ( y  +  ( Z `  X
) )  +  ( k  x.  T ) )  e.  D )  <-> 
( ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  -u ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )  ->  ( ( y  +  ( Z `  X ) )  +  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D ) ) )
292 ovex 6336 . . . . . . . . . . . 12  |-  ( y  +  ( Z `  X ) )  e. 
_V
293 eleq1 2537 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  e.  D  <->  ( y  +  ( Z `  X ) )  e.  D ) )
2942933anbi2d 1370 . . . . . . . . . . . . 13  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( ph  /\  x  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )
) )
295 oveq1 6315 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( k  x.  T
) ) )
296295eleq1d 2533 . . . . . . . . . . . . 13  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( x  +  ( k  x.  T ) )  e.  D  <->  ( (
y  +  ( Z `
 X ) )  +  ( k  x.  T ) )  e.  D ) )
297294, 296imbi12d 327 . . . . . . . . . . . 12  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( ( ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T ) )  e.  D )  <-> 
( ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )  ->  ( ( y  +  ( Z `  X
) )  +  ( k  x.  T ) )  e.  D ) ) )
298 fourierdlem41.dper . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T
) )  e.  D
)
299292, 297, 298vtocl 3086 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  e.  D )
300285, 291, 299vtocl 3086 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  -u ( |_ `  ( ( B  -  X )  /  T ) )  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D )
301240, 281, 284, 300syl3anc 1292 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( (
y  +  ( Z `
 X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D )
302239, 301eqeltrd 2549 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  D )
303302ralrimiva 2809 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  A. y  e.  (
( ( Q `  i )  -  ( Z `  X )
) (,) X ) y  e.  D )
304 dfss3 3408 . . . . . . 7  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) 
C_  D  <->  A. y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) y  e.  D )
305303, 304sylibr 217 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D )
306 breq1 4398 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y  <  X  <->  ( ( Q `
 i )  -  ( Z `  X ) )  <  X ) )
307 oveq1 6315 . . . . . . . . 9  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y (,) X )  =  ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) )
308307sseq1d 3445 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( (
y (,) X ) 
C_  D  <->  ( (
( Q `  i
)  -  ( Z `
 X ) ) (,) X )  C_  D ) )
309306, 308anbi12d 725 . . . . . . 7  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( (
y  <  X  /\  ( y (,) X
)  C_  D )  <->  ( ( ( Q `  i )  -  ( Z `  X )
)  <  X  /\  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D ) ) )
310309rspcev 3136 . . . . . 6  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR  /\  ( ( ( Q `
 i )  -  ( Z `  X ) )  <  X  /\  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D ) )  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
)
311203, 221, 305, 310syl12anc 1290 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
)
3123113exp 1230 . . . 4  |-  ( ph  ->  ( i  e.  ( 0..^ M )  -> 
( ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
) ) )
313312rexlimdv 2870 . . 3  |-  ( ph  ->  ( E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
) )
314196, 313mpd 15 . 2  |-  ( ph  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
)
315 0zd 10973 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
3163nnzd 11062 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
317 1zzd 10992 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ZZ )
318315, 316, 3173jca 1210 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )
)
319 0le1 10158 . . . . . . . . . 10  |-  0  <_  1
320319a1i 11 . . . . . . . . 9  |-  ( ph  ->  0  <_  1 )
3213nnge1d 10674 . . . . . . . . 9  |-  ( ph  ->  1  <_  M )
322318, 320, 321jca32 544 . . . . . . . 8  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
323 elfz2 11817 . . . . . . . 8  |-  ( 1  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
324322, 323sylibr 217 . . . . . . 7  |-  ( ph  ->  1  e.  ( 0 ... M ) )
325101, 324ffvelrnd 6038 . . . . . 6  |-  ( ph  ->  ( Q `  1
)  e.  RR )
326136, 52resubcld 10068 . . . . . 6  |-  ( ph  ->  ( ( Z `  X )  -  T
)  e.  RR )
327325, 326resubcld 10068 . . . . 5  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR )
328327adantr 472 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e.  RR )
32938recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  A  e.  CC )
330329, 225pncand 10006 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
331330adantr 472 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( A  +  T )  -  T )  =  A )
33243oveq2i 6319 . . . . . . . . . . 11  |-  ( A  +  T )  =  ( A  +  ( B  -  A ) )
333332a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  T )  =  ( A  +  ( B  -  A ) ) )
33440recnd 9687 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
335329, 334pncan3d 10008 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  ( B  -  A ) )  =  B )
336335adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  ( B  -  A ) )  =  B )
337 id 22 . . . . . . . . . . . 12  |-  ( ( E `  X )  =  B  ->  ( E `  X )  =  B )
338337eqcomd 2477 . . . . . . . . . . 11  |-  ( ( E `  X )  =  B  ->  B  =  ( E `  X ) )
339338adantl 473 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  B  =  ( E `  X ) )
340333, 336, 3393eqtrrd 2510 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( E `  X )  =  ( A  +  T ) )
341340oveq1d 6323 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( ( A  +  T
)  -  T ) )
34233adantr 472 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  A )
343331, 341, 3423eqtr4rd 2516 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( ( E `  X )  -  T
) )
344343oveq1d 6323 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  =  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) ) )
345139recnd 9687 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  CC )
346345, 217, 225nnncan2d 10040 . . . . . . 7  |-  ( ph  ->  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) )  =  ( ( E `  X )  -  ( Z `  X ) ) )
347346adantr 472 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( (
( E `  X
)  -  T )  -  ( ( Z `
 X )  -  T ) )  =  ( ( E `  X )  -  ( Z `  X )
) )
348219adantr 472 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  ( Z `  X ) )  =  X )
349344, 347, 3483eqtrrd 2510 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  =  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) ) )
35033, 38eqeltrd 2549 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  e.  RR )
3513nngt0d 10675 . . . . . . . . . 10  |-  ( ph  ->  0  <  M )
352 fzolb 11953 . . . . . . . . . 10  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
353315, 316, 351, 352syl3anbrc 1214 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0..^ M ) )
354 0re 9661 . . . . . . . . . 10  |-  0  e.  RR
355 eleq1 2537 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
356355anbi2d 718 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
357 fveq2 5879 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
358 oveq1 6315 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
359358fveq2d 5883 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
360357, 359breq12d 4408 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
361356, 360imbi12d 327 . . . . . . . . . . 11  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) ) ) )
362361, 152vtoclg 3093 . . . . . . . . . 10  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
363354, 362ax-mp 5 . . . . . . . . 9  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) )
364353, 363mpdan 681 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
365 0p1e1 10743 . . . . . . . . . 10  |-  ( 0  +  1 )  =  1
366365fveq2i 5882 . . . . . . . . 9  |-  ( Q `
 ( 0  +  1 ) )  =  ( Q `  1
)
367366a1i 11 . . . . . . . 8  |-  ( ph  ->  ( Q `  (
0  +  1 ) )  =  ( Q `
 1 ) )
368364, 367breqtrd 4420 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
369350, 325, 326, 368ltsub1dd 10246 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) )  <  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) )
370369adantr 472 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  < 
( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )
371349, 370eqbrtrd 4416 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  <  ( ( Q `  1
)  -  ( ( Z `  X )  -  T ) ) )
372 elioore 11691 . . . . . . . . 9  |-  ( y  e.  ( X (,) ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )  ->  y  e.  RR )
373135eqcomd 2477 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  =  ( Z `
 X ) )
374373negeqd 9889 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
375226, 374eqtrd 2505 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
376225mulid2d 9679 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  x.  T
)  =  T )
377375, 376oveq12d 6326 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  +  ( 1  x.  T ) )  =  ( -u ( Z `  X )  +  T ) )
378224negcld 9992 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u ( |_ `  ( ( B  -  X )  /  T
) )  e.  CC )
379 1cnd 9677 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  CC )
380378, 379, 225adddird 9686 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  ( (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  +  ( 1  x.  T ) ) )
381217, 225negsubdid 10020 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( Z `
 X )  -  T )  =  (
-u ( Z `  X )  +  T
) )
382377, 380, 3813eqtr4d 2515 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  -u (
( Z `  X
)  -  T ) )
383382oveq2d 6324 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) )  =  ( ( y  +  ( ( Z `  X
)  -  T ) )  +  -u (
( Z `  X
)  -  T ) ) )
384383adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  +  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T ) )  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  -u ( ( Z `  X )  -  T
) ) )
385326adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  RR )
386229, 385readdcld 9688 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
387386recnd 9687 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  CC )
388385recnd 9687 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  CC )
389387, 388negsubd 10011 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  +  -u ( ( Z `
 X )  -  T ) )  =  ( ( y  +  ( ( Z `  X )  -  T
) )  -  (
( Z `  X
)  -  T ) ) )
390235, 388pncand 10006 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  -  ( ( Z `
 X )  -  T ) )  =  y )
391384, 389, 3903eqtrrd 2510 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
392372, 391sylan2 482 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
393392adantlr 729 . . . . . . 7  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  y  =  ( ( y  +  ( ( Z `
 X )  -  T ) )  +  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
394 simpll 768 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ph )
395367eqcomd 2477 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  1
)  =  ( Q `
 ( 0  +  1 ) ) )
396395oveq2d 6324 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  =  ( ( Q `  0 ) (,) ( Q `  ( 0  +  1 ) ) ) )
397357, 359oveq12d 6326 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 0 ) (,) ( Q `  (
0  +  1 ) ) ) )
398397sseq1d 3445 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D  <->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) )
399356, 398imbi12d 327 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) ) )
400399, 241vtoclg 3093 . . . . . . . . . . . . 13  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) )
401354, 400ax-mp 5 . . . . . . . . . . . 12  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( ( Q `
 0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
)
402353, 401mpdan 681 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  ( 0  +  1 ) ) )  C_  D )
403396, 402eqsstrd 3452 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  C_  D )
404403ad2antrr 740 . . . . . . . . 9  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
( Q `  0
) (,) ( Q `
 1 ) ) 
C_  D )
40533, 39eqeltrd 2549 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
406405ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  e.  RR* )
407325rexrd 9708 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  1
)  e.  RR* )
408407ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  1 )  e.  RR* )
409372, 386sylan2 482 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
410409adantlr 729 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
y  +  ( ( Z `  X )  -  T ) )  e.  RR )
411345, 216, 217subaddd 10023 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( E `
 X )  -  X )  =  ( Z `  X )  <-> 
( X  +  ( Z `  X ) )  =  ( E `
 X ) ) )
412272, 411mpbird 240 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E `  X )  -  X
)  =  ( Z `
 X ) )
413 oveq1 6315 . . . . . . . . . . . . . . . 16  |-  ( ( E `  X )  =  B  ->  (
( E `  X
)  -  X )  =  ( B  -  X ) )
414412, 413sylan9req 2526 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Z `  X )  =  ( B  -  X ) )
415414oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Z `  X )  -  T )  =  ( ( B  -  X
)  -  T ) )
416415oveq2d 6324 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( X  +  ( ( Z `
 X )  -  T ) )  =  ( X  +  ( ( B  -  X
)  -  T ) ) )
417130recnd 9687 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  -  X
)  e.  CC )
418216, 417, 225addsubassd 10025 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( X  +  ( ( B  -  X )  -  T ) ) )
419418eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( ( B  -  X
)  -  T ) )  =  ( ( X  +  ( B  -  X ) )  -  T ) )
420419adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( X  +  ( ( B  -  X )  -  T ) )  =  ( ( X  +  ( B  -  X
) )  -  T
) )
421334, 225, 329subsub23d 37589 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  -  T )  =  A  <-> 
( B  -  A
)  =  T ) )
42258, 421mpbird 240 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  -  T
)  =  A )
423216, 334pncan3d 10008 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  +  ( B  -  X ) )  =  B )
424423oveq1d 6323 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( B  -  T ) )
425422, 424, 333eqtr4d 2515 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( Q `
 0 ) )
426425adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( X  +  ( B  -  X ) )  -  T )  =  ( Q `  0 ) )
427416, 420, 4263eqtrrd 2510 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( X  +  ( ( Z `  X
)  -  T ) ) )
428427adantr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  =  ( X  +  ( ( Z `  X )  -  T
) ) )
42974adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  X  e.  RR )
430372adantl 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  e.  RR )
431326adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( ( Z `  X )  -  T )  e.  RR )
432254adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  X  e.  RR* )
433327rexrd 9708 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR* )
434433adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e. 
RR* )
435 simpr 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( (