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

Theorem fourierdlem51 37838
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 9670 . . . . . 6  |-  ( ph  ->  ( A  +  X
)  e.  RR )
4 fourierdlem51.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
54, 2readdcld 9670 . . . . . 6  |-  ( ph  ->  ( B  +  X
)  e.  RR )
6 0red 9644 . . . . . . . . 9  |-  ( ph  ->  0  e.  RR )
7 fourierdlem51.alt0 . . . . . . . . 9  |-  ( ph  ->  A  <  0 )
81, 6, 2, 7ltadd1dd 10224 . . . . . . . 8  |-  ( ph  ->  ( A  +  X
)  <  ( 0  +  X ) )
92recnd 9669 . . . . . . . . 9  |-  ( ph  ->  X  e.  CC )
109addid2d 9834 . . . . . . . 8  |-  ( ph  ->  ( 0  +  X
)  =  X )
118, 10breqtrd 4445 . . . . . . 7  |-  ( ph  ->  ( A  +  X
)  <  X )
123, 2, 11ltled 9783 . . . . . 6  |-  ( ph  ->  ( A  +  X
)  <_  X )
13 fourierdlem51.bgt0 . . . . . . . . 9  |-  ( ph  ->  0  <  B )
146, 4, 2, 13ltadd1dd 10224 . . . . . . . 8  |-  ( ph  ->  ( 0  +  X
)  <  ( B  +  X ) )
1510, 14eqbrtrrd 4443 . . . . . . 7  |-  ( ph  ->  X  <  ( B  +  X ) )
162, 5, 15ltled 9783 . . . . . 6  |-  ( ph  ->  X  <_  ( B  +  X ) )
173, 5, 2, 12, 16eliccd 37429 . . . . 5  |-  ( ph  ->  X  e.  ( ( A  +  X ) [,] ( B  +  X ) ) )
184, 2resubcld 10047 . . . . . . . 8  |-  ( ph  ->  ( B  -  X
)  e.  RR )
19 fourierdlem51.t . . . . . . . . 9  |-  T  =  ( B  -  A
)
204, 1resubcld 10047 . . . . . . . . 9  |-  ( ph  ->  ( B  -  A
)  e.  RR )
2119, 20syl5eqel 2514 . . . . . . . 8  |-  ( ph  ->  T  e.  RR )
221, 6, 4, 7, 13lttrd 9796 . . . . . . . . . . 11  |-  ( ph  ->  A  <  B )
231, 4posdifd 10200 . . . . . . . . . . 11  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
2422, 23mpbid 213 . . . . . . . . . 10  |-  ( ph  ->  0  <  ( B  -  A ) )
2519eqcomi 2435 . . . . . . . . . . 11  |-  ( B  -  A )  =  T
2625a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  =  T )
2724, 26breqtrd 4445 . . . . . . . . 9  |-  ( ph  ->  0  <  T )
2827gt0ne0d 10178 . . . . . . . 8  |-  ( ph  ->  T  =/=  0 )
2918, 21, 28redivcld 10435 . . . . . . 7  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
3029flcld 12033 . . . . . 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 23 . . . . . . . . . 10  |-  ( x  =  X  ->  x  =  X )
34 oveq2 6309 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
3534oveq1d 6316 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
3635fveq2d 5881 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
3736oveq1d 6316 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
3833, 37oveq12d 6319 . . . . . . . . 9  |-  ( x  =  X  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
3938adantl 467 . . . . . . . 8  |-  ( (
ph  /\  x  =  X )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
4030zred 11040 . . . . . . . . . 10  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
4140, 21remulcld 9671 . . . . . . . . 9  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
422, 41readdcld 9670 . . . . . . . 8  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  RR )
4332, 39, 2, 42fvmptd 5966 . . . . . . 7  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
44 fourierdlem51.exc . . . . . . 7  |-  ( ph  ->  ( E `  X
)  e.  C )
4543, 44eqeltrrd 2511 . . . . . 6  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  C )
46 oveq1 6308 . . . . . . . . 9  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
4746oveq2d 6317 . . . . . . . 8  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  ( X  +  ( k  x.  T ) )  =  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
4847eleq1d 2491 . . . . . . 7  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( X  +  ( k  x.  T ) )  e.  C  <->  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  C ) )
4948rspcev 3182 . . . . . 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 665 . . . . 5  |-  ( ph  ->  E. k  e.  ZZ  ( X  +  (
k  x.  T ) )  e.  C )
51 oveq1 6308 . . . . . . . 8  |-  ( y  =  X  ->  (
y  +  ( k  x.  T ) )  =  ( X  +  ( k  x.  T
) ) )
5251eleq1d 2491 . . . . . . 7  |-  ( y  =  X  ->  (
( y  +  ( k  x.  T ) )  e.  C  <->  ( X  +  ( k  x.  T ) )  e.  C ) )
5352rexbidv 2939 . . . . . 6  |-  ( y  =  X  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C  <->  E. k  e.  ZZ  ( X  +  ( k  x.  T
) )  e.  C
) )
5453elrab 3229 . . . . 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 668 . . . 4  |-  ( ph  ->  X  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } )
56 elun2 3634 . . . 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 17 . . 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 2521 . 2  |-  ( ph  ->  X  e.  D )
60 prfi 7848 . . . . . 6  |-  { ( A  +  X ) ,  ( B  +  X ) }  e.  Fin
61 snfi 7653 . . . . . . . 8  |-  { ( A  +  X ) }  e.  Fin
62 fourierdlem51.cfi . . . . . . . . 9  |-  ( ph  ->  C  e.  Fin )
63 fvres 5891 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  (
y  +  ( k  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
6665eleq1d 2491 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( y  +  ( k  x.  T ) )  e.  C  <->  ( x  +  ( k  x.  T ) )  e.  C ) )
6766rexbidv 2939 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C  <->  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
) )
6867elrab 3229 . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 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 1751 . . . . . . . . . . . . . . . 16  |-  F/ k
ph
72 nfre1 2886 . . . . . . . . . . . . . . . . . 18  |-  F/ k E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C
73 nfcv 2584 . . . . . . . . . . . . . . . . . 18  |-  F/_ k
( ( A  +  X ) (,] ( B  +  X )
)
7472, 73nfrab 3010 . . . . . . . . . . . . . . . . 17  |-  F/_ k { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
7574nfcri 2577 . . . . . . . . . . . . . . . 16  |-  F/ k  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }
7671, 75nfan 1984 . . . . . . . . . . . . . . 15  |-  F/ k ( ph  /\  x  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )
77 nfv 1751 . . . . . . . . . . . . . . 15  |-  F/ k ( E `  x
)  e.  C
78 simpl 458 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ph )
793rexrd 9690 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  +  X
)  e.  RR* )
80 iocssre 11714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  +  X
)  e.  RR*  /\  ( B  +  X )  e.  RR )  ->  (
( A  +  X
) (,] ( B  +  X ) ) 
C_  RR )
8179, 5, 80syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  +  X ) (,] ( B  +  X )
)  C_  RR )
8281adantr 466 . . . . . . . . . . . . . . . . 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 3226 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
874adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
8887, 86resubcld 10047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
8921adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
9028adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
9188, 89, 90redivcld 10435 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
9291flcld 12033 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
9392zred 11040 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
9493, 89remulcld 9671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
9586, 94readdcld 9670 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  RR )
9631fvmpt2 5969 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  RR )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
9786, 95, 96syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
9897ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
99 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ ) )
10092ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )
101 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  =  A )
1021rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A  e.  RR* )
1034rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  RR* )
1041, 4, 22ltled 9783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A  <_  B )
105 lbicc2 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
106102, 103, 104, 105syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A  e.  ( A [,] B ) )
107106adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  A  e.  ( A [,] B
) )
108101, 107eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
109108adant423 37225 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( k  x.  T ) )  e.  ( A [,] B
) )
11099, 100, 109jca31 536 . . . . . . . . . . . . . . . . . . . . . . . 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 11722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A (,] B )  C_  ( A [,] B )
1121, 4, 22, 19, 31fourierdlem4 37790 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  E : RR --> ( A (,] B ) )
113112ffvelrnda 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  e.  ( A (,] B
) )
114111, 113sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  e.  ( A [,] B
) )
11597, 114eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) )
116115ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) )
117102adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  A  e. 
RR* )
11887rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  B  e. 
RR* )
119 iocgtlb 37427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 x )  e.  ( A (,] B
) )  ->  A  <  ( E `  x
) )
120117, 118, 113, 119syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  A  < 
( E `  x
) )
121120ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  A  <  ( E `  x ) )
122 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  (
x  +  ( k  x.  T ) )  =  A )
123122eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  A  =  ( x  +  ( k  x.  T
) ) )
124123adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  A  =  ( x  +  (
k  x.  T ) ) )
125121, 124, 983brtr3d 4450 . . . . . . . . . . . . . . . . . . . . . . . . . 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 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ZZ  ->  k  e.  RR )
127126adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  RR )
12821adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  RR )
129127, 128remulcld 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  x.  T )  e.  RR )
130129adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
131130adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  x.  T )  e.  RR )
13294ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
133 simpllr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  x  e.  RR )
134131, 132, 133ltadd2d 9791 . . . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  x.  T )  <  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
136126ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  k  e.  RR )
13793ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  RR )
13821, 27elrpd 11338 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  RR+ )
139138ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  T  e.  RR+ )
140136, 137, 139ltmul1d 11379 . . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) )
142 fvex 5887 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( |_
`  ( ( B  -  x )  /  T ) )  e. 
_V
143 eleq1 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  e.  ZZ  <->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ ) )
144143anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  x.  T )  =  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )
147146oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
x  +  ( j  x.  T ) )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
148147eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( x  +  ( j  x.  T ) )  e.  ( A [,] B )  <->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) ) )
149145, 148anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
k  <  j  <->  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) ) )
151149, 150anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2426 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  =  ( k  +  1 )  <->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) ) )
153151, 152imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . 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 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  k  ->  (
i  e.  ZZ  <->  k  e.  ZZ ) )
155154anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  k  ->  (
( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ ) 
<->  ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ ) ) )
156155anbi1d 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  k  ->  (
i  x.  T )  =  ( k  x.  T ) )
158157oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  k  ->  (
x  +  ( i  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
159158eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  k  ->  (
( x  +  ( i  x.  T ) )  e.  ( A [,] B )  <->  ( x  +  ( k  x.  T ) )  e.  ( A [,] B
) ) )
160156, 159anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  =  k  ->  (
i  <  j  <->  k  <  j ) )
163161, 162anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  =  k  ->  (
i  +  1 )  =  ( k  +  1 ) )
165164eqeq2d 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  =  k  ->  (
j  =  ( i  +  1 )  <->  j  =  ( k  +  1 ) ) )
166163, 165imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . 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 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37792 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2068 . . . . . . . . . . . . . . . . . . . . . . . . 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 3133 . . . . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) )
181180oveq1d 6316 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  =  ( ( k  +  1 )  x.  T ) )
182181oveq2d 6317 . . . . . . . . . . . . . . . . . . . . 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 9669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  CC )
18421recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  CC )
185184adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  CC )
186183, 185adddirp1d 37349 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( ( k  +  1 )  x.  T )  =  ( ( k  x.  T )  +  T
) )
187186oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T
)  +  T ) ) )
188187adantlr 719 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T )  +  T
) ) )
189188adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T
)  +  T ) ) )
19086recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
191190adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  x  e.  CC )
192130recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
193184ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  T  e.  CC )
194191, 192, 193addassd 9665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
( x  +  ( k  x.  T ) )  +  T )  =  ( x  +  ( ( k  x.  T )  +  T
) ) )
195194eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( ( k  x.  T )  +  T ) )  =  ( ( x  +  ( k  x.  T ) )  +  T ) )
196195adantr 466 . . . . . . . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  (
( x  +  ( k  x.  T ) )  +  T )  =  ( A  +  T ) )
198197adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
x  +  ( k  x.  T ) )  +  T )  =  ( A  +  T
) )
1994recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  B  e.  CC )
2001recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  e.  CC )
201199, 200, 184subaddd 10004 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( B  -  A )  =  T  <-> 
( A  +  T
)  =  B ) )
20226, 201mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( A  +  T
)  =  B )
203202ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( A  +  T )  =  B )
204198, 203eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
x  +  ( k  x.  T ) )  +  T )  =  B )
205189, 196, 2043eqtrd 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  B )
20698, 182, 2053eqtrd 2467 . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  B  e.  C )
209206, 208eqeltrd 2510 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  e.  C
)
2102093adantl3 1163 . . . . . . . . . . . . . . . . . 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 1008 . . . . . . . . . . . . . . . . . . . 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 1009 . . . . . . . . . . . . . . . . . . . 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 3464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
215214adantlr 719 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  ( k  x.  T ) )  e.  C )  -> 
( x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
2162153adant2 1024 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
217216adantr 466 . . . . . . . . . . . . . . . . . . . . 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 37232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  ( x  +  ( k  x.  T ) )  =  A  -> 
( x  +  ( k  x.  T ) )  =/=  A )
219218adantl 467 . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  A  e.  RR )
221211, 220syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  A  e.  RR )
222211, 87syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  B  e.  RR )
223 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  x  e.  RR )
224223, 130readdcld 9670 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( k  x.  T ) )  e.  RR )
225224rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( k  x.  T ) )  e.  RR* )
226211, 212, 225syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 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 37450 . . . . . . . . . . . . . . . . . . . . 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 930 . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
2301ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  A  e.  RR )
2314ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  B  e.  RR )
23222ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  A  <  B )
233 simpllr 767 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  x  e.  RR )
23492ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )
235 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  k  e.  ZZ )
23697, 113eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A (,] B
) )
237236ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . . 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 37822 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  k )
240239oveq1d 6316 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  =  ( k  x.  T ) )
241240oveq2d 6317 . . . . . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . 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 1010 . . . . . . . . . . . . . . . . . . 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 2510 . . . . . . . . . . . . . . . . . 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 798 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  ( E `  x )  e.  C )
2472463exp 1204 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( k  e.  ZZ  ->  (
( x  +  ( k  x.  T ) )  e.  C  -> 
( E `  x
)  e.  C ) ) )
24878, 85, 247syl2anc 665 . . . . . . . . . . . . . . 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 2909 . . . . . . . . . . . . . 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 2510 . . . . . . . . . . . 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 2422 . . . . . . . . . . . 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 6057 . . . . . . . . . . 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 11714 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
255102, 4, 254syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A (,] B
)  C_  RR )
256112, 255fssd 5751 . . . . . . . . . . . . . 14  |-  ( ph  ->  E : RR --> RR )
257 ssrab2 3546 . . . . . . . . . . . . . . 15  |-  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }  C_  ( ( A  +  X ) (,] ( B  +  X )
)
258257, 81syl5ss 3475 . . . . . . . . . . . . . 14  |-  ( ph  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  C_  RR )
259256, 258fssresd 5763 . . . . . . . . . . . . 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 5930 . . . . . . . . . . . 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 5728 . . . . . . . . . . 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 235 . . . . . . . . . 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 766 . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . 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 2521 . . . . . . . . . . . . . . . 16  |-  ( w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  w  e.  H
)
267266ad3antlr 735 . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . 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 2521 . . . . . . . . . . . . . . 15  |-  ( z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  z  e.  H
)
271270ad2antlr 731 . . . . . . . . . . . . . 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 5891 . . . . . . . . . . . . . . . . 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 2430 . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . 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 2430 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 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 5891 . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  A  e.  RR )
2824ad3antrrr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  B  e.  RR )
28322ad3antrrr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  A  <  B )
2842ad3antrrr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  X  e.  RR )
285 simpllr 767 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  e.  H )
286 simplr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  z  e.  H )
287 simpr 462 . . . . . . . . . . . . . . . 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 37805 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  -.  w  <  z )
289287eqcomd 2430 . . . . . . . . . . . . . . . 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 37805 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  -.  z  <  w )
291265, 258syl5eqss 3508 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  C_  RR )
292291sselda 3464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w  e.  H )  ->  w  e.  RR )
293292ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  e.  RR )
294291adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  w  e.  H )  ->  H  C_  RR )
295294sselda 3464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  H )  /\  z  e.  H )  ->  z  e.  RR )
296295adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  z  e.  RR )
297293, 296lttri3d 9775 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( w  =  z  <->  ( -.  w  <  z  /\  -.  z  <  w ) ) )
298288, 290, 297mpbir2and 930 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  =  z )
299268, 271, 280, 298syl21anc 1263 . . . . . . . . . . . . 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 435 . . . . . . . . . . . 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 2839 . . . . . . . . . . 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 2839 . . . . . . . . . 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 6170 . . . . . . . . . 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 668 . . . . . . . . 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 7863 . . . . . . . . 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 665 . . . . . . . 8  |-  ( ph  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  e.  Fin )
307 unfi 7840 . . . . . . . 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 667 . . . . . . 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 458 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ph )
310 elrabi 3226 . . . . . . . . . . 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 467 . . . . . . . . . 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 3229 . . . . . . . . . . . 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 465 . . . . . . . . . . 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 467 . . . . . . . . . 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 4010 . . . . . . . . . . . . 13  |-  ( x  e.  { ( A  +  X ) }  <-> 
x  =  ( A  +  X ) )
316 elun1 3633 . . . . . . . . . . . . 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 216 . . . . . . . . . . . 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 467 . . . . . . . . . . 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 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  /\  -.  x  =  ( A  +  X ) )  -> 
( A  +  X
)  e.  RR* )
3205rexrd 9690 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  +  X
)  e.  RR* )
321320ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  /\  -.  x  =  ( A  +  X ) )  -> 
( B  +  X
)  e.  RR* )
3223, 5iccssred 37430 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  +  X ) [,] ( B  +  X )
)  C_  RR )
323322sselda 3464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  ->  x  e.  RR )
324323rexrd 9690 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  ->  x  e.  RR* )
325324adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( ( A  +  X ) [,] ( B  +  X )
) )  /\  -.  x  =  ( A  +  X )