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

Theorem fourierdlem51 32182
Description:  X is in the periodic partition, when the considered interval is centered at  X. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem51.a  |-  ( ph  ->  A  e.  RR )
fourierdlem51.b  |-  ( ph  ->  B  e.  RR )
fourierdlem51.alt0  |-  ( ph  ->  A  <  0 )
fourierdlem51.bgt0  |-  ( ph  ->  0  <  B )
fourierdlem51.t  |-  T  =  ( B  -  A
)
fourierdlem51.cfi  |-  ( ph  ->  C  e.  Fin )
fourierdlem51.css  |-  ( ph  ->  C  C_  ( A [,] B ) )
fourierdlem51.bc  |-  ( ph  ->  B  e.  C )
fourierdlem51.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem51.x  |-  ( ph  ->  X  e.  RR )
fourierdlem51.exc  |-  ( ph  ->  ( E `  X
)  e.  C )
fourierdlem51.d  |-  D  =  ( { ( A  +  X ) ,  ( B  +  X
) }  u.  {
y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)
fourierdlem51.f  |-  F  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... (
( # `  D )  -  1 ) ) ,  D ) )
fourierdlem51.h  |-  H  =  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
Assertion
Ref Expression
fourierdlem51  |-  ( ph  ->  X  e.  ran  F
)
Distinct variable groups:    A, k, x, y    B, k, x, y    C, k, x, y    D, f    k, E, x   
f, F    x, H    T, k, x, y    k, X, x, y    ph, f    ph, k, x
Allowed substitution hints:    ph( y)    A( f)    B( f)    C( f)    D( x, y, k)    T( f)    E( y, f)    F( x, y, k)    H( y, f, k)    X( f)

Proof of Theorem fourierdlem51
Dummy variables  i 
j  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem51.a . . . . . . 7  |-  ( ph  ->  A  e.  RR )
2 fourierdlem51.x . . . . . . 7  |-  ( ph  ->  X  e.  RR )
31, 2readdcld 9612 . . . . . 6  |-  ( ph  ->  ( A  +  X
)  e.  RR )
4 fourierdlem51.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
54, 2readdcld 9612 . . . . . 6  |-  ( ph  ->  ( B  +  X
)  e.  RR )
6 0red 9586 . . . . . . . . 9  |-  ( ph  ->  0  e.  RR )
7 fourierdlem51.alt0 . . . . . . . . 9  |-  ( ph  ->  A  <  0 )
81, 6, 2, 7ltadd1dd 10159 . . . . . . . 8  |-  ( ph  ->  ( A  +  X
)  <  ( 0  +  X ) )
92recnd 9611 . . . . . . . . 9  |-  ( ph  ->  X  e.  CC )
109addid2d 9770 . . . . . . . 8  |-  ( ph  ->  ( 0  +  X
)  =  X )
118, 10breqtrd 4463 . . . . . . 7  |-  ( ph  ->  ( A  +  X
)  <  X )
123, 2, 11ltled 9722 . . . . . 6  |-  ( ph  ->  ( A  +  X
)  <_  X )
13 fourierdlem51.bgt0 . . . . . . . . 9  |-  ( ph  ->  0  <  B )
146, 4, 2, 13ltadd1dd 10159 . . . . . . . 8  |-  ( ph  ->  ( 0  +  X
)  <  ( B  +  X ) )
1510, 14eqbrtrrd 4461 . . . . . . 7  |-  ( ph  ->  X  <  ( B  +  X ) )
162, 5, 15ltled 9722 . . . . . 6  |-  ( ph  ->  X  <_  ( B  +  X ) )
173, 5, 2, 12, 16eliccd 31780 . . . . 5  |-  ( ph  ->  X  e.  ( ( A  +  X ) [,] ( B  +  X ) ) )
184, 2resubcld 9983 . . . . . . . 8  |-  ( ph  ->  ( B  -  X
)  e.  RR )
19 fourierdlem51.t . . . . . . . . 9  |-  T  =  ( B  -  A
)
204, 1resubcld 9983 . . . . . . . . 9  |-  ( ph  ->  ( B  -  A
)  e.  RR )
2119, 20syl5eqel 2546 . . . . . . . 8  |-  ( ph  ->  T  e.  RR )
221, 6, 4, 7, 13lttrd 9732 . . . . . . . . . . 11  |-  ( ph  ->  A  <  B )
231, 4posdifd 10135 . . . . . . . . . . 11  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
2422, 23mpbid 210 . . . . . . . . . 10  |-  ( ph  ->  0  <  ( B  -  A ) )
2519eqcomi 2467 . . . . . . . . . . 11  |-  ( B  -  A )  =  T
2625a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  =  T )
2724, 26breqtrd 4463 . . . . . . . . 9  |-  ( ph  ->  0  <  T )
2827gt0ne0d 10113 . . . . . . . 8  |-  ( ph  ->  T  =/=  0 )
2918, 21, 28redivcld 10368 . . . . . . 7  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
3029flcld 11916 . . . . . 6  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
31 fourierdlem51.e . . . . . . . . 9  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
3231a1i 11 . . . . . . . 8  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
33 id 22 . . . . . . . . . 10  |-  ( x  =  X  ->  x  =  X )
34 oveq2 6278 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
3534oveq1d 6285 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
3635fveq2d 5852 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
3736oveq1d 6285 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
3833, 37oveq12d 6288 . . . . . . . . 9  |-  ( x  =  X  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
3938adantl 464 . . . . . . . 8  |-  ( (
ph  /\  x  =  X )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
4030zred 10965 . . . . . . . . . 10  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
4140, 21remulcld 9613 . . . . . . . . 9  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
422, 41readdcld 9612 . . . . . . . 8  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  RR )
4332, 39, 2, 42fvmptd 5936 . . . . . . 7  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
44 fourierdlem51.exc . . . . . . 7  |-  ( ph  ->  ( E `  X
)  e.  C )
4543, 44eqeltrrd 2543 . . . . . 6  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  C )
46 oveq1 6277 . . . . . . . . 9  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
4746oveq2d 6286 . . . . . . . 8  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  ( X  +  ( k  x.  T ) )  =  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
4847eleq1d 2523 . . . . . . 7  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( X  +  ( k  x.  T ) )  e.  C  <->  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  C ) )
4948rspcev 3207 . . . . . 6  |-  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ  /\  ( X  +  (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  C )  ->  E. k  e.  ZZ  ( X  +  (
k  x.  T ) )  e.  C )
5030, 45, 49syl2anc 659 . . . . 5  |-  ( ph  ->  E. k  e.  ZZ  ( X  +  (
k  x.  T ) )  e.  C )
51 oveq1 6277 . . . . . . . 8  |-  ( y  =  X  ->  (
y  +  ( k  x.  T ) )  =  ( X  +  ( k  x.  T
) ) )
5251eleq1d 2523 . . . . . . 7  |-  ( y  =  X  ->  (
( y  +  ( k  x.  T ) )  e.  C  <->  ( X  +  ( k  x.  T ) )  e.  C ) )
5352rexbidv 2965 . . . . . 6  |-  ( y  =  X  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C  <->  E. k  e.  ZZ  ( X  +  ( k  x.  T
) )  e.  C
) )
5453elrab 3254 . . . . 5  |-  ( X  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } 
<->  ( X  e.  ( ( A  +  X
) [,] ( B  +  X ) )  /\  E. k  e.  ZZ  ( X  +  ( k  x.  T
) )  e.  C
) )
5517, 50, 54sylanbrc 662 . . . 4  |-  ( ph  ->  X  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } )
56 elun2 3658 . . . 4  |-  ( X  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  X  e.  ( { ( A  +  X ) ,  ( B  +  X ) }  u.  { y  e.  ( ( A  +  X ) [,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) )
5755, 56syl 16 . . 3  |-  ( ph  ->  X  e.  ( { ( A  +  X
) ,  ( B  +  X ) }  u.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) )
58 fourierdlem51.d . . 3  |-  D  =  ( { ( A  +  X ) ,  ( B  +  X
) }  u.  {
y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)
5957, 58syl6eleqr 2553 . 2  |-  ( ph  ->  X  e.  D )
60 prfi 7787 . . . . . 6  |-  { ( A  +  X ) ,  ( B  +  X ) }  e.  Fin
61 snfi 7589 . . . . . . . 8  |-  { ( A  +  X ) }  e.  Fin
62 fourierdlem51.cfi . . . . . . . . 9  |-  ( ph  ->  C  e.  Fin )
63 fvres 5862 . . . . . . . . . . . . . 14  |-  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
)  =  ( E `
 x ) )
6463adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
)  =  ( E `
 x ) )
65 oveq1 6277 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  (
y  +  ( k  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
6665eleq1d 2523 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( y  +  ( k  x.  T ) )  e.  C  <->  ( x  +  ( k  x.  T ) )  e.  C ) )
6766rexbidv 2965 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C  <->  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
) )
6867elrab 3254 . . . . . . . . . . . . . . . 16  |-  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } 
<->  ( x  e.  ( ( A  +  X
) (,] ( B  +  X ) )  /\  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
) )
6968simprbi 462 . . . . . . . . . . . . . . 15  |-  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  C )
7069adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
)
71 nfv 1712 . . . . . . . . . . . . . . . 16  |-  F/ k
ph
72 nfre1 2915 . . . . . . . . . . . . . . . . . 18  |-  F/ k E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C
73 nfcv 2616 . . . . . . . . . . . . . . . . . 18  |-  F/_ k
( ( A  +  X ) (,] ( B  +  X )
)
7472, 73nfrab 3036 . . . . . . . . . . . . . . . . 17  |-  F/_ k { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
7574nfcri 2609 . . . . . . . . . . . . . . . 16  |-  F/ k  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }
7671, 75nfan 1933 . . . . . . . . . . . . . . 15  |-  F/ k ( ph  /\  x  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )
77 nfv 1712 . . . . . . . . . . . . . . 15  |-  F/ k ( E `  x
)  e.  C
78 simpl 455 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ph )
793rexrd 9632 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  +  X
)  e.  RR* )
80 iocssre 11607 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  +  X
)  e.  RR*  /\  ( B  +  X )  e.  RR )  ->  (
( A  +  X
) (,] ( B  +  X ) ) 
C_  RR )
8179, 5, 80syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  +  X ) (,] ( B  +  X )
)  C_  RR )
8281adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( ( A  +  X ) (,] ( B  +  X
) )  C_  RR )
83 elrabi 3251 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  x  e.  ( ( A  +  X
) (,] ( B  +  X ) ) )
8483adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  x  e.  ( ( A  +  X ) (,] ( B  +  X )
) )
8582, 84sseldd 3490 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  x  e.  RR )
86 simpr 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
874adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
8887, 86resubcld 9983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
8921adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
9028adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
9188, 89, 90redivcld 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
9291flcld 11916 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
9392zred 10965 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
9493, 89remulcld 9613 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
9586, 94readdcld 9612 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  RR )
9631fvmpt2 5939 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  RR )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
9786, 95, 96syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
9897ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
99 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ ) )
10092ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )
101 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  =  A )
1021rexrd 9632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A  e.  RR* )
1034rexrd 9632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  RR* )
1041, 4, 22ltled 9722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A  <_  B )
105 lbicc2 11639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
106102, 103, 104, 105syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A  e.  ( A [,] B ) )
107106adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  A  e.  ( A [,] B
) )
108101, 107eqeltrd 2542 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
109108adant423 31668 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( k  x.  T ) )  e.  ( A [,] B
) )
11099, 100, 109jca31 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A [,] B ) ) )
111 iocssicc 11615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A (,] B )  C_  ( A [,] B )
1121, 4, 22, 19, 31fourierdlem4 32135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  E : RR --> ( A (,] B ) )
113112ffvelrnda 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  e.  ( A (,] B
) )
114111, 113sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  e.  ( A [,] B
) )
11597, 114eqeltrrd 2543 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) )
116115ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) )
117102adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  A  e. 
RR* )
11887rexrd 9632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  B  e. 
RR* )
119 iocgtlb 31777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 x )  e.  ( A (,] B
) )  ->  A  <  ( E `  x
) )
120117, 118, 113, 119syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  A  < 
( E `  x
) )
121120ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  A  <  ( E `  x ) )
122 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  (
x  +  ( k  x.  T ) )  =  A )
123122eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  A  =  ( x  +  ( k  x.  T
) ) )
124123adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  A  =  ( x  +  (
k  x.  T ) ) )
125121, 124, 983brtr3d 4468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( k  x.  T ) )  < 
( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
126 zre 10864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ZZ  ->  k  e.  RR )
127126adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  RR )
12821adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  RR )
129127, 128remulcld 9613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  x.  T )  e.  RR )
130129adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
131130adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  x.  T )  e.  RR )
13294ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
133 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  x  e.  RR )
134131, 132, 133ltadd2d 9727 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
k  x.  T )  <  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T )  <->  ( x  +  ( k  x.  T ) )  < 
( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) ) )
135125, 134mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  x.  T )  <  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
136126ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  k  e.  RR )
13793ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  RR )
13821, 27elrpd 11256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  RR+ )
139138ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  T  e.  RR+ )
140136, 137, 139ltmul1d 11296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  <  ( |_ `  (
( B  -  x
)  /  T ) )  <->  ( k  x.  T )  <  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
141135, 140mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) )
142 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( |_
`  ( ( B  -  x )  /  T ) )  e. 
_V
143 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  e.  ZZ  <->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ ) )
144143anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ ) 
<->  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ ) ) )
145144anbi1d 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( ( ( (
ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  <->  ( (
( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A [,] B ) ) ) )
146 oveq1 6277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  x.  T )  =  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )
147146oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
x  +  ( j  x.  T ) )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
148147eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( x  +  ( j  x.  T ) )  e.  ( A [,] B )  <->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) ) )
149145, 148anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  <-> 
( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T ) )  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  ( A [,] B ) ) ) )
150 breq2 4443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
k  <  j  <->  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) ) )
151149, 150anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( ( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A [,] B ) )  /\  ( x  +  ( j  x.  T ) )  e.  ( A [,] B
) )  /\  k  <  j )  <->  ( (
( ( ( (
ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T ) )  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  ( A [,] B ) )  /\  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) ) ) )
152 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  =  ( k  +  1 )  <->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) ) )
153151, 152imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A [,] B ) )  /\  ( x  +  ( j  x.  T ) )  e.  ( A [,] B
) )  /\  k  <  j )  ->  j  =  ( k  +  1 ) )  <->  ( (
( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T ) )  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  ( A [,] B ) )  /\  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) ) ) )
154 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  k  ->  (
i  e.  ZZ  <->  k  e.  ZZ ) )
155154anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  k  ->  (
( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ ) 
<->  ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ ) ) )
156155anbi1d 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  k  ->  (
( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ ) 
<->  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ ) ) )
157 oveq1 6277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  k  ->  (
i  x.  T )  =  ( k  x.  T ) )
158157oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  k  ->  (
x  +  ( i  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
159158eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  k  ->  (
( x  +  ( i  x.  T ) )  e.  ( A [,] B )  <->  ( x  +  ( k  x.  T ) )  e.  ( A [,] B
) ) )
160156, 159anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  =  k  ->  (
( ( ( (
ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  <->  ( (
( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A [,] B ) ) ) )
161160anbi1d 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  =  k  ->  (
( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  <-> 
( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) ) ) )
162 breq1 4442 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  =  k  ->  (
i  <  j  <->  k  <  j ) )
163161, 162anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  =  k  ->  (
( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  ( x  +  ( i  x.  T
) )  e.  ( A [,] B ) )  /\  ( x  +  ( j  x.  T ) )  e.  ( A [,] B
) )  /\  i  <  j )  <->  ( (
( ( ( (
ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  k  <  j
) ) )
164 oveq1 6277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  =  k  ->  (
i  +  1 )  =  ( k  +  1 ) )
165164eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  =  k  ->  (
j  =  ( i  +  1 )  <->  j  =  ( k  +  1 ) ) )
166163, 165imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  k  ->  (
( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  ( x  +  ( i  x.  T
) )  e.  ( A [,] B ) )  /\  ( x  +  ( j  x.  T ) )  e.  ( A [,] B
) )  /\  i  <  j )  ->  j  =  ( i  +  1 ) )  <->  ( (
( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  k  <  j
)  ->  j  =  ( k  +  1 ) ) ) )
167 simp-6l 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  ph )
168167, 1syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  A  e.  RR )
169167, 4syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  B  e.  RR )
170167, 22syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  A  <  B )
171 simp-6r 770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  x  e.  RR )
172 simp-5r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  i  e.  ZZ )
173 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  j  e.  ZZ )
174 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  i  <  j )
175 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  ( x  +  ( i  x.  T ) )  e.  ( A [,] B
) )
176 simplr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  ( x  +  ( j  x.  T ) )  e.  ( A [,] B
) )
177168, 169, 170, 19, 171, 172, 173, 174, 175, 176fourierdlem6 32137 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( i  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  i  <  j
)  ->  j  =  ( i  +  1 ) )
178166, 177chvarv 2019 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
j  x.  T ) )  e.  ( A [,] B ) )  /\  k  <  j
)  ->  j  =  ( k  +  1 ) )
179142, 153, 178vtocl 3158 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T ) )  e.  ZZ )  /\  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  ( A [,] B ) )  /\  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) )
180110, 116, 141, 179syl21anc 1225 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) )
181180oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  =  ( ( k  +  1 )  x.  T ) )
182181oveq2d 6286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( x  +  ( ( k  +  1 )  x.  T ) ) )
183127recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  CC )
18421recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  CC )
185184adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  CC )
186183, 185adddirp1d 31729 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( ( k  +  1 )  x.  T )  =  ( ( k  x.  T )  +  T
) )
187186oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T
)  +  T ) ) )
188187adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T )  +  T
) ) )
189188adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T
)  +  T ) ) )
19086recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
191190adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  x  e.  CC )
192130recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
193184ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  T  e.  CC )
194191, 192, 193addassd 9607 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
( x  +  ( k  x.  T ) )  +  T )  =  ( x  +  ( ( k  x.  T )  +  T
) ) )
195194eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( ( k  x.  T )  +  T ) )  =  ( ( x  +  ( k  x.  T ) )  +  T ) )
196195adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  x.  T )  +  T ) )  =  ( ( x  +  ( k  x.  T
) )  +  T
) )
197 oveq1 6277 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  (
( x  +  ( k  x.  T ) )  +  T )  =  ( A  +  T ) )
198197adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
x  +  ( k  x.  T ) )  +  T )  =  ( A  +  T
) )
1994recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  B  e.  CC )
2001recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  e.  CC )
201199, 200, 184subaddd 9940 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( B  -  A )  =  T  <-> 
( A  +  T
)  =  B ) )
20226, 201mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( A  +  T
)  =  B )
203202ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( A  +  T )  =  B )
204198, 203eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
x  +  ( k  x.  T ) )  +  T )  =  B )
205189, 196, 2043eqtrd 2499 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  B )
20698, 182, 2053eqtrd 2499 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  =  B )
207 fourierdlem51.bc . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  C )
208207ad3antrrr 727 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  B  e.  C )
209206, 208eqeltrd 2542 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  e.  C
)
2102093adantl3 1152 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  e.  C
)
211 simpl1 997 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  ( ph  /\  x  e.  RR ) )
212 simpl2 998 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  k  e.  ZZ )
213 fourierdlem51.css . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  C  C_  ( A [,] B ) )
214213sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
215214adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  ( k  x.  T ) )  e.  C )  -> 
( x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
2162153adant2 1013 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
217216adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
218 neqne 31677 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  ( x  +  ( k  x.  T ) )  =  A  -> 
( x  +  ( k  x.  T ) )  =/=  A )
219218adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  =/=  A )
2201adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  A  e.  RR )
221211, 220syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  A  e.  RR )
222211, 87syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  B  e.  RR )
223 simplr 753 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  x  e.  RR )
224223, 130readdcld 9612 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( k  x.  T ) )  e.  RR )
225224rexrd 9632 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( k  x.  T ) )  e.  RR* )
226211, 212, 225syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  RR* )
227221, 222, 226eliccelioc 31803 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
( x  +  ( k  x.  T ) )  e.  ( A (,] B )  <->  ( (
x  +  ( k  x.  T ) )  e.  ( A [,] B )  /\  (
x  +  ( k  x.  T ) )  =/=  A ) ) )
228217, 219, 227mpbir2and 920 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  ( A (,] B ) )
22997ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
2301ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  A  e.  RR )
2314ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  B  e.  RR )
23222ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  A  <  B )
233 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  x  e.  RR )
23492ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )
235 simplr 753 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  k  e.  ZZ )
23697, 113eqeltrrd 2543 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A (,] B
) )
237236ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A (,] B
) )
238 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( x  +  ( k  x.  T ) )  e.  ( A (,] B
) )
239230, 231, 232, 19, 233, 234, 235, 237, 238fourierdlem35 32166 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  k )
240239oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  =  ( k  x.  T ) )
241240oveq2d 6286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( x  +  ( k  x.  T ) ) )
242229, 241eqtrd 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( E `  x )  =  ( x  +  ( k  x.  T ) ) )
243211, 212, 228, 242syl21anc 1225 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  ( E `  x )  =  ( x  +  ( k  x.  T
) ) )
244 simpl3 999 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  C )
245243, 244eqeltrd 2542 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  ( E `  x )  e.  C )
246210, 245pm2.61dan 789 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  ( E `  x )  e.  C )
2472463exp 1193 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( k  e.  ZZ  ->  (
( x  +  ( k  x.  T ) )  e.  C  -> 
( E `  x
)  e.  C ) ) )
24878, 85, 247syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( k  e.  ZZ  ->  ( (
x  +  ( k  x.  T ) )  e.  C  ->  ( E `  x )  e.  C ) ) )
24976, 77, 248rexlimd 2938 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( E. k  e.  ZZ  (
x  +  ( k  x.  T ) )  e.  C  ->  ( E `  x )  e.  C ) )
25070, 249mpd 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( E `  x )  e.  C
)
25164, 250eqeltrd 2542 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
)  e.  C )
252 eqid 2454 . . . . . . . . . . . 12  |-  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  |->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
) )  =  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }  |->  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 x ) )
253251, 252fmptd 6031 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }  |->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
) ) : {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } --> C )
254 iocssre 11607 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
255102, 4, 254syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A (,] B
)  C_  RR )
256112, 255fssd 5722 . . . . . . . . . . . . . 14  |-  ( ph  ->  E : RR --> RR )
257 ssrab2 3571 . . . . . . . . . . . . . . 15  |-  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }  C_  ( ( A  +  X ) (,] ( B  +  X )
)
258257, 81syl5ss 3500 . . . . . . . . . . . . . 14  |-  ( ph  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  C_  RR )
259256, 258fssresd 5734 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) : { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
--> RR )
260259feqmptd 5901 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } )  =  ( x  e. 
{ y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  |->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
) ) )
261260feq1d 5699 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) : {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } --> C 
<->  ( x  e.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }  |->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  x
) ) : {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } --> C ) )
262253, 261mpbird 232 . . . . . . . . . 10  |-  ( ph  ->  ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) : { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
--> C )
263 simplll 757 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  ph )
264 id 22 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  w  e.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)
265 fourierdlem51.h . . . . . . . . . . . . . . . . 17  |-  H  =  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
266264, 265syl6eleqr 2553 . . . . . . . . . . . . . . . 16  |-  ( w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  w  e.  H
)
267266ad3antlr 728 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  w  e.  H )
268263, 267jca 530 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  ( ph  /\  w  e.  H
) )
269 id 22 . . . . . . . . . . . . . . . 16  |-  ( z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  z  e.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)
270269, 265syl6eleqr 2553 . . . . . . . . . . . . . . 15  |-  ( z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  z  e.  H
)
271270ad2antlr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  z  e.  H )
272 fvres 5862 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  =  ( E `
 z ) )
273272eqcomd 2462 . . . . . . . . . . . . . . . 16  |-  ( z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  ( E `  z )  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 z ) )
274273ad2antlr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  ( E `  z )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )
275 id 22 . . . . . . . . . . . . . . . . 17  |-  ( ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  ->  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
)  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )
276275eqcomd 2462 . . . . . . . . . . . . . . . 16  |-  ( ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  ->  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
) )
277276adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 z )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
) )
278 fvres 5862 . . . . . . . . . . . . . . . 16  |-  ( w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
)  =  ( E `
 w ) )
279278ad3antlr 728 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( E `  w
) )
280274, 277, 2793eqtrd 2499 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  ( E `  z )  =  ( E `  w ) )
2811ad3antrrr 727 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  A  e.  RR )
2824ad3antrrr 727 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  B  e.  RR )
28322ad3antrrr 727 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  A  <  B )
2842ad3antrrr 727 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  X  e.  RR )
285 simpllr 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  e.  H )
286 simplr 753 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  z  e.  H )
287 simpr 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( E `  z )  =  ( E `  w ) )
288281, 282, 283, 284, 265, 19, 31, 285, 286, 287fourierdlem19 32150 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  -.  w  <  z )
289287eqcomd 2462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( E `  w )  =  ( E `  z ) )
290281, 282, 283, 284, 265, 19, 31, 286, 285, 289fourierdlem19 32150 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  -.  z  <  w )
291265, 258syl5eqss 3533 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  C_  RR )
292291sselda 3489 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w  e.  H )  ->  w  e.  RR )
293292ad2antrr 723 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  e.  RR )
294291adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  w  e.  H )  ->  H  C_  RR )
295294sselda 3489 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  H )  /\  z  e.  H )  ->  z  e.  RR )
296295adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  z  e.  RR )
297293, 296lttri3d 9714 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( w  =  z  <->  ( -.  w  <  z  /\  -.  z  <  w ) ) )
298288, 290, 297mpbir2and 920 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  =  z )
299268, 271, 280, 298syl21anc 1225 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  (
( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) `
 w )  =  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
) )  ->  w  =  z )
300299ex 432 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  /\  z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  ->  (
( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
)  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  ->  w  =  z ) )
301300ralrimiva 2868 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  A. z  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ( ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
)  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  ->  w  =  z ) )
302301ralrimiva 2868 . . . . . . . . . 10  |-  ( ph  ->  A. w  e.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } A. z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }  (
( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
)  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  ->  w  =  z ) )
303 dff13 6141 . . . . . . . . . 10  |-  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) : {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } -1-1->
C  <->  ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) : {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } --> C  /\  A. w  e. 
{ y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } A. z  e.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } 
( ( ( E  |`  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  w
)  =  ( ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) `  z
)  ->  w  =  z ) ) )
304262, 302, 303sylanbrc 662 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) : { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } -1-1-> C )
305 f1fi 7799 . . . . . . . . 9  |-  ( ( C  e.  Fin  /\  ( E  |`  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } ) : { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } -1-1-> C )  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  e.  Fin )
30662, 304, 305syl2anc 659 . . . . . . . 8  |-  ( ph  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  e.  Fin )
307 unfi 7779 . . . . . . . 8  |-  ( ( { ( A  +  X ) }  e.  Fin  /\  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  e.  Fin )  ->  ( { ( A  +  X ) }  u.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  e.  Fin )
30861, 306, 307sylancr 661 . . . . . . 7  |-  ( ph  ->  ( { ( A  +  X ) }  u.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  e.  Fin )
309 simpl 455 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ph )
310 elrabi 3251 . . . . . . . . . . 11  |-  ( x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  x  e.  ( ( A  +  X
) [,] ( B  +  X ) ) )
311310adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )
31267elrab 3254 . . . . . . . . . . . 12  |-  ( x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } 
<->  ( x  e.  ( ( A  +  X
) [,] ( B  +  X ) )  /\  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
) )
313312simprbi 462 . . . . . . . . . . 11  |-  ( x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  E. k  e.  ZZ  ( x  +  (
k  x.  T ) )  e.  C )
314313adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
)
315 elsn 4030 . . . . . . . . . . . . 13  |-  ( x  e.  { ( A  +  X ) }  <-> 
x  =  ( A  +  X ) )
316 elun1 3657 . . . . . . . . . . . . 13  |-  ( x  e.  { ( A  +  X ) }  ->  x  e.  ( { ( A  +  X ) }  u.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
) )
317315, 316sylbir 213 . . . . . . . . . . . 12  |-  ( x  =  ( A  +  X )  ->  x  e.  ( { ( A  +  X ) }  u.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } ) )
318317adantl 464 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X
) ) )  /\  E. k  e.  ZZ  (
x  +  ( k  x.  T ) )  e.  C )  /\  x  =  ( A  +  X ) )  ->  x  e.  ( {
( A  +  X
) }  u.  {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
) )
31979ad2antrr 723 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  /\  -.  x  =  ( A  +  X ) )  -> 
( A  +  X
)  e.  RR* )
3205rexrd 9632 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  +  X
)  e.  RR* )
321320ad2antrr 723 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  /\  -.  x  =  ( A  +  X ) )  -> 
( B  +  X
)  e.  RR* )
3223, 5iccssred 31781 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  +  X ) [,] ( B  +  X )
)  C_  RR )
323322sselda 3489 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  ->  x  e.  RR )
324323rexrd 9632 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  ->  x  e.  RR* )
325324adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  /\  -.  x  =  ( A  +  X