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 38005
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 463 . . . . . 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 37965 . . . . . . . . . . . 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 214 . . . . . . . . . 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 461 . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
9 elmapi 7490 . . . . . . . . 9  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
10 ffn 5726 . . . . . . . . 9  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
118, 9, 103syl 18 . . . . . . . 8  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
1211adantr 467 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  Q  Fn  ( 0 ... M
) )
13 fvelrnb 5910 . . . . . . 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 214 . . . . 5  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X ) )
16 0zd 10946 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  e.  ZZ )
17 elfzelz 11797 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
18173ad2ant2 1029 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  ZZ )
19 1zzd 10965 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  e.  ZZ )
2018, 19zsubcld 11042 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ZZ )
21 simpll 759 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  ->  ph )
22 elfzle1 11799 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
2322anim1i 571 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  <_ 
j  /\  -.  0  <  j ) )
24 0red 9641 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  e.  RR )
2517zred 11037 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
2625adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  e.  RR )
2724, 26eqleltd 9776 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  =  j  <->  ( 0  <_ 
j  /\  -.  0  <  j ) ) )
2823, 27mpbird 236 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  =  j )
2928eqcomd 2456 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  =  0 )
3029adantll 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
j  =  0 )
31 fveq2 5863 . . . . . . . . . . . . . . . 16  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
327simprld 764 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
3332simpld 461 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  =  A )
3431, 33sylan9eqr 2506 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  = 
0 )  ->  ( Q `  j )  =  A )
3521, 30, 34syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
( Q `  j
)  =  A )
36353adantl3 1165 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =  A )
37 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR )
3938rexrd 9687 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  RR* )
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
4140rexrd 9687 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  RR* )
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  <  B )
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  =  ( B  -  A
)
44 eqid 2450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
4538, 40, 42, 43, 44fourierdlem4 37967 . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
4940adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
5049, 48resubcld 10044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
5140, 38resubcld 10044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( B  -  A
)  e.  RR )
5243, 51syl5eqel 2532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  T  e.  RR )
5352adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
54 0red 9641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  0  e.  RR )
5538, 40posdifd 10197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
5642, 55mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  0  <  ( B  -  A ) )
5743eqcomi 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( B  -  A )  =  T
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( B  -  A
)  =  T )
5956, 58breqtrd 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  0  <  T )
6054, 59gtned 9767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  T  =/=  0 )
6160adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
6250, 53, 61redivcld 10432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
6362flcld 12031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
6463zred 11037 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
6564, 53remulcld 9668 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5955 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  RR  /\  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
)  e.  RR )  ->  ( Z `  x )  =  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
6848, 65, 67syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( Z `
 x )  =  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
6968oveq2d 6304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( Z `  x ) )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
7069mpteq2dva 4488 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7147, 70eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7271feq1d 5712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( E : RR --> ( A (,] B )  <-> 
( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) : RR --> ( A (,] B ) ) )
7345, 72mpbird 236 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  E : RR --> ( A (,] B ) )
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  RR )
7573, 74ffvelrnd 6021 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( E `  X
)  e.  ( A (,] B ) )
76 iocgtlb 37593 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 X )  e.  ( A (,] B
) )  ->  A  <  ( E `  X
) )
7739, 41, 75, 76syl3anc 1267 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  <  ( E `
 X ) )
7838, 77gtned 9767 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E `  X
)  =/=  A )
7978adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =/=  A
)
8037, 79eqnetrd 2690 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =/=  A
)
8180adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A
)
82813adantl2 1164 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A )
8382neneqd 2628 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  -.  ( Q `  j )  =  A )
8436, 83condan 802 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <  j )
85 zltlem1 10986 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  j  e.  ZZ )  ->  ( 0  <  j  <->  0  <_  ( j  - 
1 ) ) )
8616, 18, 85syl2anc 666 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  <  j  <->  0  <_  ( j  -  1 ) ) )
8784, 86mpbid 214 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  ( j  -  1 ) )
88 eluz2 11162 . . . . . . . . . . 11  |-  ( ( j  -  1 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( j  -  1 )  e.  ZZ  /\  0  <_ 
( j  -  1 ) ) )
8916, 20, 87, 88syl3anbrc 1191 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( ZZ>= `  0 )
)
90 elfzel2 11795 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
91903ad2ant2 1029 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  M  e.  ZZ )
92 1red 9655 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  1  e.  RR )
9325, 92resubcld 10044 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  RR )
9490zred 11037 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  M  e.  RR )
9525ltm1d 10536 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  j )
96 elfzle2 11800 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
9793, 25, 94, 95, 96ltletrd 9792 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  M )
98973ad2ant2 1029 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  < 
M )
99 elfzo2 11920 . . . . . . . . . 10  |-  ( ( j  -  1 )  e.  ( 0..^ M )  <->  ( ( j  -  1 )  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  ( j  -  1 )  <  M ) )
10089, 91, 98, 99syl3anbrc 1191 . . . . . . . . 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 1028 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  Q :
( 0 ... M
) --> RR )
10316, 91, 203jca 1187 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  ( j  -  1 )  e.  ZZ ) )
10493, 94, 97ltled 9780 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <_  M )
1051043ad2ant2 1029 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  <_  M )
106103, 87, 105jca32 538 . . . . . . . . . . . . 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 11788 . . . . . . . . . . . . 13  |-  ( ( j  -  1 )  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
108106, 107sylibr 216 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0 ... M
) )
109102, 108ffvelrnd 6021 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR )
110109rexrd 9687 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR* )
11125recnd 9666 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
112 1cnd 9656 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  1  e.  CC )
113111, 112npcand 9987 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( j  -  1 )  +  1 )  =  j )
114113fveq2d 5867 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
115114adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
116101ffvelrnda 6020 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR )
117116rexrd 9687 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
118115, 117eqeltrd 2528 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  e.  RR* )
1191183adant3 1027 . . . . . . . . . 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 5863 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  ( Z `  x )  =  ( Z `  X ) )
122120, 121oveq12d 6306 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
123122adantl 468 . . . . . . . . . . . . . 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 6296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
126125oveq1d 6303 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
127126fveq2d 5867 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
128127oveq1d 6303 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
129128adantl 468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  =  X )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
13040, 74resubcld 10044 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  -  X
)  e.  RR )
131130, 52, 60redivcld 10432 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
132131flcld 12031 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
133132zred 11037 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
134133, 52remulcld 9668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
135124, 129, 74, 134fvmptd 5952 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Z `  X
)  =  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
136135, 134eqeltrd 2528 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z `  X
)  e.  RR )
13774, 136readdcld 9667 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( Z `  X ) )  e.  RR )
13847, 123, 74, 137fvmptd 5952 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( Z `  X ) ) )
139138, 137eqeltrd 2528 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  X
)  e.  RR )
140139rexrd 9687 . . . . . . . . . . 11  |-  ( ph  ->  ( E `  X
)  e.  RR* )
1411403ad2ant1 1028 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  RR* )
142 simp1 1007 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ph )
143 ovex 6316 . . . . . . . . . . . . . 14  |-  ( j  -  1 )  e. 
_V
144 eleq1 2516 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  (
i  e.  ( 0..^ M )  <->  ( j  -  1 )  e.  ( 0..^ M ) ) )
145144anbi2d 709 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  - 
1 )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  ( j  -  1 )  e.  ( 0..^ M ) ) ) )
146 fveq2 5863 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  i )  =  ( Q `  ( j  -  1 ) ) )
147 oveq1 6295 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  (
i  +  1 )  =  ( ( j  -  1 )  +  1 ) )
148147fveq2d 5867 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
149146, 148breq12d 4414 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
150145, 149imbi12d 322 . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
152151r19.21bi 2756 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
153143, 150, 152vtocl 3099 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
154142, 100, 153syl2anc 666 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
1551143ad2ant2 1029 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  =  ( Q `  j ) )
156154, 155breqtrd 4426 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  j )
)
157 simp3 1009 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
158156, 157breqtrd 4426 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( E `  X )
)
159139leidd 10177 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  X
)  <_  ( E `  X ) )
160159adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( E `  X )
)
16137eqcomd 2456 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =  ( Q `  j ) )
162160, 161breqtrd 4426 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
1631623adant2 1026 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
164113eqcomd 2456 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  =  ( ( j  -  1 )  +  1 ) )
165164fveq2d 5867 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  j )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
1661653ad2ant2 1029 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( Q `  ( ( j  -  1 )  +  1 ) ) )
167163, 166breqtrd 4426 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  ( (
j  -  1 )  +  1 ) ) )
168110, 119, 141, 158, 167eliocd 37599 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) )
169146, 148oveq12d 6306 . . . . . . . . . . 11  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
170169eleq2d 2513 . . . . . . . . . 10  |-  ( i  =  ( j  - 
1 )  ->  (
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  <->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) ) )
171170rspcev 3149 . . . . . . . . 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 666 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
1731723exp 1206 . . . . . . 7  |-  ( ph  ->  ( j  e.  ( 0 ... M )  ->  ( ( Q `
 j )  =  ( E `  X
)  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) ) ) )
174173adantr 467 . . . . . 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 2876 . . . . 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 467 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  M  e.  NN )
178101adantr 467 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  Q : ( 0 ... M ) --> RR )
179 iocssicc 11719 . . . . . . . 8  |-  ( ( Q `  0 ) (,] ( Q `  M ) )  C_  ( ( Q ` 
0 ) [,] ( Q `  M )
)
18032simprd 465 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  =  B )
18133, 180oveq12d 6306 . . . . . . . . 9  |-  ( ph  ->  ( ( Q ` 
0 ) (,] ( Q `  M )
)  =  ( A (,] B ) )
18275, 181eleqtrrd 2531 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) (,] ( Q `  M ) ) )
183179, 182sseldi 3429 . . . . . . 7  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
184183adantr 467 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  -> 
( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
185 simpr 463 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  -.  ( E `  X
)  e.  ran  Q
)
186 fveq2 5863 . . . . . . . . 9  |-  ( k  =  j  ->  ( Q `  k )  =  ( Q `  j ) )
187186breq1d 4411 . . . . . . . 8  |-  ( k  =  j  ->  (
( Q `  k
)  <  ( E `  X )  <->  ( Q `  j )  <  ( E `  X )
) )
188187cbvrabv 3043 . . . . . . 7  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
( E `  X
) }  =  {
j  e.  ( 0..^ M )  |  ( Q `  j )  <  ( E `  X ) }
189188supeq1i 7958 . . . . . 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 37988 . . . . 5  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
191 ioossioc 37582 . . . . . . . 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 3430 . . . . . 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 2861 . . . . 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 799 . . 3  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
197101adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
198 elfzofz 11932 . . . . . . . . . 10  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
199198adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
200197, 199ffvelrnd 6021 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
2012003adant3 1027 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
2021363ad2ant1 1028 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Z `  X
)  e.  RR )
203201, 202resubcld 10044 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  e.  RR )
2041393ad2ant1 1028 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR )
205201rexrd 9687 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR* )
206 fzofzp1 12005 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
207206adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
208197, 207ffvelrnd 6021 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
209208rexrd 9687 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
2102093adant3 1027 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
211 simp3 1009 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
212 iocgtlb 37593 . . . . . . . . 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 1267 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( E `  X ) )
214201, 204, 202, 213ltsub1dd 10222 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  ( ( E `  X )  -  ( Z `  X ) ) )
215138oveq1d 6303 . . . . . . . . 9  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  ( ( X  +  ( Z `
 X ) )  -  ( Z `  X ) ) )
21674recnd 9666 . . . . . . . . . 10  |-  ( ph  ->  X  e.  CC )
217136recnd 9666 . . . . . . . . . 10  |-  ( ph  ->  ( Z `  X
)  e.  CC )
218216, 217pncand 9984 . . . . . . . . 9  |-  ( ph  ->  ( ( X  +  ( Z `  X ) )  -  ( Z `
 X ) )  =  X )
219215, 218eqtrd 2484 . . . . . . . 8  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  X )
2202193ad2ant1 1028 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( E `  X )  -  ( Z `  X )
)  =  X )
221214, 220breqtrd 4426 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  X )
222 elioore 11663 . . . . . . . . . . 11  |-  ( y  e.  ( ( ( Q `  i )  -  ( Z `  X ) ) (,) X )  ->  y  e.  RR )
223135oveq2d 6304 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  +  ( Z `  X ) )  =  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
224133recnd 9666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  CC )
22552recnd 9666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  CC )
226224, 225mulneg1d 10068 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )
227223, 226oveq12d 6306 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  =  ( ( y  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  +  -u (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
228227adantr 467 . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
230134adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  RR )
231229, 230readdcld 9667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  RR )
232231recnd 9666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  CC )
233230recnd 9666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  CC )
234232, 233negsubd 9989 . . . . . . . . . . . 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 9666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
236235, 233pncand 9984 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  -  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  =  y )
237228, 234, 2363eqtrrd 2489 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
238222, 237sylan2 477 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
2392383ad2antl1 1169 . . . . . . . . 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 1010 . . . . . . . . . 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 1027 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
243242adantr 467 . . . . . . . . . . 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 467 . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
247136adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
248246, 247readdcld 9667 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  RR )
2492483ad2antl1 1169 . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Z `  X )  e.  RR )
251200, 250resubcld 10044 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR )
252251rexrd 9687 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR* )
253252adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  e. 
RR* )
25474rexrd 9687 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  RR* )
255254ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR* )
256 simpr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )
257 ioogtlb 37586 . . . . . . . . . . . . . . 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 1267 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  < 
y )
259200adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  e.  RR )
260136ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
261222adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
262259, 260, 261ltsubaddd 10206 . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) )
2642633adantl3 1165 . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2672663adantl3 1165 . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR )
269 iooltub 37604 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR*  /\  X  e.  RR*  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
270253, 255, 256, 269syl3anc 1267 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
271261, 268, 260, 270ltadd1dd 10221 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( X  +  ( Z `  X ) ) )
272138eqcomd 2456 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  +  ( Z `  X ) )  =  ( E `
 X ) )
273272ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( X  +  ( Z `  X ) )  =  ( E `  X
) )
274271, 273breqtrd 4426 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( E `  X
) )
2752743adantl3 1165 . . . . . . . . . . . . 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 37594 . . . . . . . . . . . . . . 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 1267 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( Q `  ( i  +  1 ) ) )
278277adantr 467 . . . . . . . . . . . . 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 9792 . . . . . . . . . . . 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 37589 . . . . . . . . . . 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 3432 . . . . . . . . . 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 12031 . . . . . . . . . . 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 11039 . . . . . . . . . 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 9870 . . . . . . . . . . 11  |-  -u ( |_ `  ( ( B  -  X )  /  T ) )  e. 
_V
286 eleq1 2516 . . . . . . . . . . . . 13  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  e.  ZZ  <->  -u ( |_
`  ( ( B  -  X )  /  T ) )  e.  ZZ ) )
2872863anbi3d 1344 . . . . . . . . . . . 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 6295 . . . . . . . . . . . . . 14  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
289288oveq2d 6304 . . . . . . . . . . . . 13  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
290289eleq1d 2512 . . . . . . . . . . . 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 322 . . . . . . . . . . 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 6316 . . . . . . . . . . . 12  |-  ( y  +  ( Z `  X ) )  e. 
_V
293 eleq1 2516 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  e.  D  <->  ( y  +  ( Z `  X ) )  e.  D ) )
2942933anbi2d 1343 . . . . . . . . . . . . 13  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( ph  /\  x  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )
) )
295 oveq1 6295 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( k  x.  T
) ) )
296295eleq1d 2512 . . . . . . . . . . . . 13  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( x  +  ( k  x.  T ) )  e.  D  <->  ( (
y  +  ( Z `
 X ) )  +  ( k  x.  T ) )  e.  D ) )
297294, 296imbi12d 322 . . . . . . . . . . . 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 3099 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  e.  D )
300285, 291, 299vtocl 3099 . . . . . . . . . 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 1267 . . . . . . . . 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 2528 . . . . . . . 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 2801 . . . . . . 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 3421 . . . . . . 7  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) 
C_  D  <->  A. y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) y  e.  D )
305303, 304sylibr 216 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D )
306 breq1 4404 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y  <  X  <->  ( ( Q `
 i )  -  ( Z `  X ) )  <  X ) )
307 oveq1 6295 . . . . . . . . 9  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y (,) X )  =  ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) )
308307sseq1d 3458 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( (
y (,) X ) 
C_  D  <->  ( (
( Q `  i
)  -  ( Z `
 X ) ) (,) X )  C_  D ) )
309306, 308anbi12d 716 . . . . . . 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 3149 . . . . . 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 1265 . . . . 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 1206 . . . 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 2876 . . 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 10946 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
3163nnzd 11036 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
317 1zzd 10965 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ZZ )
318315, 316, 3173jca 1187 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )
)
319 0le1 10134 . . . . . . . . . 10  |-  0  <_  1
320319a1i 11 . . . . . . . . 9  |-  ( ph  ->  0  <_  1 )
3213nnge1d 10649 . . . . . . . . 9  |-  ( ph  ->  1  <_  M )
322318, 320, 321jca32 538 . . . . . . . 8  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
323 elfz2 11788 . . . . . . . 8  |-  ( 1  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
324322, 323sylibr 216 . . . . . . 7  |-  ( ph  ->  1  e.  ( 0 ... M ) )
325101, 324ffvelrnd 6021 . . . . . 6  |-  ( ph  ->  ( Q `  1
)  e.  RR )
326136, 52resubcld 10044 . . . . . 6  |-  ( ph  ->  ( ( Z `  X )  -  T
)  e.  RR )
327325, 326resubcld 10044 . . . . 5  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR )
328327adantr 467 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e.  RR )
32938recnd 9666 . . . . . . . . . 10  |-  ( ph  ->  A  e.  CC )
330329, 225pncand 9984 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
331330adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( A  +  T )  -  T )  =  A )
33243oveq2i 6299 . . . . . . . . . . 11  |-  ( A  +  T )  =  ( A  +  ( B  -  A ) )
333332a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  T )  =  ( A  +  ( B  -  A ) ) )
33440recnd 9666 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
335329, 334pncan3d 9986 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  ( B  -  A ) )  =  B )
336335adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  ( B  -  A ) )  =  B )
337 id 22 . . . . . . . . . . . 12  |-  ( ( E `  X )  =  B  ->  ( E `  X )  =  B )
338337eqcomd 2456 . . . . . . . . . . 11  |-  ( ( E `  X )  =  B  ->  B  =  ( E `  X ) )
339338adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  B  =  ( E `  X ) )
340333, 336, 3393eqtrrd 2489 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( E `  X )  =  ( A  +  T ) )
341340oveq1d 6303 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( ( A  +  T
)  -  T ) )
34233adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  A )
343331, 341, 3423eqtr4rd 2495 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( ( E `  X )  -  T
) )
344343oveq1d 6303 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  =  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) ) )
345139recnd 9666 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  CC )
346345, 217, 225nnncan2d 10018 . . . . . . 7  |-  ( ph  ->  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) )  =  ( ( E `  X )  -  ( Z `  X ) ) )
347346adantr 467 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( (
( E `  X
)  -  T )  -  ( ( Z `
 X )  -  T ) )  =  ( ( E `  X )  -  ( Z `  X )
) )
348219adantr 467 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  ( Z `  X ) )  =  X )
349344, 347, 3483eqtrrd 2489 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  =  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) ) )
35033, 38eqeltrd 2528 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  e.  RR )
3513nngt0d 10650 . . . . . . . . . 10  |-  ( ph  ->  0  <  M )
352 fzolb 11923 . . . . . . . . . 10  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
353315, 316, 351, 352syl3anbrc 1191 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0..^ M ) )
354 0re 9640 . . . . . . . . . 10  |-  0  e.  RR
355 eleq1 2516 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
356355anbi2d 709 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
357 fveq2 5863 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
358 oveq1 6295 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
359358fveq2d 5867 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
360357, 359breq12d 4414 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
361356, 360imbi12d 322 . . . . . . . . . . 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 3106 . . . . . . . . . 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 673 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
365 0p1e1 10718 . . . . . . . . . 10  |-  ( 0  +  1 )  =  1
366365fveq2i 5866 . . . . . . . . 9  |-  ( Q `
 ( 0  +  1 ) )  =  ( Q `  1
)
367366a1i 11 . . . . . . . 8  |-  ( ph  ->  ( Q `  (
0  +  1 ) )  =  ( Q `
 1 ) )
368364, 367breqtrd 4426 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
369350, 325, 326, 368ltsub1dd 10222 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) )  <  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) )
370369adantr 467 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  < 
( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )
371349, 370eqbrtrd 4422 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  <  ( ( Q `  1
)  -  ( ( Z `  X )  -  T ) ) )
372 elioore 11663 . . . . . . . . 9  |-  ( y  e.  ( X (,) ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )  ->  y  e.  RR )
373135eqcomd 2456 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  =  ( Z `
 X ) )
374373negeqd 9866 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
375226, 374eqtrd 2484 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
376225mulid2d 9658 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  x.  T
)  =  T )
377375, 376oveq12d 6306 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  +  ( 1  x.  T ) )  =  ( -u ( Z `  X )  +  T ) )
378224negcld 9970 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u ( |_ `  ( ( B  -  X )  /  T
) )  e.  CC )
379 1cnd 9656 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  CC )
380378, 379, 225adddird 9665 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  ( (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  +  ( 1  x.  T ) ) )
381217, 225negsubdid 9998 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( Z `
 X )  -  T )  =  (
-u ( Z `  X )  +  T
) )
382377, 380, 3813eqtr4d 2494 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  -u (
( Z `  X
)  -  T ) )
383382oveq2d 6304 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) )  =  ( ( y  +  ( ( Z `  X
)  -  T ) )  +  -u (
( Z `  X
)  -  T ) ) )
384383adantr 467 . . . . . . . . . 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 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  RR )
386229, 385readdcld 9667 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
387386recnd 9666 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  CC )
388385recnd 9666 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  CC )
389387, 388negsubd 9989 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  +  -u ( ( Z `
 X )  -  T ) )  =  ( ( y  +  ( ( Z `  X )  -  T
) )  -  (
( Z `  X
)  -  T ) ) )
390235, 388pncand 9984 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  -  ( ( Z `
 X )  -  T ) )  =  y )
391384, 389, 3903eqtrrd 2489 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
392372, 391sylan2 477 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
393392adantlr 720 . . . . . . 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 759 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ph )
395367eqcomd 2456 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  1
)  =  ( Q `
 ( 0  +  1 ) ) )
396395oveq2d 6304 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  =  ( ( Q `  0 ) (,) ( Q `  ( 0  +  1 ) ) ) )
397357, 359oveq12d 6306 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 0 ) (,) ( Q `  (
0  +  1 ) ) ) )
398397sseq1d 3458 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D  <->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) )
399356, 398imbi12d 322 . . . . . . . . . . . . . 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 3106 . . . . . . . . . . . . 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 673 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  ( 0  +  1 ) ) )  C_  D )
403396, 402eqsstrd 3465 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  C_  D )
404403ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
( Q `  0
) (,) ( Q `
 1 ) ) 
C_  D )
40533, 39eqeltrd 2528 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
406405ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  e.  RR* )
407325rexrd 9687 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  1
)  e.  RR* )
408407ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  1 )  e.  RR* )
409372, 386sylan2 477 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
410409adantlr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
y  +  ( ( Z `  X )  -  T ) )  e.  RR )
411345, 216, 217subaddd 10001 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( E `
 X )  -  X )  =  ( Z `  X )  <-> 
( X  +  ( Z `  X ) )  =  ( E `
 X ) ) )
412272, 411mpbird 236 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E `  X )  -  X
)  =  ( Z `
 X ) )
413 oveq1 6295 . . . . . . . . . . . . . . . 16  |-  ( ( E `  X )  =  B  ->  (
( E `  X
)  -  X )  =  ( B  -  X ) )
414412, 413sylan9req 2505 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Z `  X )  =  ( B  -  X ) )
415414oveq1d 6303 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Z `  X )  -  T )  =  ( ( B  -  X
)  -  T ) )
416415oveq2d 6304 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( X  +  ( ( Z `
 X )  -  T ) )  =  ( X  +  ( ( B  -  X
)  -  T ) ) )
417130recnd 9666 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  -  X
)  e.  CC )
418216, 417, 225addsubassd 10003 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( X  +  ( ( B  -  X )  -  T ) ) )
419418eqcomd 2456 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( ( B  -  X
)  -  T ) )  =  ( ( X  +  ( B  -  X ) )  -  T ) )
420419adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( X  +  ( ( B  -  X )  -  T ) )  =  ( ( X  +  ( B  -  X
) )  -  T
) )
421334, 225, 329subsub23d 37494 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  -  T )  =  A  <-> 
( B  -  A
)  =  T ) )
42258, 421mpbird 236 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  -  T
)  =  A )
423216, 334pncan3d 9986 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  +  ( B  -  X ) )  =  B )
424423oveq1d 6303 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( B  -  T ) )
425422, 424, 333eqtr4d 2494 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( Q `
 0 ) )
426425adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( X  +  ( B  -  X ) )  -  T )  =  ( Q `  0 ) )
427416, 420, 4263eqtrrd 2489 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( X  +  ( ( Z `  X
)  -  T ) ) )
428427adantr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  =  ( X  +  ( ( Z `  X )  -  T
) ) )
42974adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  X  e.  RR )
430372adantl 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  e.  RR )
431326adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( ( Z `  X )  -  T )  e.  RR )
432254adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  X  e.  RR* )
433327rexrd 9687 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR* )
434433adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e. 
RR* )
435 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( (