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

Theorem fourierdlem63 32194
Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem63.t  |-  T  =  ( B  -  A
)
fourierdlem63.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 ) ) ) } )
fourierdlem63.m  |-  ( ph  ->  M  e.  NN )
fourierdlem63.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem63.c  |-  ( ph  ->  C  e.  RR )
fourierdlem63.d  |-  ( ph  ->  D  e.  RR )
fourierdlem63.cltd  |-  ( ph  ->  C  <  D )
fourierdlem63.o  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  C  /\  ( p `
 m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem63.h  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
fourierdlem63.n  |-  N  =  ( ( # `  H
)  -  1 )
fourierdlem63.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
fourierdlem63.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem63.k  |-  ( ph  ->  K  e.  ( 0 ... M ) )
fourierdlem63.j  |-  ( ph  ->  J  e.  ( 0..^ N ) )
fourierdlem63.y  |-  ( ph  ->  Y  e.  ( ( S `  J ) [,) ( S `  ( J  +  1
) ) ) )
fourierdlem63.eyltqk  |-  ( ph  ->  ( E `  Y
)  <  ( Q `  K ) )
fourierdlem63.x  |-  X  =  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )
Assertion
Ref Expression
fourierdlem63  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  <_  ( Q `  K ) )
Distinct variable groups:    A, i, m, p    x, A, i    B, i, m, p    x, B    C, i, m, p   
x, C    D, i, m, p    x, D    k, E, x    f, H    x, H    k, J, x    k, K, x    i, M, m, p    f, N    i, N, m, p    x, N    Q, i, k, x    Q, p    S, f    S, i, k, x    S, p    T, i, k, x    k, Y, x    ph, f    ph, i,
k, x
Allowed substitution hints:    ph( m, p)    A( f, k)    B( f, k)    C( f, k)    D( f, k)    P( x, f, i, k, m, p)    Q( f, m)    S( m)    T( f, m, p)    E( f, i, m, p)    H( i, k, m, p)    J( f, i, m, p)    K( f, i, m, p)    M( x, f, k)    N( k)    O( x, f, i, k, m, p)    X( x, f, i, k, m, p)    Y( f, i, m, p)

Proof of Theorem fourierdlem63
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 fourierdlem63.e . . . . 5  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
21a1i 11 . . . 4  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
3 id 22 . . . . . 6  |-  ( x  =  ( S `  ( J  +  1
) )  ->  x  =  ( S `  ( J  +  1
) ) )
4 oveq2 6278 . . . . . . . . 9  |-  ( x  =  ( S `  ( J  +  1
) )  ->  ( B  -  x )  =  ( B  -  ( S `  ( J  +  1 ) ) ) )
54oveq1d 6285 . . . . . . . 8  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )
65fveq2d 5852 . . . . . . 7  |-  ( x  =  ( S `  ( J  +  1
) )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) ) )
76oveq1d 6285 . . . . . 6  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) )
83, 7oveq12d 6288 . . . . 5  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 ( J  + 
1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) ) )
98adantl 464 . . . 4  |-  ( (
ph  /\  x  =  ( S `  ( J  +  1 ) ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `  ( J  +  1
) )  +  ( ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) ) )
10 fourierdlem63.t . . . . . . . . . . 11  |-  T  =  ( B  -  A
)
11 fourierdlem63.p . . . . . . . . . . 11  |-  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 ) ) ) } )
12 fourierdlem63.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
13 fourierdlem63.q . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
14 fourierdlem63.c . . . . . . . . . . 11  |-  ( ph  ->  C  e.  RR )
15 fourierdlem63.d . . . . . . . . . . 11  |-  ( ph  ->  D  e.  RR )
16 fourierdlem63.cltd . . . . . . . . . . 11  |-  ( ph  ->  C  <  D )
17 fourierdlem63.o . . . . . . . . . . 11  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  C  /\  ( p `
 m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
18 fourierdlem63.h . . . . . . . . . . 11  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
19 fourierdlem63.n . . . . . . . . . . 11  |-  N  =  ( ( # `  H
)  -  1 )
20 fourierdlem63.s . . . . . . . . . . 11  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
2110, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20fourierdlem54 32185 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  e.  NN  /\  S  e.  ( O `  N
) )  /\  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) ) )
2221simpld 457 . . . . . . . . 9  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
2322simprd 461 . . . . . . . 8  |-  ( ph  ->  S  e.  ( O `
 N ) )
2422simpld 457 . . . . . . . . 9  |-  ( ph  ->  N  e.  NN )
2517fourierdlem2 32133 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( S  e.  ( O `  N )  <->  ( S  e.  ( RR  ^m  (
0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) ) )
2624, 25syl 16 . . . . . . . 8  |-  ( ph  ->  ( S  e.  ( O `  N )  <-> 
( S  e.  ( RR  ^m  ( 0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) ) )
2723, 26mpbid 210 . . . . . . 7  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) )
2827simpld 457 . . . . . 6  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... N ) ) )
29 elmapi 7433 . . . . . 6  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
3028, 29syl 16 . . . . 5  |-  ( ph  ->  S : ( 0 ... N ) --> RR )
31 fourierdlem63.j . . . . . 6  |-  ( ph  ->  J  e.  ( 0..^ N ) )
32 fzofzp1 11890 . . . . . 6  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
3331, 32syl 16 . . . . 5  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
3430, 33ffvelrnd 6008 . . . 4  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR )
3511, 12, 13fourierdlem11 32142 . . . . . . . . . . 11  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
3635simp2d 1007 . . . . . . . . . 10  |-  ( ph  ->  B  e.  RR )
3736, 34resubcld 9983 . . . . . . . . 9  |-  ( ph  ->  ( B  -  ( S `  ( J  +  1 ) ) )  e.  RR )
3835simp1d 1006 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
3936, 38resubcld 9983 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
4010, 39syl5eqel 2546 . . . . . . . . 9  |-  ( ph  ->  T  e.  RR )
4135simp3d 1008 . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
4238, 36posdifd 10135 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
4341, 42mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
4443, 10syl6breqr 4479 . . . . . . . . . 10  |-  ( ph  ->  0  <  T )
4544gt0ne0d 10113 . . . . . . . . 9  |-  ( ph  ->  T  =/=  0 )
4637, 40, 45redivcld 10368 . . . . . . . 8  |-  ( ph  ->  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T )  e.  RR )
4746flcld 11916 . . . . . . 7  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  ZZ )
4847zred 10965 . . . . . 6  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  RR )
4948, 40remulcld 9613 . . . . 5  |-  ( ph  ->  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T )  e.  RR )
5034, 49readdcld 9612 . . . 4  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  +  ( ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) )  e.  RR )
512, 9, 34, 50fvmptd 5936 . . 3  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  =  ( ( S `  ( J  +  1 ) )  +  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) ) )
5251, 50eqeltrd 2542 . 2  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  RR )
5311fourierdlem2 32133 . . . . . . 7  |-  ( 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 ) ) ) ) ) )
5412, 53syl 16 . . . . . 6  |-  ( 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 ) ) ) ) ) )
5513, 54mpbid 210 . . . . 5  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
5655simpld 457 . . . 4  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
57 elmapi 7433 . . . 4  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
5856, 57syl 16 . . 3  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
59 fourierdlem63.k . . 3  |-  ( ph  ->  K  e.  ( 0 ... M ) )
6058, 59ffvelrnd 6008 . 2  |-  ( ph  ->  ( Q `  K
)  e.  RR )
6114adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  C  e.  RR )
6215adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  D  e.  RR )
6338rexrd 9632 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  RR* )
64 iocssre 11607 . . . . . . . . . . . 12  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
6563, 36, 64syl2anc 659 . . . . . . . . . . 11  |-  ( ph  ->  ( A (,] B
)  C_  RR )
6638, 36, 41, 10, 1fourierdlem4 32135 . . . . . . . . . . . 12  |-  ( ph  ->  E : RR --> ( A (,] B ) )
67 fourierdlem63.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  ( ( S `  J ) [,) ( S `  ( J  +  1
) ) ) )
68 elfzofz 11819 . . . . . . . . . . . . . . . . 17  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
6931, 68syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  J  e.  ( 0 ... N ) )
7030, 69ffvelrnd 6008 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S `  J
)  e.  RR )
7134rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR* )
72 elico2 11591 . . . . . . . . . . . . . . 15  |-  ( ( ( S `  J
)  e.  RR  /\  ( S `  ( J  +  1 ) )  e.  RR* )  ->  ( Y  e.  ( ( S `  J ) [,) ( S `  ( J  +  1 ) ) )  <->  ( Y  e.  RR  /\  ( S `
 J )  <_  Y  /\  Y  <  ( S `  ( J  +  1 ) ) ) ) )
7370, 71, 72syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y  e.  ( ( S `  J
) [,) ( S `
 ( J  + 
1 ) ) )  <-> 
( Y  e.  RR  /\  ( S `  J
)  <_  Y  /\  Y  <  ( S `  ( J  +  1
) ) ) ) )
7467, 73mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y  e.  RR  /\  ( S `  J
)  <_  Y  /\  Y  <  ( S `  ( J  +  1
) ) ) )
7574simp1d 1006 . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  RR )
7666, 75ffvelrnd 6008 . . . . . . . . . . 11  |-  ( ph  ->  ( E `  Y
)  e.  ( A (,] B ) )
7765, 76sseldd 3490 . . . . . . . . . 10  |-  ( ph  ->  ( E `  Y
)  e.  RR )
7877, 75resubcld 9983 . . . . . . . . 9  |-  ( ph  ->  ( ( E `  Y )  -  Y
)  e.  RR )
7960, 78resubcld 9983 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  e.  RR )
8079adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  RR )
81 icossicc 11614 . . . . . . . . . . . . . 14  |-  ( ( S `  J ) [,) ( S `  ( J  +  1
) ) )  C_  ( ( S `  J ) [,] ( S `  ( J  +  1 ) ) )
8214rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR* )
8315rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( ph  ->  D  e.  RR* )
8417, 24, 23fourierdlem15 32146 . . . . . . . . . . . . . . 15  |-  ( ph  ->  S : ( 0 ... N ) --> ( C [,] D ) )
8582, 83, 84, 31fourierdlem8 32139 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( S `  J ) [,] ( S `  ( J  +  1 ) ) )  C_  ( C [,] D ) )
8681, 85syl5ss 3500 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S `  J ) [,) ( S `  ( J  +  1 ) ) )  C_  ( C [,] D ) )
8786, 67sseldd 3490 . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  ( C [,] D ) )
88 elicc2 11592 . . . . . . . . . . . . 13  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( Y  e.  ( C [,] D )  <-> 
( Y  e.  RR  /\  C  <_  Y  /\  Y  <_  D ) ) )
8914, 15, 88syl2anc 659 . . . . . . . . . . . 12  |-  ( ph  ->  ( Y  e.  ( C [,] D )  <-> 
( Y  e.  RR  /\  C  <_  Y  /\  Y  <_  D ) ) )
9087, 89mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  ( Y  e.  RR  /\  C  <_  Y  /\  Y  <_  D ) )
9190simp2d 1007 . . . . . . . . . 10  |-  ( ph  ->  C  <_  Y )
9260, 77resubcld 9983 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  K )  -  ( E `  Y )
)  e.  RR )
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  Y
)  <  ( Q `  K ) )
9477, 60posdifd 10135 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E `  Y )  <  ( Q `  K )  <->  0  <  ( ( Q `
 K )  -  ( E `  Y ) ) ) )
9593, 94mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( ( Q `  K )  -  ( E `  Y ) ) )
9692, 95elrpd 11256 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q `  K )  -  ( E `  Y )
)  e.  RR+ )
9775, 96ltaddrpd 11288 . . . . . . . . . . 11  |-  ( ph  ->  Y  <  ( Y  +  ( ( Q `
 K )  -  ( E `  Y ) ) ) )
9860recnd 9611 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  K
)  e.  CC )
9977recnd 9611 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  Y
)  e.  CC )
10075recnd 9611 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  CC )
10198, 99, 100subsub3d 9952 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  =  ( ( ( Q `  K
)  +  Y )  -  ( E `  Y ) ) )
10298, 100addcomd 9771 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  K )  +  Y
)  =  ( Y  +  ( Q `  K ) ) )
103102oveq1d 6285 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( Q `
 K )  +  Y )  -  ( E `  Y )
)  =  ( ( Y  +  ( Q `
 K ) )  -  ( E `  Y ) ) )
104100, 98, 99addsubassd 9942 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Y  +  ( Q `  K ) )  -  ( E `
 Y ) )  =  ( Y  +  ( ( Q `  K )  -  ( E `  Y )
) ) )
105101, 103, 1043eqtrrd 2500 . . . . . . . . . . 11  |-  ( ph  ->  ( Y  +  ( ( Q `  K
)  -  ( E `
 Y ) ) )  =  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
10697, 105breqtrd 4463 . . . . . . . . . 10  |-  ( ph  ->  Y  <  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
10714, 75, 79, 91, 106lelttrd 9729 . . . . . . . . 9  |-  ( ph  ->  C  <  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
10814, 79, 107ltled 9722 . . . . . . . 8  |-  ( ph  ->  C  <_  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
109108adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  C  <_  (
( Q `  K
)  -  ( ( E `  Y )  -  Y ) ) )
11034adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( S `  ( J  +  1
) )  e.  RR )
11160adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( Q `  K )  e.  RR )
11252, 34resubcld 9983 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  e.  RR )
113112adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  e.  RR )
114111, 113resubcld 9983 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) )  e.  RR )
11574simp3d 1008 . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  <  ( S `
 ( J  + 
1 ) ) )
11675, 34, 115ltled 9722 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  <_  ( S `  ( J  +  1 ) ) )
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 32138 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  <_  ( ( E `
 Y )  -  Y ) )
118112, 78, 60, 117lesub2dd 10165 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  <_  ( ( Q `  K )  -  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) ) ) )
119118adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <_  (
( Q `  K
)  -  ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( S `  ( J  +  1
) ) ) ) )
12098adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( Q `  K )  e.  CC )
12152recnd 9611 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  CC )
122121adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  CC )
123110recnd 9611 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( S `  ( J  +  1
) )  e.  CC )
124120, 122, 123subsubd 9950 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) )  =  ( ( ( Q `  K
)  -  ( E `
 ( S `  ( J  +  1
) ) ) )  +  ( S `  ( J  +  1
) ) ) )
12598, 121subcld 9922 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  e.  CC )
12634recnd 9611 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  CC )
127125, 126addcomd 9771 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  +  ( S `
 ( J  + 
1 ) ) )  =  ( ( S `
 ( J  + 
1 ) )  +  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) ) )
128127adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  +  ( S `  ( J  +  1 ) ) )  =  ( ( S `  ( J  +  1 ) )  +  ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) ) ) )
129124, 128eqtrd 2495 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) )  =  ( ( S `  ( J  +  1 ) )  +  ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) ) ) )
130 simpr 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )
13152adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  RR )
132111, 131sublt0d 31737 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  <  0  <->  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) ) )
133130, 132mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  <  0 )
134111, 131resubcld 9983 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  e.  RR )
135 ltaddneg 31727 . . . . . . . . . . . . 13  |-  ( ( ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  e.  RR  /\  ( S `  ( J  +  1 ) )  e.  RR )  -> 
( ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  <  0  <->  (
( S `  ( J  +  1 ) )  +  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )  < 
( S `  ( J  +  1 ) ) ) )
136134, 110, 135syl2anc 659 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  <  0  <->  ( ( S `  ( J  +  1 ) )  +  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )  < 
( S `  ( J  +  1 ) ) ) )
137133, 136mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( S `
 ( J  + 
1 ) )  +  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )  <  ( S `
 ( J  + 
1 ) ) )
138129, 137eqbrtrd 4459 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) )  <  ( S `
 ( J  + 
1 ) ) )
13980, 114, 110, 119, 138lelttrd 9729 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <  ( S `  ( J  +  1 ) ) )
14084, 33ffvelrnd 6008 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  ( C [,] D ) )
141 elicc2 11592 . . . . . . . . . . . . 13  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( S `  ( J  +  1
) )  e.  ( C [,] D )  <-> 
( ( S `  ( J  +  1
) )  e.  RR  /\  C  <_  ( S `  ( J  +  1 ) )  /\  ( S `  ( J  +  1 ) )  <_  D ) ) )
14214, 15, 141syl2anc 659 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  e.  ( C [,] D )  <-> 
( ( S `  ( J  +  1
) )  e.  RR  /\  C  <_  ( S `  ( J  +  1 ) )  /\  ( S `  ( J  +  1 ) )  <_  D ) ) )
143140, 142mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  e.  RR  /\  C  <_  ( S `  ( J  +  1 ) )  /\  ( S `  ( J  +  1 ) )  <_  D ) )
144143simp3d 1008 . . . . . . . . . 10  |-  ( ph  ->  ( S `  ( J  +  1 ) )  <_  D )
145144adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( S `  ( J  +  1
) )  <_  D
)
14680, 110, 62, 139, 145ltletrd 9731 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <  D
)
14780, 62, 146ltled 9722 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <_  D
)
14861, 62, 80, 109, 147eliccd 31780 . . . . . 6  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  ( C [,] D ) )
149 id 22 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  x  =  Y )
150 oveq2 6278 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  Y  ->  ( B  -  x )  =  ( B  -  Y ) )
151150oveq1d 6285 . . . . . . . . . . . . . . . . 17  |-  ( x  =  Y  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  Y )  /  T ) )
152151fveq2d 5852 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  Y
)  /  T ) ) )
153152oveq1d 6285 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T ) )
154149, 153oveq12d 6288 . . . . . . . . . . . . . 14  |-  ( x  =  Y  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
) ) )
155154adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  =  Y )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
) ) )
15636, 75resubcld 9983 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B  -  Y
)  e.  RR )
157156, 40, 45redivcld 10368 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( B  -  Y )  /  T
)  e.  RR )
158157flcld 11916 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( |_ `  (
( B  -  Y
)  /  T ) )  e.  ZZ )
159158zred 10965 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
( B  -  Y
)  /  T ) )  e.  RR )
160159, 40remulcld 9613 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
)  e.  RR )
16175, 160readdcld 9612 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y  +  ( ( |_ `  (
( B  -  Y
)  /  T ) )  x.  T ) )  e.  RR )
1622, 155, 75, 161fvmptd 5936 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  Y
)  =  ( Y  +  ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T ) ) )
163162oveq1d 6285 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E `  Y )  -  Y
)  =  ( ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T ) )  x.  T ) )  -  Y ) )
164163oveq1d 6285 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( E `
 Y )  -  Y )  /  T
)  =  ( ( ( Y  +  ( ( |_ `  (
( B  -  Y
)  /  T ) )  x.  T ) )  -  Y )  /  T ) )
165160recnd 9611 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
)  e.  CC )
166100, 165pncan2d 9924 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
) )  -  Y
)  =  ( ( |_ `  ( ( B  -  Y )  /  T ) )  x.  T ) )
167166oveq1d 6285 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( Y  +  ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T ) )  -  Y )  /  T
)  =  ( ( ( |_ `  (
( B  -  Y
)  /  T ) )  x.  T )  /  T ) )
168159recnd 9611 . . . . . . . . . . 11  |-  ( ph  ->  ( |_ `  (
( B  -  Y
)  /  T ) )  e.  CC )
16940recnd 9611 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  CC )
170168, 169, 45divcan4d 10322 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T )  /  T
)  =  ( |_
`  ( ( B  -  Y )  /  T ) ) )
171164, 167, 1703eqtrd 2499 . . . . . . . . 9  |-  ( ph  ->  ( ( ( E `
 Y )  -  Y )  /  T
)  =  ( |_
`  ( ( B  -  Y )  /  T ) ) )
172171, 158eqeltrd 2542 . . . . . . . 8  |-  ( ph  ->  ( ( ( E `
 Y )  -  Y )  /  T
)  e.  ZZ )
17378recnd 9611 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E `  Y )  -  Y
)  e.  CC )
174173, 169, 45divcan1d 10317 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( E `  Y )  -  Y )  /  T )  x.  T
)  =  ( ( E `  Y )  -  Y ) )
175174oveq2d 6286 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  =  ( ( ( Q `  K
)  -  ( ( E `  Y )  -  Y ) )  +  ( ( E `
 Y )  -  Y ) ) )
17698, 173npcand 9926 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( E `  Y
)  -  Y ) )  =  ( Q `
 K ) )
177175, 176eqtrd 2495 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  =  ( Q `
 K ) )
178 ffun 5715 . . . . . . . . . . 11  |-  ( Q : ( 0 ... M ) --> RR  ->  Fun 
Q )
17958, 178syl 16 . . . . . . . . . 10  |-  ( ph  ->  Fun  Q )
180 fdm 5717 . . . . . . . . . . . 12  |-  ( Q : ( 0 ... M ) --> RR  ->  dom 
Q  =  ( 0 ... M ) )
18158, 180syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  Q  =  ( 0 ... M ) )
18259, 181eleqtrrd 2545 . . . . . . . . . 10  |-  ( ph  ->  K  e.  dom  Q
)
183 fvelrn 6000 . . . . . . . . . 10  |-  ( ( Fun  Q  /\  K  e.  dom  Q )  -> 
( Q `  K
)  e.  ran  Q
)
184179, 182, 183syl2anc 659 . . . . . . . . 9  |-  ( ph  ->  ( Q `  K
)  e.  ran  Q
)
185177, 184eqeltrd 2542 . . . . . . . 8  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  e.  ran  Q
)
186 oveq1 6277 . . . . . . . . . . 11  |-  ( k  =  ( ( ( E `  Y )  -  Y )  /  T )  ->  (
k  x.  T )  =  ( ( ( ( E `  Y
)  -  Y )  /  T )  x.  T ) )
187186oveq2d 6286 . . . . . . . . . 10  |-  ( k  =  ( ( ( E `  Y )  -  Y )  /  T )  ->  (
( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  +  ( k  x.  T ) )  =  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( ( ( ( E `  Y )  -  Y )  /  T )  x.  T
) ) )
188187eleq1d 2523 . . . . . . . . 9  |-  ( k  =  ( ( ( E `  Y )  -  Y )  /  T )  ->  (
( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( k  x.  T ) )  e.  ran  Q  <->  ( ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  +  ( ( ( ( E `  Y )  -  Y
)  /  T )  x.  T ) )  e.  ran  Q ) )
189188rspcev 3207 . . . . . . . 8  |-  ( ( ( ( ( E `
 Y )  -  Y )  /  T
)  e.  ZZ  /\  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  e.  ran  Q
)  ->  E. k  e.  ZZ  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( k  x.  T
) )  e.  ran  Q )
190172, 185, 189syl2anc 659 . . . . . . 7  |-  ( ph  ->  E. k  e.  ZZ  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( k  x.  T ) )  e.  ran  Q
)
191190adantr 463 . . . . . 6  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  E. k  e.  ZZ  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( k  x.  T ) )  e.  ran  Q
)
192 oveq1 6277 . . . . . . . . 9  |-  ( x  =  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  ->  (
x  +  ( k  x.  T ) )  =  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( k  x.  T
) ) )
193192eleq1d 2523 . . . . . . . 8  |-  ( x  =  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  ->  (
( x  +  ( k  x.  T ) )  e.  ran  Q  <->  ( ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  +  ( k  x.  T ) )  e.  ran  Q ) )
194193rexbidv 2965 . . . . . . 7  |-  ( x  =  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  ->  ( E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  (
( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  +  ( k  x.  T ) )  e.  ran  Q ) )
195194elrab 3254 . . . . . 6  |-  ( ( ( Q `  K
)  -  ( ( E `  Y )  -  Y ) )  e.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q }  <->  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  e.  ( C [,] D
)  /\  E. k  e.  ZZ  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( k  x.  T
) )  e.  ran  Q ) )
196148, 191, 195sylanbrc 662 . . . . 5  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  {
x  e.  ( C [,] D )  |  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  ran  Q } )
197 elun2 3658 . . . . 5  |-  ( ( ( Q `  K
)  -  ( ( E `  Y )  -  Y ) )  e.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q }  ->  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  e.  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } ) )
198196, 197syl 16 . . . 4  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } ) )
199 fourierdlem63.x . . . 4  |-  X  =  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )
200198, 199, 183eltr4g 2560 . . 3  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  X  e.  H
)
201 elfzelz 11691 . . . . . . . . 9  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
202201ad2antlr 724 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  -> 
j  e.  ZZ )
203 elfzoelz 11804 . . . . . . . . . . 11  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ZZ )
20431, 203syl 16 . . . . . . . . . 10  |-  ( ph  ->  J  e.  ZZ )
205204ad2antrr 723 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  ->  J  e.  ZZ )
206 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  ( S `  J )  <  ( S `  j
) )
20721simprd 461 . . . . . . . . . . . . 13  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  H ) )
208207ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
20969ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  J  e.  ( 0 ... N
) )
210 simplr 753 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  j  e.  ( 0 ... N
) )
211 isorel 6197 . . . . . . . . . . . 12  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  /\  ( J  e.  ( 0 ... N
)  /\  j  e.  ( 0 ... N
) ) )  -> 
( J  <  j  <->  ( S `  J )  <  ( S `  j ) ) )
212208, 209, 210, 211syl12anc 1224 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  ( J  <  j  <->  ( S `  J )  <  ( S `  j )
) )
213206, 212mpbird 232 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  J  <  j )
214213adantrr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  ->  J  <  j )
215 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  ( S `  j )  <  ( S `  ( J  +  1 ) ) )
216207ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
217 simplr 753 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  j  e.  ( 0 ... N
) )
21833ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  ( J  +  1 )  e.  ( 0 ... N ) )
219 isorel 6197 . . . . . . . . . . . 12  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  /\  ( j  e.  ( 0 ... N
)  /\  ( J  +  1 )  e.  ( 0 ... N
) ) )  -> 
( j  <  ( J  +  1 )  <-> 
( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
220216, 217, 218, 219syl12anc 1224 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  (
j  <  ( J  +  1 )  <->  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )
221215, 220mpbird 232 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  j  <  ( J  +  1 ) )
222221adantrl 713 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  -> 
j  <  ( J  +  1 ) )
223 btwnnz 10935 . . . . . . . . 9  |-  ( ( J  e.  ZZ  /\  J  <  j  /\  j  <  ( J  +  1 ) )  ->  -.  j  e.  ZZ )
224205, 214, 222, 223syl3anc 1226 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  ->  -.  j  e.  ZZ )
225202, 224pm2.65da 574 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  -.  ( ( S `  J )  <  ( S `  j )  /\  ( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
226225adantlr 712 . . . . . 6  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  ->  -.  ( ( S `  J )  <  ( S `  j )  /\  ( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
22770ad2antrr 723 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  e.  RR )
22875ad2antrr 723 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  Y  e.  RR )
22930ffvelrnda 6007 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( S `  j )  e.  RR )
230229adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  e.  RR )
23174simp2d 1007 . . . . . . . . . 10  |-  ( ph  ->  ( S `  J
)  <_  Y )
232231ad2antrr 723 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  <_  Y )
233106, 199syl6breqr 4479 . . . . . . . . . . . 12  |-  ( ph  ->  Y  <  X )
234233adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  ( S `  j )  =  X )  ->  Y  <  X )
235 eqcom 2463 . . . . . . . . . . . . 13  |-  ( X  =  ( S `  j )  <->  ( S `  j )  =  X )
236235biimpri 206 . . . . . . . . . . . 12  |-  ( ( S `  j )  =  X  ->  X  =  ( S `  j ) )
237236adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  ( S `  j )  =  X )  ->  X  =  ( S `  j ) )
238234, 237breqtrd 4463 . . . . . . . . . 10  |-  ( (
ph  /\  ( S `  j )  =  X )  ->  Y  <  ( S `  j ) )
239238adantlr 712 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  Y  <  ( S `  j
) )
240227, 228, 230, 232, 239lelttrd 9729 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  <  ( S `  j
) )
241240adantllr 716 . . . . . . 7  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  <  ( S `  j
) )
242 simpr 459 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  =  X )
243199, 139syl5eqbr 4472 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  X  <  ( S `  ( J  +  1 ) ) )
244243adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  ( S `  j )  =  X )  ->  X  <  ( S `  ( J  +  1 ) ) )
245242, 244eqbrtrd 4459 . . . . . . . 8  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  <  ( S `  ( J  +  1 ) ) )
246245adantlr 712 . . . . . . 7  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  <  ( S `  ( J  +  1 ) ) )
247241, 246jca 530 . . . . . 6  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )
248226, 247mtand 657 . . . . 5  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  ->  -.  ( S `  j )  =  X )
249248nrexdv 2910 . . . 4  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  -.  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
250 isof1o 6196 . . . . . . . . 9  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  H )  ->  S : ( 0 ... N ) -1-1-onto-> H )
251207, 250syl 16 . . . . . . . 8  |-  ( ph  ->  S : ( 0 ... N ) -1-1-onto-> H )
252 f1ofo 5805 . . . . . . . 8  |-  ( S : ( 0 ... N ) -1-1-onto-> H  ->  S :
( 0 ... N
) -onto-> H )
253251, 252syl 16 . . . . . . 7  |-  ( ph  ->  S : ( 0 ... N ) -onto-> H )
254 foelrn 6026 . . . . . . 7  |-  ( ( S : ( 0 ... N ) -onto-> H  /\  X  e.  H
)  ->  E. j  e.  ( 0 ... N
) X  =  ( S `  j ) )
255253, 254sylan 469 . . . . . 6  |-  ( (
ph  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) X  =  ( S `  j ) )
256235rexbii 2956 . . . . . 6  |-  ( E. j  e.  ( 0 ... N ) X  =  ( S `  j )  <->  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
257255, 256sylib 196 . . . . 5  |-  ( (
ph  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
258257adantlr 712 . . . 4  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
259249, 258mtand 657 . . 3  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  -.  X  e.  H )
260200, 259pm2.65da 574 . 2  |-  ( ph  ->  -.  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )
26152, 60, 260nltled 31720 1  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  <_  ( Q `  K ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823   A.wral 2804   E.wrex 2805   {crab 2808    u. cun 3459    C_ wss 3461   {cpr 4018   class class class wbr 4439    |-> cmpt 4497   dom cdm 4988   ran crn 4989   iotacio 5532   Fun wfun 5564   -->wf 5566   -onto->wfo 5568   -1-1-onto->wf1o 5569   ` cfv 5570    Isom wiso 5571  (class class class)co 6270    ^m cmap 7412   CCcc 9479   RRcr 9480   0cc0 9481   1c1 9482    + caddc 9484    x. cmul 9486   RR*cxr 9616    < clt 9617    <_ cle 9618    - cmin 9796    / cdiv 10202   NNcn 10531   ZZcz 10860   (,]cioc 11533   [,)cico 11534   [,]cicc 11535   ...cfz 11675  ..^cfzo 11799   |_cfl 11908   #chash 12390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-iin 4318  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fi 7863  df-sup 7893  df-oi 7927  df-card 8311  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ioo 11536  df-ioc 11537  df-ico 11538  df-icc 11539  df-fz 11676  df-fzo 11800  df-fl 11910  df-seq 12093  df-exp 12152  df-hash 12391  df-cj 13017  df-re 13018  df-im 13019  df-sqrt 13153  df-abs 13154  df-rest 14915  df-topgen 14936  df-psmet 18609  df-xmet 18610  df-met 18611  df-bl 18612  df-mopn 18613  df-top 19569  df-bases 19571  df-topon 19572  df-cld 19690  df-ntr 19691  df-cls 19692  df-nei 19769  df-lp 19807  df-cmp 20057
This theorem is referenced by:  fourierdlem79  32210
  Copyright terms: Public domain W3C validator