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

Theorem fourierdlem41 37298
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 459 . . . . . 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 37259 . . . . . . . . . . . 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 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 457 . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
9 elmapi 7478 . . . . . . . . 9  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
10 ffn 5714 . . . . . . . . 9  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
118, 9, 103syl 18 . . . . . . . 8  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
1211adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  Q  Fn  ( 0 ... M
) )
13 fvelrnb 5896 . . . . . . 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 210 . . . . 5  |-  ( (
ph  /\  ( E `  X )  e.  ran  Q )  ->  E. j  e.  ( 0 ... M
) ( Q `  j )  =  ( E `  X ) )
16 0zd 10917 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  e.  ZZ )
17 elfzelz 11742 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
18173ad2ant2 1019 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  j  e.  ZZ )
19 1zzd 10936 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  1  e.  ZZ )
2018, 19zsubcld 11013 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ZZ )
21 simpll 752 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  ->  ph )
22 elfzle1 11743 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  0  <_  j )
2322anim1i 566 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  <_ 
j  /\  -.  0  <  j ) )
24 0red 9627 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  e.  RR )
2517zred 11008 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
2625adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  e.  RR )
2724, 26eqleltd 9761 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  ( 0  =  j  <->  ( 0  <_ 
j  /\  -.  0  <  j ) ) )
2823, 27mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  0  =  j )
2928eqcomd 2410 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ( 0 ... M )  /\  -.  0  <  j )  ->  j  =  0 )
3029adantll 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
j  =  0 )
31 fveq2 5849 . . . . . . . . . . . . . . . 16  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
327simprld 757 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
3332simpld 457 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  =  A )
3431, 33sylan9eqr 2465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  = 
0 )  ->  ( Q `  j )  =  A )
3521, 30, 34syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  0  <  j )  -> 
( Q `  j
)  =  A )
36353adantl3 1155 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =  A )
37 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR )
3938rexrd 9673 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  RR* )
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
4140rexrd 9673 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  RR* )
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  <  B )
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  =  ( B  -  A
)
44 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
4538, 40, 42, 43, 44fourierdlem4 37261 . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
4940adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
5049, 48resubcld 10028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
5140, 38resubcld 10028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( B  -  A
)  e.  RR )
5243, 51syl5eqel 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  T  e.  RR )
5352adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
54 0red 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  0  e.  RR )
5538, 40posdifd 10179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
5642, 55mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  0  <  ( B  -  A ) )
5743eqcomi 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( B  -  A )  =  T
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( B  -  A
)  =  T )
5956, 58breqtrd 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  0  <  T )
6054, 59gtned 9752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  T  =/=  0 )
6160adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
6250, 53, 61redivcld 10413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
6362flcld 11972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
6463zred 11008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
6564, 53remulcld 9654 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  RR  /\  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
)  e.  RR )  ->  ( Z `  x )  =  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
6848, 65, 67syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( Z `
 x )  =  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
6968oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( Z `  x ) )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
7069mpteq2dva 4481 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7147, 70eqtrd 2443 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
7271feq1d 5700 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( E : RR --> ( A (,] B )  <-> 
( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) : RR --> ( A (,] B ) ) )
7345, 72mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  E : RR --> ( A (,] B ) )
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  RR )
7573, 74ffvelrnd 6010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( E `  X
)  e.  ( A (,] B ) )
76 iocgtlb 36904 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 X )  e.  ( A (,] B
) )  ->  A  <  ( E `  X
) )
7739, 41, 75, 76syl3anc 1230 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  <  ( E `
 X ) )
7838, 77gtned 9752 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E `  X
)  =/=  A )
7978adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =/=  A
)
8037, 79eqnetrd 2696 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =/=  A
)
8180adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A
)
82813adantl2 1154 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  ( Q `  j )  =/=  A )
8382neneqd 2605 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  /\  -.  0  <  j )  ->  -.  ( Q `  j )  =  A )
8436, 83condan 795 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <  j )
85 zltlem1 10957 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  j  e.  ZZ )  ->  ( 0  <  j  <->  0  <_  ( j  - 
1 ) ) )
8616, 18, 85syl2anc 659 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  <  j  <->  0  <_  ( j  -  1 ) ) )
8784, 86mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  0  <_  ( j  -  1 ) )
88 eluz2 11133 . . . . . . . . . . 11  |-  ( ( j  -  1 )  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  ( j  -  1 )  e.  ZZ  /\  0  <_ 
( j  -  1 ) ) )
8916, 20, 87, 88syl3anbrc 1181 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( ZZ>= `  0 )
)
90 elfzel2 11740 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
91903ad2ant2 1019 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  M  e.  ZZ )
92 1red 9641 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  1  e.  RR )
9325, 92resubcld 10028 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  e.  RR )
9490zred 11008 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  M  e.  RR )
9525ltm1d 10518 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  j )
96 elfzle2 11744 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
9793, 25, 94, 95, 96ltletrd 9776 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <  M )
98973ad2ant2 1019 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  < 
M )
99 elfzo2 11862 . . . . . . . . . 10  |-  ( ( j  -  1 )  e.  ( 0..^ M )  <->  ( ( j  -  1 )  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  ( j  -  1 )  <  M ) )
10089, 91, 98, 99syl3anbrc 1181 . . . . . . . . 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 1018 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  Q :
( 0 ... M
) --> RR )
10316, 91, 203jca 1177 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  ( j  -  1 )  e.  ZZ ) )
10493, 94, 97ltled 9765 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  (
j  -  1 )  <_  M )
1051043ad2ant2 1019 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  <_  M )
106103, 87, 105jca32 533 . . . . . . . . . . . . 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 11733 . . . . . . . . . . . . 13  |-  ( ( j  -  1 )  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  (
j  -  1 )  e.  ZZ )  /\  ( 0  <_  (
j  -  1 )  /\  ( j  - 
1 )  <_  M
) ) )
108106, 107sylibr 212 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( j  -  1 )  e.  ( 0 ... M
) )
109102, 108ffvelrnd 6010 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR )
110109rexrd 9673 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  e.  RR* )
11125recnd 9652 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  j  e.  CC )
112 1cnd 9642 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  1  e.  CC )
113111, 112npcand 9971 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0 ... M )  ->  (
( j  -  1 )  +  1 )  =  j )
114113fveq2d 5853 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
115114adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  =  ( Q `  j ) )
116101ffvelrnda 6009 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR )
117116rexrd 9673 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  j )  e.  RR* )
118115, 117eqeltrd 2490 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( Q `  ( (
j  -  1 )  +  1 ) )  e.  RR* )
1191183adant3 1017 . . . . . . . . . 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 5849 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  ( Z `  x )  =  ( Z `  X ) )
122120, 121oveq12d 6296 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
123122adantl 464 . . . . . . . . . . . . . 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 6286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
126125oveq1d 6293 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
127126fveq2d 5853 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
128127oveq1d 6293 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
129128adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  =  X )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
13040, 74resubcld 10028 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  -  X
)  e.  RR )
131130, 52, 60redivcld 10413 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
132131flcld 11972 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
133132zred 11008 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
134133, 52remulcld 9654 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
135124, 129, 74, 134fvmptd 5938 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Z `  X
)  =  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
136135, 134eqeltrd 2490 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z `  X
)  e.  RR )
13774, 136readdcld 9653 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( Z `  X ) )  e.  RR )
13847, 123, 74, 137fvmptd 5938 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( Z `  X ) ) )
139138, 137eqeltrd 2490 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  X
)  e.  RR )
140139rexrd 9673 . . . . . . . . . . 11  |-  ( ph  ->  ( E `  X
)  e.  RR* )
1411403ad2ant1 1018 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  RR* )
142 simp1 997 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ph )
143 ovex 6306 . . . . . . . . . . . . . 14  |-  ( j  -  1 )  e. 
_V
144 eleq1 2474 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  (
i  e.  ( 0..^ M )  <->  ( j  -  1 )  e.  ( 0..^ M ) ) )
145144anbi2d 702 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  - 
1 )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  ( j  -  1 )  e.  ( 0..^ M ) ) ) )
146 fveq2 5849 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  i )  =  ( Q `  ( j  -  1 ) ) )
147 oveq1 6285 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  - 
1 )  ->  (
i  +  1 )  =  ( ( j  -  1 )  +  1 ) )
148147fveq2d 5853 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  - 
1 )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
149146, 148breq12d 4408 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) ) )
150145, 149imbi12d 318 . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
152151r19.21bi 2773 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
153143, 150, 152vtocl 3111 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( j  -  1 )  e.  ( 0..^ M ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
154142, 100, 153syl2anc 659 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  ( (
j  -  1 )  +  1 ) ) )
1551143ad2ant2 1019 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( ( j  - 
1 )  +  1 ) )  =  ( Q `  j ) )
156154, 155breqtrd 4419 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( Q `  j )
)
157 simp3 999 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( E `  X ) )
158156, 157breqtrd 4419 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  ( j  -  1 ) )  <  ( E `  X )
)
159139leidd 10159 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  X
)  <_  ( E `  X ) )
160159adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( E `  X )
)
16137eqcomd 2410 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  =  ( Q `  j ) )
162160, 161breqtrd 4419 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
1631623adant2 1016 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  j )
)
164113eqcomd 2410 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0 ... M )  ->  j  =  ( ( j  -  1 )  +  1 ) )
165164fveq2d 5853 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... M )  ->  ( Q `  j )  =  ( Q `  ( ( j  - 
1 )  +  1 ) ) )
1661653ad2ant2 1019 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( Q `  j )  =  ( Q `  ( ( j  -  1 )  +  1 ) ) )
167163, 166breqtrd 4419 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  <_  ( Q `  ( (
j  -  1 )  +  1 ) ) )
168110, 119, 141, 158, 167eliocd 36911 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) )
169146, 148oveq12d 6296 . . . . . . . . . . 11  |-  ( i  =  ( j  - 
1 )  ->  (
( Q `  i
) (,] ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 ( j  - 
1 ) ) (,] ( Q `  (
( j  -  1 )  +  1 ) ) ) )
170169eleq2d 2472 . . . . . . . . . 10  |-  ( i  =  ( j  - 
1 )  ->  (
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) )  <->  ( E `  X )  e.  ( ( Q `  (
j  -  1 ) ) (,] ( Q `
 ( ( j  -  1 )  +  1 ) ) ) ) )
171170rspcev 3160 . . . . . . . . 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 659 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
)  /\  ( Q `  j )  =  ( E `  X ) )  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
1731723exp 1196 . . . . . . 7  |-  ( ph  ->  ( j  e.  ( 0 ... M )  ->  ( ( Q `
 j )  =  ( E `  X
)  ->  E. i  e.  ( 0..^ M ) ( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) ) ) )
174173adantr 463 . . . . . 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 2894 . . . . 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 463 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  M  e.  NN )
178101adantr 463 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  Q : ( 0 ... M ) --> RR )
179 iocssicc 11666 . . . . . . . 8  |-  ( ( Q `  0 ) (,] ( Q `  M ) )  C_  ( ( Q ` 
0 ) [,] ( Q `  M )
)
18032simprd 461 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  =  B )
18133, 180oveq12d 6296 . . . . . . . . 9  |-  ( ph  ->  ( ( Q ` 
0 ) (,] ( Q `  M )
)  =  ( A (,] B ) )
18275, 181eleqtrrd 2493 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) (,] ( Q `  M ) ) )
183179, 182sseldi 3440 . . . . . . 7  |-  ( ph  ->  ( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
184183adantr 463 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  -> 
( E `  X
)  e.  ( ( Q `  0 ) [,] ( Q `  M ) ) )
185 simpr 459 . . . . . 6  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  -.  ( E `  X
)  e.  ran  Q
)
186 fveq2 5849 . . . . . . . . 9  |-  ( k  =  j  ->  ( Q `  k )  =  ( Q `  j ) )
187186breq1d 4405 . . . . . . . 8  |-  ( k  =  j  ->  (
( Q `  k
)  <  ( E `  X )  <->  ( Q `  j )  <  ( E `  X )
) )
188187cbvrabv 3058 . . . . . . 7  |-  { k  e.  ( 0..^ M )  |  ( Q `
 k )  < 
( E `  X
) }  =  {
j  e.  ( 0..^ M )  |  ( Q `  j )  <  ( E `  X ) }
189188supeq1i 7940 . . . . . 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 37282 . . . . 5  |-  ( (
ph  /\  -.  ( E `  X )  e.  ran  Q )  ->  E. i  e.  (
0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
191 ioossioc 36893 . . . . . . . 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 3441 . . . . . 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 2879 . . . . 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 792 . . 3  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )
197101adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
198 elfzofz 11874 . . . . . . . . . 10  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
199198adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
200197, 199ffvelrnd 6010 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
2012003adant3 1017 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
2021363ad2ant1 1018 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Z `  X
)  e.  RR )
203201, 202resubcld 10028 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  e.  RR )
2041393ad2ant1 1018 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  RR )
205201rexrd 9673 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR* )
206 fzofzp1 11946 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
207206adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
208197, 207ffvelrnd 6010 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
209208rexrd 9673 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
2102093adant3 1017 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
211 simp3 999 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  e.  ( ( Q `  i ) (,] ( Q `  ( i  +  1 ) ) ) )
212 iocgtlb 36904 . . . . . . . . 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 1230 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( E `  X ) )
214201, 204, 202, 213ltsub1dd 10204 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  ( ( E `  X )  -  ( Z `  X ) ) )
215138oveq1d 6293 . . . . . . . . 9  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  ( ( X  +  ( Z `
 X ) )  -  ( Z `  X ) ) )
21674recnd 9652 . . . . . . . . . 10  |-  ( ph  ->  X  e.  CC )
217136recnd 9652 . . . . . . . . . 10  |-  ( ph  ->  ( Z `  X
)  e.  CC )
218216, 217pncand 9968 . . . . . . . . 9  |-  ( ph  ->  ( ( X  +  ( Z `  X ) )  -  ( Z `
 X ) )  =  X )
219215, 218eqtrd 2443 . . . . . . . 8  |-  ( ph  ->  ( ( E `  X )  -  ( Z `  X )
)  =  X )
2202193ad2ant1 1018 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( E `  X )  -  ( Z `  X )
)  =  X )
221214, 220breqtrd 4419 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i )  -  ( Z `  X )
)  <  X )
222 elioore 11612 . . . . . . . . . . 11  |-  ( y  e.  ( ( ( Q `  i )  -  ( Z `  X ) ) (,) X )  ->  y  e.  RR )
223135oveq2d 6294 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  +  ( Z `  X ) )  =  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
224133recnd 9652 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  CC )
22552recnd 9652 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  CC )
226224, 225mulneg1d 10050 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )
227223, 226oveq12d 6296 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  =  ( ( y  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  +  -u (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
228227adantr 463 . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
230134adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  RR )
231229, 230readdcld 9653 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  RR )
232231recnd 9652 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  CC )
233230recnd 9652 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  e.  CC )
234232, 233negsubd 9973 . . . . . . . . . . . 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 9652 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
236235, 233pncand 9968 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  -  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  =  y )
237228, 234, 2363eqtrrd 2448 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
238222, 237sylan2 472 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  =  ( ( y  +  ( Z `  X
) )  +  (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
2392383ad2antl1 1159 . . . . . . . . 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 1000 . . . . . . . . . 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 1017 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
243242adantr 463 . . . . . . . . . . 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 463 . . . . . . . . . . . 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 463 . . . . . . . . . . . 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 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
247136adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
248246, 247readdcld 9653 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  e.  RR )
2492483ad2antl1 1159 . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Z `  X )  e.  RR )
251200, 250resubcld 10028 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR )
252251rexrd 9673 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  ( Z `  X ) )  e.  RR* )
253252adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  e. 
RR* )
25474rexrd 9673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  RR* )
255254ad2antrr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR* )
256 simpr 459 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )
257 ioogtlb 36897 . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( ( Q `  i )  -  ( Z `  X ) )  < 
y )
259200adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  e.  RR )
260136ad2antrr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Z `  X )  e.  RR )
261222adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  e.  RR )
262259, 260, 261ltsubaddd 10188 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  i )  <  (
y  +  ( Z `
 X ) ) )
2642633adantl3 1155 . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2672663adantl3 1155 . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  X  e.  RR )
269 iooltub 36916 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
)  e.  RR*  /\  X  e.  RR*  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
270253, 255, 256, 269syl3anc 1230 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  y  <  X )
271261, 268, 260, 270ltadd1dd 10203 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( X  +  ( Z `  X ) ) )
272138eqcomd 2410 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  +  ( Z `  X ) )  =  ( E `
 X ) )
273272ad2antrr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( X  +  ( Z `  X ) )  =  ( E `  X
) )
274271, 273breqtrd 4419 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) )  ->  ( y  +  ( Z `  X ) )  < 
( E `  X
) )
2752743adantl3 1155 . . . . . . . . . . . . 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 36905 . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( E `  X
)  <_  ( Q `  ( i  +  1 ) ) )
278277adantr 463 . . . . . . . . . . . . 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 9776 . . . . . . . . . . . 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 36900 . . . . . . . . . . 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 3443 . . . . . . . . . 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 11972 . . . . . . . . . . 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 11010 . . . . . . . . . 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 9854 . . . . . . . . . . 11  |-  -u ( |_ `  ( ( B  -  X )  /  T ) )  e. 
_V
286 eleq1 2474 . . . . . . . . . . . . 13  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  e.  ZZ  <->  -u ( |_
`  ( ( B  -  X )  /  T ) )  e.  ZZ ) )
2872863anbi3d 1307 . . . . . . . . . . . 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 6285 . . . . . . . . . . . . . 14  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
289288oveq2d 6294 . . . . . . . . . . . . 13  |-  ( k  =  -u ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
290289eleq1d 2471 . . . . . . . . . . . 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 318 . . . . . . . . . . 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 6306 . . . . . . . . . . . 12  |-  ( y  +  ( Z `  X ) )  e. 
_V
293 eleq1 2474 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  e.  D  <->  ( y  +  ( Z `  X ) )  e.  D ) )
2942933anbi2d 1306 . . . . . . . . . . . . 13  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( ph  /\  x  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )
) )
295 oveq1 6285 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
x  +  ( k  x.  T ) )  =  ( ( y  +  ( Z `  X ) )  +  ( k  x.  T
) ) )
296295eleq1d 2471 . . . . . . . . . . . . 13  |-  ( x  =  ( y  +  ( Z `  X
) )  ->  (
( x  +  ( k  x.  T ) )  e.  D  <->  ( (
y  +  ( Z `
 X ) )  +  ( k  x.  T ) )  e.  D ) )
297294, 296imbi12d 318 . . . . . . . . . . . 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 3111 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  +  ( Z `  X ) )  e.  D  /\  k  e.  ZZ )  ->  (
( y  +  ( Z `  X ) )  +  ( k  x.  T ) )  e.  D )
300285, 291, 299vtocl 3111 . . . . . . . . . 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 1230 . . . . . . . . 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 2490 . . . . . . . 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 2818 . . . . . . 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 3432 . . . . . . 7  |-  ( ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) 
C_  D  <->  A. y  e.  ( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) y  e.  D )
305303, 304sylibr 212 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M )  /\  ( E `  X )  e.  ( ( Q `
 i ) (,] ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( Q `
 i )  -  ( Z `  X ) ) (,) X ) 
C_  D )
306 breq1 4398 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y  <  X  <->  ( ( Q `
 i )  -  ( Z `  X ) )  <  X ) )
307 oveq1 6285 . . . . . . . . 9  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( y (,) X )  =  ( ( ( Q `  i )  -  ( Z `  X )
) (,) X ) )
308307sseq1d 3469 . . . . . . . 8  |-  ( y  =  ( ( Q `
 i )  -  ( Z `  X ) )  ->  ( (
y (,) X ) 
C_  D  <->  ( (
( Q `  i
)  -  ( Z `
 X ) ) (,) X )  C_  D ) )
309306, 308anbi12d 709 . . . . . . 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 3160 . . . . . 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 1228 . . . . 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 1196 . . . 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 2894 . . 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 10917 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
3163nnzd 11007 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
317 1zzd 10936 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ZZ )
318315, 316, 3173jca 1177 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )
)
319 0le1 10116 . . . . . . . . . 10  |-  0  <_  1
320319a1i 11 . . . . . . . . 9  |-  ( ph  ->  0  <_  1 )
3213nnge1d 10619 . . . . . . . . 9  |-  ( ph  ->  1  <_  M )
322318, 320, 321jca32 533 . . . . . . . 8  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
323 elfz2 11733 . . . . . . . 8  |-  ( 1  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
324322, 323sylibr 212 . . . . . . 7  |-  ( ph  ->  1  e.  ( 0 ... M ) )
325101, 324ffvelrnd 6010 . . . . . 6  |-  ( ph  ->  ( Q `  1
)  e.  RR )
326136, 52resubcld 10028 . . . . . 6  |-  ( ph  ->  ( ( Z `  X )  -  T
)  e.  RR )
327325, 326resubcld 10028 . . . . 5  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR )
328327adantr 463 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e.  RR )
32938recnd 9652 . . . . . . . . . 10  |-  ( ph  ->  A  e.  CC )
330329, 225pncand 9968 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
331330adantr 463 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( A  +  T )  -  T )  =  A )
33243oveq2i 6289 . . . . . . . . . . 11  |-  ( A  +  T )  =  ( A  +  ( B  -  A ) )
333332a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  T )  =  ( A  +  ( B  -  A ) ) )
33440recnd 9652 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
335329, 334pncan3d 9970 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  ( B  -  A ) )  =  B )
336335adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( A  +  ( B  -  A ) )  =  B )
337 id 22 . . . . . . . . . . . 12  |-  ( ( E `  X )  =  B  ->  ( E `  X )  =  B )
338337eqcomd 2410 . . . . . . . . . . 11  |-  ( ( E `  X )  =  B  ->  B  =  ( E `  X ) )
339338adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  B  =  ( E `  X ) )
340333, 336, 3393eqtrrd 2448 . . . . . . . . 9  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( E `  X )  =  ( A  +  T ) )
341340oveq1d 6293 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( ( A  +  T
)  -  T ) )
34233adantr 463 . . . . . . . 8  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  A )
343331, 341, 3423eqtr4rd 2454 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( ( E `  X )  -  T
) )
344343oveq1d 6293 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  =  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) ) )
345139recnd 9652 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  CC )
346345, 217, 225nnncan2d 10002 . . . . . . 7  |-  ( ph  ->  ( ( ( E `
 X )  -  T )  -  (
( Z `  X
)  -  T ) )  =  ( ( E `  X )  -  ( Z `  X ) ) )
347346adantr 463 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( (
( E `  X
)  -  T )  -  ( ( Z `
 X )  -  T ) )  =  ( ( E `  X )  -  ( Z `  X )
) )
348219adantr 463 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  ( Z `  X ) )  =  X )
349344, 347, 3483eqtrrd 2448 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  =  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) ) )
35033, 38eqeltrd 2490 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  e.  RR )
3513nngt0d 10620 . . . . . . . . . 10  |-  ( ph  ->  0  <  M )
352 fzolb 11865 . . . . . . . . . 10  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
353315, 316, 351, 352syl3anbrc 1181 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0..^ M ) )
354 0re 9626 . . . . . . . . . 10  |-  0  e.  RR
355 eleq1 2474 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
356355anbi2d 702 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
357 fveq2 5849 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
358 oveq1 6285 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
359358fveq2d 5853 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
360357, 359breq12d 4408 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
361356, 360imbi12d 318 . . . . . . . . . . 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 3117 . . . . . . . . . 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 666 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
365 0p1e1 10688 . . . . . . . . . 10  |-  ( 0  +  1 )  =  1
366365fveq2i 5852 . . . . . . . . 9  |-  ( Q `
 ( 0  +  1 ) )  =  ( Q `  1
)
367366a1i 11 . . . . . . . 8  |-  ( ph  ->  ( Q `  (
0  +  1 ) )  =  ( Q `
 1 ) )
368364, 367breqtrd 4419 . . . . . . 7  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
369350, 325, 326, 368ltsub1dd 10204 . . . . . 6  |-  ( ph  ->  ( ( Q ` 
0 )  -  (
( Z `  X
)  -  T ) )  <  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) )
370369adantr 463 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Q `  0 )  -  ( ( Z `
 X )  -  T ) )  < 
( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )
371349, 370eqbrtrd 4415 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  X  <  ( ( Q `  1
)  -  ( ( Z `  X )  -  T ) ) )
372 elioore 11612 . . . . . . . . 9  |-  ( y  e.  ( X (,) ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) ) )  ->  y  e.  RR )
373135eqcomd 2410 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  =  ( Z `
 X ) )
374373negeqd 9850 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
375226, 374eqtrd 2443 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  =  -u ( Z `  X ) )
376225mulid2d 9644 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  x.  T
)  =  T )
377375, 376oveq12d 6296 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  +  ( 1  x.  T ) )  =  ( -u ( Z `  X )  +  T ) )
378224negcld 9954 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u ( |_ `  ( ( B  -  X )  /  T
) )  e.  CC )
379 1cnd 9642 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  CC )
380378, 379, 225adddird 9651 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  ( (
-u ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  +  ( 1  x.  T ) ) )
381217, 225negsubdid 9982 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( Z `
 X )  -  T )  =  (
-u ( Z `  X )  +  T
) )
382377, 380, 3813eqtr4d 2453 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u ( |_ `  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
)  =  -u (
( Z `  X
)  -  T ) )
383382oveq2d 6294 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) )  =  ( ( y  +  ( ( Z `  X
)  -  T ) )  +  -u (
( Z `  X
)  -  T ) ) )
384383adantr 463 . . . . . . . . . 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 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  RR )
386229, 385readdcld 9653 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
387386recnd 9652 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  CC )
388385recnd 9652 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( Z `  X )  -  T )  e.  CC )
389387, 388negsubd 9973 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  +  -u ( ( Z `
 X )  -  T ) )  =  ( ( y  +  ( ( Z `  X )  -  T
) )  -  (
( Z `  X
)  -  T ) ) )
390235, 388pncand 9968 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  +  ( ( Z `  X )  -  T ) )  -  ( ( Z `
 X )  -  T ) )  =  y )
391384, 389, 3903eqtrrd 2448 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
392372, 391sylan2 472 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  =  ( ( y  +  ( ( Z `  X )  -  T
) )  +  ( ( -u ( |_
`  ( ( B  -  X )  /  T ) )  +  1 )  x.  T
) ) )
393392adantlr 713 . . . . . . 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 752 . . . . . . . 8  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ph )
395367eqcomd 2410 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  1
)  =  ( Q `
 ( 0  +  1 ) ) )
396395oveq2d 6294 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  =  ( ( Q `  0 ) (,) ( Q `  ( 0  +  1 ) ) ) )
397357, 359oveq12d 6296 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 0 ) (,) ( Q `  (
0  +  1 ) ) ) )
398397sseq1d 3469 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D  <->  ( ( Q `  0 ) (,) ( Q `  (
0  +  1 ) ) )  C_  D
) )
399356, 398imbi12d 318 . . . . . . . . . . . . . 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 3117 . . . . . . . . . . . . 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 666 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  ( 0  +  1 ) ) )  C_  D )
403396, 402eqsstrd 3476 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q ` 
0 ) (,) ( Q `  1 )
)  C_  D )
404403ad2antrr 724 . . . . . . . . 9  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
( Q `  0
) (,) ( Q `
 1 ) ) 
C_  D )
40533, 39eqeltrd 2490 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
406405ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  e.  RR* )
407325rexrd 9673 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  1
)  e.  RR* )
408407ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  1 )  e.  RR* )
409372, 386sylan2 472 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( y  +  ( ( Z `
 X )  -  T ) )  e.  RR )
410409adantlr 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  (
y  +  ( ( Z `  X )  -  T ) )  e.  RR )
411345, 216, 217subaddd 9985 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( E `
 X )  -  X )  =  ( Z `  X )  <-> 
( X  +  ( Z `  X ) )  =  ( E `
 X ) ) )
412272, 411mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( E `  X )  -  X
)  =  ( Z `
 X ) )
413 oveq1 6285 . . . . . . . . . . . . . . . 16  |-  ( ( E `  X )  =  B  ->  (
( E `  X
)  -  X )  =  ( B  -  X ) )
414412, 413sylan9req 2464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Z `  X )  =  ( B  -  X ) )
415414oveq1d 6293 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( Z `  X )  -  T )  =  ( ( B  -  X
)  -  T ) )
416415oveq2d 6294 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( X  +  ( ( Z `
 X )  -  T ) )  =  ( X  +  ( ( B  -  X
)  -  T ) ) )
417130recnd 9652 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  -  X
)  e.  CC )
418216, 417, 225addsubassd 9987 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( X  +  ( ( B  -  X )  -  T ) ) )
419418eqcomd 2410 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  +  ( ( B  -  X
)  -  T ) )  =  ( ( X  +  ( B  -  X ) )  -  T ) )
420419adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( X  +  ( ( B  -  X )  -  T ) )  =  ( ( X  +  ( B  -  X
) )  -  T
) )
421334, 225, 329subsub23d 36847 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  -  T )  =  A  <-> 
( B  -  A
)  =  T ) )
42258, 421mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  -  T
)  =  A )
423216, 334pncan3d 9970 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  +  ( B  -  X ) )  =  B )
424423oveq1d 6293 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( B  -  T ) )
425422, 424, 333eqtr4d 2453 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( X  +  ( B  -  X
) )  -  T
)  =  ( Q `
 0 ) )
426425adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( X  +  ( B  -  X ) )  -  T )  =  ( Q `  0 ) )
427416, 420, 4263eqtrrd 2448 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( Q `  0 )  =  ( X  +  ( ( Z `  X
)  -  T ) ) )
428427adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( E `  X )  =  B )  /\  y  e.  ( X (,) (
( Q `  1
)  -  ( ( Z `  X )  -  T ) ) ) )  ->  ( Q `  0 )  =  ( X  +  ( ( Z `  X )  -  T
) ) )
42974adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  X  e.  RR )
430372adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  y  e.  RR )
431326adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( ( Z `  X )  -  T )  e.  RR )
432254adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  X  e.  RR* )
433327rexrd 9673 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q ` 
1 )  -  (
( Z `  X
)  -  T ) )  e.  RR* )
434433adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) ) ) )  ->  ( ( Q `  1 )  -  ( ( Z `
 X )  -  T ) )  e. 
RR* )
435 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( X (,) ( ( Q `  1 )  -  ( ( Z