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

Theorem fourierdlem63 31793
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.c . . . . . . . . 9  |-  ( ph  ->  C  e.  RR )
21adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  C  e.  RR )
3 fourierdlem63.d . . . . . . . . 9  |-  ( ph  ->  D  e.  RR )
43adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  D  e.  RR )
5 fourierdlem63.q . . . . . . . . . . . . . 14  |-  ( ph  ->  Q  e.  ( P `
 M ) )
6 fourierdlem63.m . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
7 fourierdlem63.p . . . . . . . . . . . . . . . 16  |-  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 ) ) ) } )
87fourierdlem2 31732 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) ) ) )
96, 8syl 16 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) ) )
105, 9mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
1110simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
12 elmapi 7452 . . . . . . . . . . . 12  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
1311, 12syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
14 fourierdlem63.k . . . . . . . . . . 11  |-  ( ph  ->  K  e.  ( 0 ... M ) )
1513, 14ffvelrnd 6033 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  K
)  e.  RR )
167, 6, 5fourierdlem11 31741 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
1716simp1d 1008 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR )
1817rexrd 9655 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR* )
1916simp2d 1009 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  RR )
20 iocssre 11616 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
2118, 19, 20syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( A (,] B
)  C_  RR )
2216simp3d 1010 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  <  B )
23 fourierdlem63.t . . . . . . . . . . . . . 14  |-  T  =  ( B  -  A
)
24 fourierdlem63.e . . . . . . . . . . . . . 14  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
2517, 19, 22, 23, 24fourierdlem4 31734 . . . . . . . . . . . . 13  |-  ( ph  ->  E : RR --> ( A (,] B ) )
26 fourierdlem63.y . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  e.  ( ( S `  J ) [,) ( S `  ( J  +  1
) ) ) )
27 fourierdlem63.cltd . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  C  <  D )
28 fourierdlem63.o . . . . . . . . . . . . . . . . . . . . . . 23  |-  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 ) ) ) } )
29 fourierdlem63.h . . . . . . . . . . . . . . . . . . . . . . 23  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
30 fourierdlem63.n . . . . . . . . . . . . . . . . . . . . . . 23  |-  N  =  ( ( # `  H
)  -  1 )
31 fourierdlem63.s . . . . . . . . . . . . . . . . . . . . . . 23  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
3223, 7, 6, 5, 1, 3, 27, 28, 29, 30, 31fourierdlem54 31784 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( N  e.  NN  /\  S  e.  ( O `  N
) )  /\  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) ) )
3332simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
3433simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  S  e.  ( O `
 N ) )
3533simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  NN )
3628fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) ) )
3735, 36syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) ) ) )
3834, 37mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) )
3938simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... N ) ) )
40 elmapi 7452 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
4139, 40syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S : ( 0 ... N ) --> RR )
42 fourierdlem63.j . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  e.  ( 0..^ N ) )
43 elfzofz 11823 . . . . . . . . . . . . . . . . . 18  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
4442, 43syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  J  e.  ( 0 ... N ) )
4541, 44ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S `  J
)  e.  RR )
46 fzofzp1 11889 . . . . . . . . . . . . . . . . . . 19  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
4742, 46syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
4841, 47ffvelrnd 6033 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR )
4948rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR* )
50 elico2 11600 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) ) )
5145, 49, 50syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Y  e.  ( ( S `  J
) [,) ( S `
 ( J  + 
1 ) ) )  <-> 
( Y  e.  RR  /\  ( S `  J
)  <_  Y  /\  Y  <  ( S `  ( J  +  1
) ) ) ) )
5226, 51mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y  e.  RR  /\  ( S `  J
)  <_  Y  /\  Y  <  ( S `  ( J  +  1
) ) ) )
5352simp1d 1008 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
5425, 53ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  Y
)  e.  ( A (,] B ) )
5521, 54sseldd 3510 . . . . . . . . . . 11  |-  ( ph  ->  ( E `  Y
)  e.  RR )
5655, 53resubcld 9999 . . . . . . . . . 10  |-  ( ph  ->  ( ( E `  Y )  -  Y
)  e.  RR )
5715, 56resubcld 9999 . . . . . . . . 9  |-  ( ph  ->  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  e.  RR )
5857adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  RR )
59 icossicc 11623 . . . . . . . . . . . . . . . 16  |-  ( ( S `  J ) [,) ( S `  ( J  +  1
) ) )  C_  ( ( S `  J ) [,] ( S `  ( J  +  1 ) ) )
6059a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( S `  J ) [,) ( S `  ( J  +  1 ) ) )  C_  ( ( S `  J ) [,] ( S `  ( J  +  1 ) ) ) )
611rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR* )
623rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D  e.  RR* )
6328, 35, 34fourierdlem15 31745 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  S : ( 0 ... N ) --> ( C [,] D ) )
6461, 62, 63, 42fourierdlem8 31738 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( S `  J ) [,] ( S `  ( J  +  1 ) ) )  C_  ( C [,] D ) )
6560, 64sstrd 3519 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( S `  J ) [,) ( S `  ( J  +  1 ) ) )  C_  ( C [,] D ) )
6665, 26sseldd 3510 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  ( C [,] D ) )
67 elicc2 11601 . . . . . . . . . . . . . 14  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( Y  e.  ( C [,] D )  <-> 
( Y  e.  RR  /\  C  <_  Y  /\  Y  <_  D ) ) )
681, 3, 67syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y  e.  ( C [,] D )  <-> 
( Y  e.  RR  /\  C  <_  Y  /\  Y  <_  D ) ) )
6966, 68mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( Y  e.  RR  /\  C  <_  Y  /\  Y  <_  D ) )
7069simp2d 1009 . . . . . . . . . . 11  |-  ( ph  ->  C  <_  Y )
7115, 55resubcld 9999 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q `  K )  -  ( E `  Y )
)  e.  RR )
72 fourierdlem63.eyltqk . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E `  Y
)  <  ( Q `  K ) )
7355, 15posdifd 10151 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E `  Y )  <  ( Q `  K )  <->  0  <  ( ( Q `
 K )  -  ( E `  Y ) ) ) )
7472, 73mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( ( Q `  K )  -  ( E `  Y ) ) )
7571, 74elrpd 11266 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  K )  -  ( E `  Y )
)  e.  RR+ )
76 ltaddrp 11264 . . . . . . . . . . . . 13  |-  ( ( Y  e.  RR  /\  ( ( Q `  K )  -  ( E `  Y )
)  e.  RR+ )  ->  Y  <  ( Y  +  ( ( Q `
 K )  -  ( E `  Y ) ) ) )
7753, 75, 76syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  Y  <  ( Y  +  ( ( Q `
 K )  -  ( E `  Y ) ) ) )
7815recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  K
)  e.  CC )
7955recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  Y
)  e.  CC )
8053recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  CC )
8178, 79, 80subsub3d 9972 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  =  ( ( ( Q `  K
)  +  Y )  -  ( E `  Y ) ) )
8278, 80addcomd 9793 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q `  K )  +  Y
)  =  ( Y  +  ( Q `  K ) ) )
8382oveq1d 6310 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Q `
 K )  +  Y )  -  ( E `  Y )
)  =  ( ( Y  +  ( Q `
 K ) )  -  ( E `  Y ) ) )
8480, 78, 79addsubassd 9962 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Y  +  ( Q `  K ) )  -  ( E `
 Y ) )  =  ( Y  +  ( ( Q `  K )  -  ( E `  Y )
) ) )
8581, 83, 843eqtrrd 2513 . . . . . . . . . . . 12  |-  ( ph  ->  ( Y  +  ( ( Q `  K
)  -  ( E `
 Y ) ) )  =  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
8677, 85breqtrd 4477 . . . . . . . . . . 11  |-  ( ph  ->  Y  <  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
871, 53, 57, 70, 86lelttrd 9751 . . . . . . . . . 10  |-  ( ph  ->  C  <  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
881, 57, 87ltled 9744 . . . . . . . . 9  |-  ( ph  ->  C  <_  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) ) )
8988adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  C  <_  (
( Q `  K
)  -  ( ( E `  Y )  -  Y ) ) )
9048adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( S `  ( J  +  1
) )  e.  RR )
9115adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( Q `  K )  e.  RR )
9224a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
93 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( S `  ( J  +  1
) )  ->  x  =  ( S `  ( J  +  1
) ) )
94 oveq2 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( S `  ( J  +  1
) )  ->  ( B  -  x )  =  ( B  -  ( S `  ( J  +  1 ) ) ) )
9594oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )
9695fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( S `  ( J  +  1
) )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) ) )
9796oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) )
9893, 97oveq12d 6313 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 ( J  + 
1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) ) )
9998adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  =  ( S `  ( J  +  1 ) ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `  ( J  +  1
) )  +  ( ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) ) )
10019, 48resubcld 9999 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  -  ( S `  ( J  +  1 ) ) )  e.  RR )
10123a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  T  =  ( B  -  A ) )
10219, 17resubcld 9999 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B  -  A
)  e.  RR )
103101, 102eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  e.  RR )
104 0re 9608 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR
105104a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  e.  RR )
10617, 19posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
10722, 106mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  <  ( B  -  A ) )
108101eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( B  -  A
)  =  T )
109107, 108breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  <  T )
110105, 109gtned 9731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  =/=  0 )
111100, 103, 110redivcld 10384 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T )  e.  RR )
112111flcld 11915 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  ZZ )
113112zred 10978 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  RR )
114113, 103remulcld 9636 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T )  e.  RR )
11548, 114readdcld 9635 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  +  ( ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) )  e.  RR )
11692, 99, 48, 115fvmptd 5962 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  =  ( ( S `  ( J  +  1 ) )  +  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) ) )
117116, 115eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  RR )
118117, 48resubcld 9999 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  e.  RR )
119118adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  e.  RR )
12091, 119resubcld 9999 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) )  e.  RR )
12152simp3d 1010 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  <  ( S `
 ( J  + 
1 ) ) )
12253, 48, 121ltled 9744 . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  <_  ( S `  ( J  +  1 ) ) )
12317, 19, 22, 23, 24, 53, 48, 122fourierdlem7 31737 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  <_  ( ( E `
 Y )  -  Y ) )
124118, 56, 15lesub2d 10172 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  <_  ( ( E `  Y )  -  Y )  <->  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  <_ 
( ( Q `  K )  -  (
( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) ) ) )
125123, 124mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  <_  ( ( Q `  K )  -  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) ) ) )
126125adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <_  (
( Q `  K
)  -  ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( S `  ( J  +  1
) ) ) ) )
12778adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( Q `  K )  e.  CC )
128117recnd 9634 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  CC )
129128adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  CC )
13090recnd 9634 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( S `  ( J  +  1
) )  e.  CC )
131127, 129, 130subsubd 9970 . . . . . . . . . . . . 13  |-  ( (
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
) ) ) )
13278, 128subcld 9942 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  e.  CC )
13348recnd 9634 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  CC )
134132, 133addcomd 9793 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  +  ( S `
 ( J  + 
1 ) ) )  =  ( ( S `
 ( J  + 
1 ) )  +  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) ) )
135134adantr 465 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) ) ) )
136131, 135eqtrd 2508 . . . . . . . . . . . 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 ) ) ) ) ) )
137 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )
138117adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  RR )
13991, 138sublt0d 31395 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  <  0  <->  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) ) )
140137, 139mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  <  0 )
14191, 138resubcld 9999 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  e.  RR )
142 ltaddneg 31384 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) )
143141, 90, 142syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
144140, 143mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( S `
 ( J  + 
1 ) )  +  ( ( Q `  K )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )  <  ( S `
 ( J  + 
1 ) ) )
145136, 144eqbrtrd 4473 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) ) )  <  ( S `
 ( J  + 
1 ) ) )
14658, 120, 90, 126, 145lelttrd 9751 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <  ( S `  ( J  +  1 ) ) )
14763, 47ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  ( C [,] D ) )
148 elicc2 11601 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) )
1491, 3, 148syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  e.  ( C [,] D )  <-> 
( ( S `  ( J  +  1
) )  e.  RR  /\  C  <_  ( S `  ( J  +  1 ) )  /\  ( S `  ( J  +  1 ) )  <_  D ) ) )
150147, 149mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  e.  RR  /\  C  <_  ( S `  ( J  +  1 ) )  /\  ( S `  ( J  +  1 ) )  <_  D ) )
151150simp3d 1010 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  ( J  +  1 ) )  <_  D )
152151adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( S `  ( J  +  1
) )  <_  D
)
15358, 90, 4, 146, 152ltletrd 9753 . . . . . . . . 9  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <  D
)
15458, 4, 153ltled 9744 . . . . . . . 8  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <_  D
)
1552, 4, 58, 89, 154eliccd 31425 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  ( C [,] D ) )
156 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  x  =  Y )
157 oveq2 6303 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  Y  ->  ( B  -  x )  =  ( B  -  Y ) )
158157oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  Y  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  Y )  /  T ) )
159158fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( x  =  Y  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  Y
)  /  T ) ) )
160159oveq1d 6310 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T ) )
161156, 160oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
) ) )
162161adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  =  Y )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
) ) )
16319, 53resubcld 9999 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B  -  Y
)  e.  RR )
164163, 103, 110redivcld 10384 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  -  Y )  /  T
)  e.  RR )
165164flcld 11915 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  (
( B  -  Y
)  /  T ) )  e.  ZZ )
166165zred 10978 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( |_ `  (
( B  -  Y
)  /  T ) )  e.  RR )
167166, 103remulcld 9636 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
)  e.  RR )
16853, 167readdcld 9635 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y  +  ( ( |_ `  (
( B  -  Y
)  /  T ) )  x.  T ) )  e.  RR )
16992, 162, 53, 168fvmptd 5962 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  Y
)  =  ( Y  +  ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T ) ) )
170169oveq1d 6310 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E `  Y )  -  Y
)  =  ( ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T ) )  x.  T ) )  -  Y ) )
171170oveq1d 6310 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E `
 Y )  -  Y )  /  T
)  =  ( ( ( Y  +  ( ( |_ `  (
( B  -  Y
)  /  T ) )  x.  T ) )  -  Y )  /  T ) )
172167recnd 9634 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
)  e.  CC )
17380, 172pncan2d 9944 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Y  +  ( ( |_ `  ( ( B  -  Y )  /  T
) )  x.  T
) )  -  Y
)  =  ( ( |_ `  ( ( B  -  Y )  /  T ) )  x.  T ) )
174173oveq1d 6310 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Y  +  ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T ) )  -  Y )  /  T
)  =  ( ( ( |_ `  (
( B  -  Y
)  /  T ) )  x.  T )  /  T ) )
175166recnd 9634 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  (
( B  -  Y
)  /  T ) )  e.  CC )
176103recnd 9634 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  CC )
177175, 176, 110divcan4d 10338 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( |_
`  ( ( B  -  Y )  /  T ) )  x.  T )  /  T
)  =  ( |_
`  ( ( B  -  Y )  /  T ) ) )
178171, 174, 1773eqtrd 2512 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( E `
 Y )  -  Y )  /  T
)  =  ( |_
`  ( ( B  -  Y )  /  T ) ) )
179178, 165eqeltrd 2555 . . . . . . . . 9  |-  ( ph  ->  ( ( ( E `
 Y )  -  Y )  /  T
)  e.  ZZ )
18056recnd 9634 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E `  Y )  -  Y
)  e.  CC )
181180, 176, 110divcan1d 10333 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( E `  Y )  -  Y )  /  T )  x.  T
)  =  ( ( E `  Y )  -  Y ) )
182181oveq2d 6311 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  =  ( ( ( Q `  K
)  -  ( ( E `  Y )  -  Y ) )  +  ( ( E `
 Y )  -  Y ) ) )
18378, 180npcand 9946 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( E `  Y
)  -  Y ) )  =  ( Q `
 K ) )
184182, 183eqtrd 2508 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  =  ( Q `
 K ) )
185 ffun 5739 . . . . . . . . . . . 12  |-  ( Q : ( 0 ... M ) --> RR  ->  Fun 
Q )
18613, 185syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Fun  Q )
187 fdm 5741 . . . . . . . . . . . . . 14  |-  ( Q : ( 0 ... M ) --> RR  ->  dom 
Q  =  ( 0 ... M ) )
18813, 187syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  dom  Q  =  ( 0 ... M ) )
189188eqcomd 2475 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... M
)  =  dom  Q
)
19014, 189eleqtrd 2557 . . . . . . . . . . 11  |-  ( ph  ->  K  e.  dom  Q
)
191 fvelrn 6025 . . . . . . . . . . 11  |-  ( ( Fun  Q  /\  K  e.  dom  Q )  -> 
( Q `  K
)  e.  ran  Q
)
192186, 190, 191syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  K
)  e.  ran  Q
)
193184, 192eqeltrd 2555 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( ( ( ( E `
 Y )  -  Y )  /  T
)  x.  T ) )  e.  ran  Q
)
194 oveq1 6302 . . . . . . . . . . . 12  |-  ( k  =  ( ( ( E `  Y )  -  Y )  /  T )  ->  (
k  x.  T )  =  ( ( ( ( E `  Y
)  -  Y )  /  T )  x.  T ) )
195194oveq2d 6311 . . . . . . . . . . 11  |-  ( k  =  ( ( ( E `  Y )  -  Y )  /  T )  ->  (
( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )  +  ( k  x.  T ) )  =  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( ( ( ( E `  Y )  -  Y )  /  T )  x.  T
) ) )
196195eleq1d 2536 . . . . . . . . . 10  |-  ( 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 ) )
197196rspcev 3219 . . . . . . . . 9  |-  ( ( ( ( ( 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 )
198179, 193, 197syl2anc 661 . . . . . . . 8  |-  ( ph  ->  E. k  e.  ZZ  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( k  x.  T ) )  e.  ran  Q
)
199198adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  E. k  e.  ZZ  ( ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  +  ( k  x.  T ) )  e.  ran  Q
)
200155, 199jca 532 . . . . . 6  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  e.  ( C [,] D
)  /\  E. k  e.  ZZ  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( k  x.  T
) )  e.  ran  Q ) )
201 oveq1 6302 . . . . . . . . 9  |-  ( x  =  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  ->  (
x  +  ( k  x.  T ) )  =  ( ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  +  ( k  x.  T
) ) )
202201eleq1d 2536 . . . . . . . 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 ) )
203202rexbidv 2978 . . . . . . 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 ) )
204203elrab 3266 . . . . . 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 ) )
205200, 204sylibr 212 . . . . 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 } )
206 elun2 3677 . . . . 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 } ) )
207205, 206syl 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 } ) )
208 fourierdlem63.x . . . . . 6  |-  X  =  ( ( Q `  K )  -  (
( E `  Y
)  -  Y ) )
209208a1i 11 . . . . 5  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  X  =  ( ( Q `  K
)  -  ( ( E `  Y )  -  Y ) ) )
21029a1i 11 . . . . 5  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } ) )
211209, 210eleq12d 2549 . . . 4  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( X  e.  H  <->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  e.  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
212207, 211mpbird 232 . . 3  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  X  e.  H
)
21332simprd 463 . . . . . . . . . 10  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  H ) )
214 isof1o 6220 . . . . . . . . . 10  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  H )  ->  S : ( 0 ... N ) -1-1-onto-> H )
215213, 214syl 16 . . . . . . . . 9  |-  ( ph  ->  S : ( 0 ... N ) -1-1-onto-> H )
216 f1ofo 5829 . . . . . . . . 9  |-  ( S : ( 0 ... N ) -1-1-onto-> H  ->  S :
( 0 ... N
) -onto-> H )
217215, 216syl 16 . . . . . . . 8  |-  ( ph  ->  S : ( 0 ... N ) -onto-> H )
218217adantr 465 . . . . . . 7  |-  ( (
ph  /\  X  e.  H )  ->  S : ( 0 ... N ) -onto-> H )
219 simpr 461 . . . . . . 7  |-  ( (
ph  /\  X  e.  H )  ->  X  e.  H )
220 foelrn 6051 . . . . . . 7  |-  ( ( S : ( 0 ... N ) -onto-> H  /\  X  e.  H
)  ->  E. j  e.  ( 0 ... N
) X  =  ( S `  j ) )
221218, 219, 220syl2anc 661 . . . . . 6  |-  ( (
ph  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) X  =  ( S `  j ) )
222 eqcom 2476 . . . . . . . 8  |-  ( X  =  ( S `  j )  <->  ( S `  j )  =  X )
223222rexbii 2969 . . . . . . 7  |-  ( E. j  e.  ( 0 ... N ) X  =  ( S `  j )  <->  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
224223imbi2i 312 . . . . . 6  |-  ( ( ( ph  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) X  =  ( S `  j ) )  <->  ( ( ph  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N ) ( S `  j
)  =  X ) )
225221, 224mpbi 208 . . . . 5  |-  ( (
ph  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
226225adantlr 714 . . . 4  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  X  e.  H )  ->  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
22745ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  e.  RR )
22853ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  Y  e.  RR )
22941ffvelrnda 6032 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( S `  j )  e.  RR )
230229adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  e.  RR )
23152simp2d 1009 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  J
)  <_  Y )
232231ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  <_  Y )
233208eqcomi 2480 . . . . . . . . . . . . . . 15  |-  ( ( Q `  K )  -  ( ( E `
 Y )  -  Y ) )  =  X
23486, 233syl6breq 4492 . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  <  X )
235234adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( S `  j )  =  X )  ->  Y  <  X )
236222biimpri 206 . . . . . . . . . . . . . 14  |-  ( ( S `  j )  =  X  ->  X  =  ( S `  j ) )
237236adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( S `  j )  =  X )  ->  X  =  ( S `  j ) )
238235, 237breqtrd 4477 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( S `  j )  =  X )  ->  Y  <  ( S `  j ) )
239238adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  Y  <  ( S `  j
) )
240227, 228, 230, 232, 239lelttrd 9751 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  <  ( S `  j
) )
241240adantllr 718 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  J )  <  ( S `  j
) )
242 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  =  X )
243146idi 2 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  ( ( Q `
 K )  -  ( ( E `  Y )  -  Y
) )  <  ( S `  ( J  +  1 ) ) )
244208, 243syl5eqbr 4486 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  X  <  ( S `  ( J  +  1 ) ) )
245244adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  ( S `  j )  =  X )  ->  X  <  ( S `  ( J  +  1 ) ) )
246242, 245eqbrtrd 4473 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  <  ( S `  ( J  +  1 ) ) )
247246adantlr 714 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  ( S `  j )  <  ( S `  ( J  +  1 ) ) )
248241, 247jca 532 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )
249 elfzelz 11700 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
250249ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  -> 
j  e.  ZZ )
251 elfzoelz 11809 . . . . . . . . . . . . . 14  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ZZ )
25242, 251syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  J  e.  ZZ )
253252ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  ->  J  e.  ZZ )
254 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  ( S `  J )  <  ( S `  j
) )
255213ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
25644ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  J  e.  ( 0 ... N
) )
257 simplr 754 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  j  e.  ( 0 ... N
) )
258 isorel 6221 . . . . . . . . . . . . . . 15  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  /\  ( J  e.  ( 0 ... N
)  /\  j  e.  ( 0 ... N
) ) )  -> 
( J  <  j  <->  ( S `  J )  <  ( S `  j ) ) )
259255, 256, 257, 258syl12anc 1226 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  ( J  <  j  <->  ( S `  J )  <  ( S `  j )
) )
260254, 259mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  J )  <  ( S `  j
) )  ->  J  <  j )
261260adantrr 716 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  ->  J  <  j )
262 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  ( S `  j )  <  ( S `  ( J  +  1 ) ) )
263213ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
264 simplr 754 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  j  e.  ( 0 ... N
) )
26547ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  ( J  +  1 )  e.  ( 0 ... N ) )
266 isorel 6221 . . . . . . . . . . . . . . 15  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  /\  ( j  e.  ( 0 ... N
)  /\  ( J  +  1 )  e.  ( 0 ... N
) ) )  -> 
( j  <  ( J  +  1 )  <-> 
( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
267263, 264, 265, 266syl12anc 1226 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  (
j  <  ( J  +  1 )  <->  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )
268262, 267mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) )  ->  j  <  ( J  +  1 ) )
269268adantrl 715 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  -> 
j  <  ( J  +  1 ) )
270 btwnnz 10949 . . . . . . . . . . . 12  |-  ( ( J  e.  ZZ  /\  J  <  j  /\  j  <  ( J  +  1 ) )  ->  -.  j  e.  ZZ )
271253, 261, 269, 270syl3anc 1228 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( S `  J
)  <  ( S `  j )  /\  ( S `  j )  <  ( S `  ( J  +  1 ) ) ) )  ->  -.  j  e.  ZZ )
272250, 271pm2.65da 576 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  -.  ( ( S `  J )  <  ( S `  j )  /\  ( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
273272adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  ->  -.  ( ( S `  J )  <  ( S `  j )  /\  ( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
274273adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  ( S `  j )  =  X )  ->  -.  ( ( S `  J )  <  ( S `  j )  /\  ( S `  j
)  <  ( S `  ( J  +  1 ) ) ) )
275248, 274pm2.65da 576 . . . . . . 7  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  j  e.  ( 0 ... N
) )  ->  -.  ( S `  j )  =  X )
276275ralrimiva 2881 . . . . . 6  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  A. j  e.  ( 0 ... N )  -.  ( S `  j )  =  X )
277 ralnex 2913 . . . . . 6  |-  ( A. j  e.  ( 0 ... N )  -.  ( S `  j
)  =  X  <->  -.  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
278276, 277sylib 196 . . . . 5  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  -.  E. j  e.  ( 0 ... N
) ( S `  j )  =  X )
279278adantr 465 . . . 4  |-  ( ( ( ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  /\  X  e.  H )  ->  -.  E. j  e.  ( 0 ... N ) ( S `  j )  =  X )
280226, 279pm2.65da 576 . . 3  |-  ( (
ph  /\  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )  ->  -.  X  e.  H )
281212, 280pm2.65da 576 . 2  |-  ( ph  ->  -.  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) )
282117, 15lenltd 9742 . 2  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  <_  ( Q `  K )  <->  -.  ( Q `  K )  <  ( E `  ( S `  ( J  +  1 ) ) ) ) )
283281, 282mpbird 232 1  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  <_  ( Q `  K ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818   {crab 2821    u. cun 3479    C_ wss 3481   {cpr 4035   class class class wbr 4453    |-> cmpt 4511   dom cdm 5005   ran crn 5006   iotacio 5555   Fun wfun 5588   -->wf 5590   -onto->wfo 5592   -1-1-onto->wf1o 5593   ` cfv 5594    Isom wiso 5595  (class class class)co 6295    ^m cmap 7432   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505    + caddc 9507    x. cmul 9509   RR*cxr 9639    < clt 9640    <_ cle 9641    - cmin 9817    / cdiv 10218   NNcn 10548   ZZcz 10876   RR+crp 11232   (,]cioc 11542   [,)cico 11543   [,]cicc 11544   ...cfz 11684  ..^cfzo 11804   |_cfl 11907   #chash 12385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-n0 10808  df-z 10877  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-rest 14695  df-topgen 14716  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-top 19268  df-bases 19270  df-topon 19271  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-cmp 19755
This theorem is referenced by:  fourierdlem79  31809
  Copyright terms: Public domain W3C validator