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

Theorem fourierdlem41 31771
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 461 . . . . . 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 31732 . . . . . . . . . . . 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 16 . . . . . . . . . . 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 210 . . . . . . . . . 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 459 . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
9 elmapi 7452 . . . . . . . . 9  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
10 ffn 5737 . . . . . . . . 9  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
118, 9, 103syl 20 . . . . . . . 8  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
1211adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  Q  Fn  ( 0 ... M
) )
13 fvelrnb 5921 . . . . . . 7  |-  ( Q  Fn  ( 0 ... M )  ->  (
( E `  X
)  e.  ran  Q  <->  E. j  e.  ( 0 ... M ) ( Q `  j )  =  ( E `  X ) ) )
1412, 13syl 16 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  ( ( E `  X )  e.  ran  Q  <->  E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X ) ) )
151, 14mpbid 210 . . . . 5  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X ) )
16 0zd 10888 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  e.  ZZ )
17 elfzelz 11700 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
18173ad2ant2 1018 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  ZZ )
19 1zzd 10907 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  e.  ZZ )
2018, 19zsubcld 10983 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ZZ )
21 simpll 753 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  ->  ph )
22 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
2322anim1i 568 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  <_ 
j  /\  -.  0  <  j ) )
24 0red 9609 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  e.  RR )
2517zred 10978 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
2625adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  e.  RR )
2724, 26eqleltd 9740 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  =  j  <->  ( 0  <_ 
j  /\  -.  0  <  j ) ) )
2823, 27mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  =  j )
2928eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  =  0 )
3029adantll 713 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
j  =  0 )
31 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
3231adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  = 
0 )  ->  ( Q `  j )  =  ( Q ` 
0 ) )
337simprld 31320 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
3433simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q `  0
)  =  A )
3534adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  = 
0 )  ->  ( Q `  0 )  =  A )
36 eqidd 2468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  = 
0 )  ->  A  =  A )
3732, 35, 363eqtrd 2512 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  = 
0 )  ->  ( Q `  j )  =  A )
3821, 30, 37syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
( Q `  j
)  =  A )
39383adantl3 1154 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =  A )
40 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
41 fourierdlem41.a . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  RR )
4241rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  RR* )
43 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  RR )
4443rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  RR* )
45 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  <  B )
46 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  T  =  ( B  -  A
)
47 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
4841, 43, 45, 46, 47fourierdlem4 31734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) : RR --> ( A (,] B ) )
49 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )
5049a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) ) )
51 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
5243adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
5352, 51resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
5443, 41resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( B  -  A
)  e.  RR )
5546, 54syl5eqel 2559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  T  e.  RR )
5655adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
57 0red 9609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  0  e.  RR )
5841, 43posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
5945, 58mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  0  <  ( B  -  A ) )
6046eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( B  -  A )  =  T
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( B  -  A
)  =  T )
6259, 61breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  0  <  T )
6357, 62gtned 9731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  T  =/=  0 )
6463adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
6553, 56, 64redivcld 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
6665flcld 11915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
6766zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
6867, 56remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
69 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
7069fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  RR  /\  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
)  e.  RR )  ->  ( Z `  x )  =  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
7151, 68, 70syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( Z `
 x )  =  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
7271oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( Z `  x ) )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
7372mpteq2dva 4539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7450, 73eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7574feq1d 5723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( E : RR --> ( A (,] B )  <-> 
( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) : RR --> ( A (,] B ) ) )
7648, 75mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  E : RR --> ( A (,] B ) )
77 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  X  e.  RR )
7876, 77ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( E `  X
)  e.  ( A (,] B ) )
79 iocgtlb 31422 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 X )  e.  ( A (,] B
) )  ->  A  <  ( E `  X
) )
8042, 44, 78, 79syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  <  ( E `
 X ) )
8141, 80gtned 9731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( E `  X
)  =/=  A )
8281adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =/=  A
)
8340, 82eqnetrd 2760 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =/=  A
)
8483adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A
)
85843adantl2 1153 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A )
8685neneqd 2669 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  -.  ( Q `  j )  =  A )
8739, 86condan 792 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <  j )
88 zltlem1 10927 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  ZZ  /\  j  e.  ZZ )  ->  ( 0  <  j  <->  0  <_  ( j  - 
1 ) ) )
8916, 18, 88syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  <  j  <->  0  <_  ( j  -  1 ) ) )
9087, 89mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  ( j  -  1 ) )
9116, 20, 903jca 1176 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  e.  ZZ  /\  (
j  -  1 )  e.  ZZ  /\  0  <_  ( j  -  1 ) ) )
92 eluz2 11100 . . . . . . . . . . . 12  |-  ( ( j  -  1 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( j  -  1 )  e.  ZZ  /\  0  <_ 
( j  -  1 ) ) )
9391, 92sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( ZZ>= `  0 )
)
94 elfzel2 11698 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
95943ad2ant2 1018 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  M  e.  ZZ )
96 1red 9623 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  1  e.  RR )
9725, 96resubcld 9999 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  RR )
9894zred 10978 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  M  e.  RR )
9925ltm1d 10490 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  j )
100 elfzle2 11702 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
10197, 25, 98, 99, 100ltletrd 9753 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  M )
1021013ad2ant2 1018 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  < 
M )
10393, 95, 1023jca 1176 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( (
j  -  1 )  e.  ( ZZ>= `  0
)  /\  M  e.  ZZ  /\  ( j  - 
1 )  <  M
) )
104 elfzo2 11812 . . . . . . . . . 10  |-  ( ( j  -  1 )  e.  ( 0..^ M )  <->  ( ( j  -  1 )  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  ( j  -  1 )  <  M ) )
105103, 104sylibr 212 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0..^ M ) )
1068, 9syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
1071063ad2ant1 1017 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  Q :
( 0 ... M
) --> RR )
10816, 95, 203jca 1176 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  ( j  -  1 )  e.  ZZ ) )
10997, 98, 101ltled 9744 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <_  M )
1101093ad2ant2 1018 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  <_  M )
111108, 90, 110jca32 535 . . . . . . . . . . . . 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
) ) )
112 elfz2 11691 . . . . . . . . . . . . 13  |-  ( ( j  -  1 )  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
113111, 112sylibr 212 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0 ... M
) )
114107, 113ffvelrnd 6033 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR )
115114rexrd 9655 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR* )
11625recnd 9634 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
117 1cnd 9624 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  1  e.  CC )
118116, 117npcand 9946 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( j  -  1 )  +  1 )  =  j )
119118fveq2d 5876 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
120119adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
121106ffvelrnda 6032 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR )
122121rexrd 9655 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
123120, 122eqeltrd 2555 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  e.  RR* )
1241233adant3 1016 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  e.  RR* )
125 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  x  =  X )
126 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  ( Z `  x )  =  ( Z `  X ) )
127125, 126oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
128127adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  X )  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
12969a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
130 oveq2 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
131130oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
132131fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
133132oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
134133adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  =  X )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
13543, 77resubcld 9999 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  -  X
)  e.  RR )
136135, 55, 63redivcld 10384 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
137136flcld 11915 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
138137zred 10978 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
139138, 55remulcld 9636 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
140129, 134, 77, 139fvmptd 5962 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Z `  X
)  =  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
141140, 139eqeltrd 2555 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z `  X
)  e.  RR )
14277, 141readdcld 9635 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( Z `  X ) )  e.  RR )
14350, 128, 77, 142fvmptd 5962 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( Z `  X ) ) )
144143, 142eqeltrd 2555 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  X
)  e.  RR )
145144rexrd 9655 . . . . . . . . . . 11  |-  ( ph  ->  ( E `  X
)  e.  RR* )
1461453ad2ant1 1017 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  RR* )
147 simp1 996 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ph )
148 ovex 6320 . . . . . . . . . . . . . 14  |-  ( j  -  1 )  e. 
_V
149 eleq1 2539 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  (
i  e.  ( 0..^ M )  <->  ( j  -  1 )  e.  ( 0..^ M ) ) )
150149anbi2d 703 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  ( j  -  1 )  e.  ( 0..^ M ) ) ) )
151 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  i )  =  ( Q `  ( j  -  1 ) ) )
152 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  - 
1 )  ->  (
i  +  1 )  =  ( ( j  -  1 )  +  1 ) )
153152fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
154151, 153breq12d 4466 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
155150, 154imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) ) )
1567simprrd 31328 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
157156r19.21bi 2836 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
158155, 157vtoclg 3176 . . . . . . . . . . . . . 14  |-  ( ( j  -  1 )  e.  _V  ->  (
( ph  /\  (
j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( ( j  - 
1 )  +  1 ) ) ) )
159148, 158ax-mp 5 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
160147, 105, 159syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
1611193ad2ant2 1018 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  =  ( Q `  j ) )
162160, 161breqtrd 4477 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  j )
)
163 simp3 998 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
164162, 163breqtrd 4477 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( E `  X )
)
165144leidd 10131 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  X
)  <_  ( E `  X ) )
166165adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( E `  X )
)
16740eqcomd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =  ( Q `  j ) )
168166, 167breqtrd 4477 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
1691683adant2 1015 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
170118eqcomd 2475 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  =  ( ( j  -  1 )  +  1 ) )
171170fveq2d 5876 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  j )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
1721713ad2ant2 1018 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( Q `  ( ( j  -  1 )  +  1 ) ) )
173169, 172breqtrd 4477 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  ( (
j  -  1 )  +  1 ) ) )
174115, 124, 146, 164, 173eliocd 31430 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) )
175151, 153oveq12d 6313 . . . . . . . . . . 11  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
176175eleq2d 2537 . . . . . . . . . 10  |-  ( i  =  ( j  - 
1 )  ->  (
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  <->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) ) )
177176rspcev 3219 . . . . . . . . 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 ) ) ) )
178105, 174, 177syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
1791783exp 1195 . . . . . . 7  |-  ( ph  ->  ( j  e.  ( 0 ... M )  ->  ( ( Q `
 j )  =  ( E `  X
)  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) ) ) )
180179adantr 465 . . . . . 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 ) ) ) ) ) )
181180rexlimdv 2957 . . . . 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 ) ) ) ) )
18215, 181mpd 15 . . . 4  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
1833adantr 465 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  M  e.  NN )
184106adantr 465 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  Q : ( 0 ... M ) --> RR )
185 iocssicc 11624 . . . . . . . 8  |-  ( ( Q `  0 ) (,] ( Q `  M ) )  C_  ( ( Q ` 
0 ) [,] ( Q `  M )
)
18633simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  M
)  =  B )
18734, 186oveq12d 6313 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q ` 
0 ) (,] ( Q `  M )
)  =  ( A (,] B ) )
188187eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  ( A (,] B
)  =  ( ( Q `  0 ) (,] ( Q `  M ) ) )
18978, 188eleqtrd 2557 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) (,] ( Q `  M ) ) )
190185, 189sseldi 3507 . . . . . . 7  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
191190adantr 465 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  -> 
( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
192 simpr 461 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  -.  ( E `  X
)  e.  ran  Q
)
193 fveq2 5872 . . . . . . . . 9  |-  ( k  =  j  ->  ( Q `  k )  =  ( Q `  j ) )
194193breq1d 4463 . . . . . . . 8  |-  ( k  =  j  ->  (
( Q `  k
)  <  ( E `  X )  <->  ( Q `  j )  <  ( E `  X )
) )
195194cbvrabv 3117 . . . . . . 7  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
( E `  X
) }  =  {
j  e.  ( 0..^ M )  |  ( Q `  j )  <  ( E `  X ) }
196195supeq1i 7919 . . . . . 6  |-  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k
)  <  ( E `  X ) } ,  RR ,  <  )  =  sup ( { j  e.  ( 0..^ M )  |  ( Q `
 j )  < 
( E `  X
) } ,  RR ,  <  )
197183, 184, 191, 192, 196fourierdlem25 31755 . . . . 5  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
198 ioossioc 31411 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )
199198a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  -.  ( E `  X )  e.  ran  Q )  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )
200199sseld 3508 . . . . . 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 ) ) ) ) )
201200reximdva 2942 . . . . 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 ) ) ) ) )
202197, 201mpd 15 . . . 4  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
203182, 202pm2.61dan 789 . . 3  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
204106adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
205 elfzofz 11823 . . . . . . . . . 10  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
206205adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
207204, 206ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
2082073adant3 1016 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
2091413ad2ant1 1017 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Z `  X
)  e.  RR )
210208, 209resubcld 9999 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  e.  RR )
2111443ad2ant1 1017 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR )
212208rexrd 9655 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR* )
213 fzofzp1 11889 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
214213adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
215204, 214ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
216215rexrd 9655 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
2172163adant3 1016 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
218 simp3 998 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
219 iocgtlb 31422 . . . . . . . . . 10  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( E `  X
) )
220212, 217, 218, 219syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( E `  X ) )
221208, 211, 209, 220ltsub1dd 10176 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  ( ( E `  X )  -  ( Z `  X ) ) )
222143oveq1d 6310 . . . . . . . . . 10  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  ( ( X  +  ( Z `
 X ) )  -  ( Z `  X ) ) )
22377recnd 9634 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  CC )
224141recnd 9634 . . . . . . . . . . 11  |-  ( ph  ->  ( Z `  X
)  e.  CC )
225223, 224pncand 9943 . . . . . . . . . 10  |-  ( ph  ->  ( ( X  +  ( Z `  X ) )  -  ( Z `
 X ) )  =  X )
226222, 225eqtrd 2508 . . . . . . . . 9  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  X )
2272263ad2ant1 1017 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( E `  X )  -  ( Z `  X )
)  =  X )
228221, 227breqtrd 4477 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  X )
229 simpl 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ph )
230 elioore 11571 . . . . . . . . . . . . 13  |-  ( y  e.  ( ( ( Q `  i )  -  ( Z `  X ) ) (,) X )  ->  y  e.  RR )
231230adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
232140oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  +  ( Z `  X ) )  =  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
233138recnd 9634 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  CC )
23455recnd 9634 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  CC )
235233, 234mulneg1d 10021 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )
236232, 235oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  =  ( ( y  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  +  -u (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
237236adantr 465 . . . . . . . . . . . . 13  |-  ( (
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
) ) )
238 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
239139adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  RR )
240238, 239readdcld 9635 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  RR )
241240recnd 9634 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  CC )
242239recnd 9634 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  CC )
243241, 242negsubd 9948 . . . . . . . . . . . . 13  |-  ( (
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 ) ) )
244238recnd 9634 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
245244, 242pncand 9943 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  -  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  =  y )
246237, 243, 2453eqtrrd 2513 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
247229, 231, 246syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
2482473ad2antl1 1158 . . . . . . . . . 10  |-  ( ( ( 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
) ) )
249 simpl1 999 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ph )
250 fourierdlem41.qssd . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
2512503adant3 1016 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
252251adantr 465 . . . . . . . . . . . 12  |-  ( ( ( 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
)
253212adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  e.  RR* )
254217adantr 465 . . . . . . . . . . . . 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* )
255141adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
256231, 255readdcld 9635 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  RR )
2572563ad2antl1 1158 . . . . . . . . . . . . 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.  RR )
258141adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Z `  X )  e.  RR )
259207, 258resubcld 9999 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR )
260259rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR* )
261260adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  e. 
RR* )
26277rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  RR* )
263262ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR* )
264 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )
265 ioogtlb 31415 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR*  /\  X  e.  RR*  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  < 
y )
266261, 263, 264, 265syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  < 
y )
267207adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  e.  RR )
268255adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
269230adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
270267, 268, 269ltsubaddd 10160 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( (
( Q `  i
)  -  ( Z `
 X ) )  <  y  <->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) ) )
271266, 270mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) )
2722713adantl3 1154 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
273249, 144syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( E `  X )  e.  RR )
274215adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2752743adantl3 1154 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
27677ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR )
277 iooltub 31435 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR*  /\  X  e.  RR*  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
278261, 263, 264, 277syl3anc 1228 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
279269, 276, 268, 278ltadd1dd 10175 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( X  +  ( Z `  X ) ) )
280143eqcomd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( X  +  ( Z `  X ) )  =  ( E `
 X ) )
281280ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( X  +  ( Z `  X ) )  =  ( E `  X
) )
282279, 281breqtrd 4477 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( E `  X
) )
2832823adantl3 1154 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) )
284 iocleub 31423 . . . . . . . . . . . . . . . 16  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( E `  X )  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )  ->  ( E `  X )  <_  ( Q `  (
i  +  1 ) ) )
285212, 217, 218, 284syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( Q `  ( i  +  1 ) ) )
286285adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
287257, 273, 275, 283, 286ltletrd 9753 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
288253, 254, 257, 272, 287eliood 31418 . . . . . . . . . . . 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.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
289252, 288sseldd 3510 . . . . . . . . . . 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.  D )
290249, 136syl 16 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
291290flcld 11915 . . . . . . . . . . . 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.  ZZ )
292291znegcld 10980 . . . . . . . . . . 11  |-  ( ( ( 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 )
293 negex 9830 . . . . . . . . . . . 12  |-  -u ( |_ `  ( ( B  -  X )  /  T ) )  e. 
_V
294 eleq1 2539 . . . . . . . . . . . . . . 15  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  e.  ZZ  <->  -u ( |_
`  ( ( B  -  X )  /  T ) )  e.  ZZ ) )
2952943anbi3d 1305 . . . . . . . . . . . . . 14  |-  ( 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 ) ) )
296 oveq1 6302 . . . . . . . . . . . . . . . 16  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
297296oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
298297eleq1d 2536 . . . . . . . . . . . . . 14  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( ( y  +  ( Z `  X
) )  +  ( k  x.  T ) )  e.  D  <->  ( (
y  +  ( Z `
 X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D ) )
299295, 298imbi12d 320 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
300 ovex 6320 . . . . . . . . . . . . . 14  |-  ( y  +  ( Z `  X ) )  e. 
_V
301 eleq1 2539 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  e.  D  <->  ( y  +  ( Z `  X ) )  e.  D ) )
3023013anbi2d 1304 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( ph  /\  x  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )
) )
303 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( k  x.  T
) ) )
304303eleq1d 2536 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( x  +  ( k  x.  T ) )  e.  D  <->  ( (
y  +  ( Z `
 X ) )  +  ( k  x.  T ) )  e.  D ) )
305302, 304imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) )
306 fourierdlem41.dper . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T
) )  e.  D
)
307305, 306vtoclg 3176 . . . . . . . . . . . . . 14  |-  ( ( y  +  ( Z `
 X ) )  e.  _V  ->  (
( ph  /\  (
y  +  ( Z `
 X ) )  e.  D  /\  k  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  e.  D ) )
308300, 307ax-mp 5 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  e.  D )
309299, 308vtoclg 3176 . . . . . . . . . . . 12  |-  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  e.  _V  ->  (
( ph  /\  (
y  +  ( Z `
 X ) )  e.  D  /\  -u ( |_ `  ( ( B  -  X )  /  T ) )  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D ) )
310293, 309ax-mp 5 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  -u ( |_ `  ( ( B  -  X )  /  T ) )  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  D )
311249, 289, 292, 310syl3anc 1228 . . . . . . . . . 10  |-  ( ( ( 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 )
312248, 311eqeltrd 2555 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  D )
313312ralrimiva 2881 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  A. y  e.  (
( ( Q `  i )  -  ( Z `  X )
) (,) X ) y  e.  D )
314 dfss3 3499 . . . . . . . 8  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) 
C_  D  <->  A. y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) y  e.  D )
315313, 314sylibr 212 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D )
316228, 315jca 532 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i )  -  ( Z `  X ) )  <  X  /\  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D ) )
317 breq1 4456 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y  <  X  <->  ( ( Q `
 i )  -  ( Z `  X ) )  <  X ) )
318 oveq1 6302 . . . . . . . . 9  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y (,) X )  =  ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) )
319318sseq1d 3536 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( (
y (,) X ) 
C_  D  <->  ( (
( Q `  i
)  -  ( Z `
 X ) ) (,) X )  C_  D ) )
320317, 319anbi12d 710 . . . . . . 7  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( (
y  <  X  /\  ( y (,) X
)  C_  D )  <->  ( ( ( Q `  i )  -  ( Z `  X )
)  <  X  /\  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D ) ) )
321320rspcev 3219 . . . . . 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 )
)
322210, 316, 321syl2anc 661 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
)
3233223exp 1195 . . . 4  |-  ( ph  ->  ( i  e.  ( 0..^ M )  -> 
( ( E `  X )  e.  ( ( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
) ) )
324323rexlimdv 2957 . . 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 )
) )
325203, 324mpd 15 . 2  |-  ( ph  ->  E. y  e.  RR  ( y  <  X  /\  ( y (,) X
)  C_  D )
)
326 0zd 10888 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
3273nnzd 10977 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
328 1zzd 10907 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ZZ )
329326, 327, 3283jca 1176 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )
)
330 0le1 10088 . . . . . . . . . 10  |-  0  <_  1
331330a1i 11 . . . . . . . . 9  |-  ( ph  ->  0  <_  1 )
3323nnge1d 10590 . . . . . . . . 9  |-  ( ph  ->  1  <_  M )
333329, 331, 332jca32 535 . . . . . . . 8  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
334 elfz2 11691 . . . . . . . 8  |-  ( 1  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
335333, 334sylibr 212 . . . . . . 7  |-  ( ph  ->  1  e.  ( 0 ... M ) )
336106, 335ffvelrnd 6033 . . . . . 6  |-  ( ph  ->  ( Q `  1
)  e.  RR )
337141, 55resubcld 9999 . . . . . 6  |-  ( ph  ->  ( ( Z `  X )  -  T
)  e.  RR )
338336, 337resubcld 9999 . . . . 5  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR )
339338adantr 465 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e.  RR )
34034adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  A )
34146oveq2i 6306 . . . . . . . . . . . . 13  |-  ( A  +  T )  =  ( A  +  ( B  -  A ) )
342341a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  T )  =  ( A  +  ( B  -  A ) ) )
34341recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  CC )
34443recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  CC )
345343, 344pncan3d 9945 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  ( B  -  A ) )  =  B )
346345adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  ( B  -  A ) )  =  B )
347 id 22 . . . . . . . . . . . . . 14  |-  ( ( E `  X )  =  B  ->  ( E `  X )  =  B )
348347eqcomd 2475 . . . . . . . . . . . . 13  |-  ( ( E `  X )  =  B  ->  B  =  ( E `  X ) )
349348adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  B  =  ( E `  X ) )
350342, 346, 3493eqtrrd 2513 . . . . . . . . . . 11  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( E `  X )  =  ( A  +  T ) )
351350oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( ( A  +  T
)  -  T ) )
352343, 234pncand 9943 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
353352adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( A  +  T )  -  T )  =  A )
354351, 353eqtr2d 2509 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  A  =  ( ( E `  X )  -  T
) )
355 eqidd 2468 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( ( E `  X
)  -  T ) )
356340, 354, 3553eqtrd 2512 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( ( E `  X )  -  T
) )
357356oveq1d 6310 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  =  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) ) )
358144recnd 9634 . . . . . . . . 9  |-  ( ph  ->  ( E `  X
)  e.  CC )
359358, 224, 234nnncan2d 9977 . . . . . . . 8  |-  ( ph  ->  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) )  =  ( ( E `  X )  -  ( Z `  X ) ) )
360359adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( (
( E `  X
)  -  T )  -  ( ( Z `
 X )  -  T ) )  =  ( ( E `  X )  -  ( Z `  X )
) )
361226adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  ( Z `  X ) )  =  X )
362357, 360, 3613eqtrrd 2513 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  =  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) ) )
36334, 41eqeltrd 2555 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  e.  RR )
364 id 22 . . . . . . . . . 10  |-  ( ph  ->  ph )
3653nngt0d 10591 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  M )
366326, 327, 3653jca 1176 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <  M ) )
367 fzolb 11814 . . . . . . . . . . 11  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
368366, 367sylibr 212 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( 0..^ M ) )
369 0re 9608 . . . . . . . . . . 11  |-  0  e.  RR
370 eleq1 2539 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
371370anbi2d 703 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
372 fveq2 5872 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
373 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
374373fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
375372, 374breq12d 4466 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
376371, 375imbi12d 320 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) ) ) )
377376, 157vtoclg 3176 . . . . . . . . . . 11  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
378369, 377ax-mp 5 . . . . . . . . . 10  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) )
379364, 368, 378syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
380 0p1e1 10659 . . . . . . . . . . 11  |-  ( 0  +  1 )  =  1
381380fveq2i 5875 . . . . . . . . . 10  |-  ( Q `
 ( 0  +  1 ) )  =  ( Q `  1
)
382381a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( Q `  (
0  +  1 ) )  =  ( Q `
 1 ) )
383379, 382breqtrd 4477 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
384363, 336, 337, 383ltsub1dd 10176 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) )  <  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) )
385384adantr 465 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  < 
( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )
386362, 385eqbrtrd 4473 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  <  ( ( Q `  1
)  -  ( ( Z `  X )  -  T ) ) )
387 simpl 457 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ph )
388 elioore 11571 . . . . . . . . . . 11  |-  ( y  e.  ( X (,) ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )  ->  y  e.  RR )
389388adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  e.  RR )
390233negcld 9929 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u ( |_ `  ( ( B  -  X )  /  T
) )  e.  CC )
391 1cnd 9624 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
392390, 391, 234adddird 9633 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  ( (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  +  ( 1  x.  T ) ) )
393140eqcomd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  =  ( Z `
 X ) )
394393negeqd 9826 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
395235, 394eqtrd 2508 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
396234mulid2d 9626 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  x.  T
)  =  T )
397395, 396oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  +  ( 1  x.  T ) )  =  ( -u ( Z `  X )  +  T ) )
398224, 234negsubdid 9957 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u ( ( Z `
 X )  -  T )  =  (
-u ( Z `  X )  +  T
) )
399398eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( Z `
 X )  +  T )  =  -u ( ( Z `  X )  -  T
) )
400392, 397, 3993eqtrd 2512 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  -u (
( Z `  X
)  -  T ) )
401400oveq2d 6311 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) )  =  ( ( y  +  ( ( Z `  X
)  -  T ) )  +  -u (
( Z `  X
)  -  T ) ) )
402401adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  +  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T ) )  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  -u ( ( Z `  X )  -  T
) ) )
403337adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  RR )
404238, 403readdcld 9635 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
405404recnd 9634 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  CC )
406403recnd 9634 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  CC )
407405, 406negsubd 9948 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  +  -u ( ( Z `
 X )  -  T ) )  =  ( ( y  +  ( ( Z `  X )  -  T
) )  -  (
( Z `  X
)  -  T ) ) )
408244, 406pncand 9943 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  -  ( ( Z `
 X )  -  T ) )  =  y )
409402, 407, 4083eqtrrd 2513 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
410387, 389, 409syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
411410adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  y  =  ( ( y  +  ( ( Z `
 X )  -  T ) )  +  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
412364ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ph )
413382eqcomd 2475 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  1
)  =  ( Q `
 ( 0  +  1 ) ) )
414413oveq2d 6311 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  =  ( ( Q `  0 ) (,) ( Q `  ( 0  +  1 ) ) ) )
415372, 374oveq12d 6313 . . . . . . . . . . . . . . . . 17  |-  ( i  =  0  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 0 ) (,) ( Q `  (
0  +  1 ) ) ) )
416415sseq1d 3536 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D  <->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) )
417371, 416imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( 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
) ) )
418417, 250vtoclg 3176 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) )
419369, 418ax-mp 5 . . . . . . . . . . . . 13  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( ( Q `
 0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
)
420364, 368, 419syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  ( 0  +  1 ) ) )  C_  D )
421414, 420eqsstrd 3543 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  C_  D )
422421ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
( Q `  0
) (,) ( Q `
 1 ) ) 
C_  D )
42334, 42eqeltrd 2555 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
424423ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  e.  RR* )
425336rexrd 9655 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  1
)  e.  RR* )
426425ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  1 )  e.  RR* )
427389, 404syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
428427adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
y  +  ( ( Z `  X )  -  T ) )  e.  RR )
429358, 223, 224subaddd 9960 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( E `
 X )  -  X )  =  ( Z `  X )  <-> 
( X  +  ( Z `  X ) )  =  ( E `
 X ) ) )
430280, 429mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( E `  X )  -  X
)  =  ( Z `
 X ) )
431430eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( Z `  X
)  =  ( ( E `  X )  -  X ) )
432431adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Z `  X )  =  ( ( E `  X
)  -  X ) )
433 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( ( E `  X )  =  B  ->