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

Theorem fourierdlem51 31781
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 . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
2 fourierdlem51.x . . . . . . . 8  |-  ( ph  ->  X  e.  RR )
31, 2readdcld 9635 . . . . . . 7  |-  ( ph  ->  ( A  +  X
)  e.  RR )
4 fourierdlem51.b . . . . . . . 8  |-  ( ph  ->  B  e.  RR )
54, 2readdcld 9635 . . . . . . 7  |-  ( ph  ->  ( B  +  X
)  e.  RR )
6 0red 9609 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR )
7 fourierdlem51.alt0 . . . . . . . . . 10  |-  ( ph  ->  A  <  0 )
81, 6, 2, 7ltadd1dd 10175 . . . . . . . . 9  |-  ( ph  ->  ( A  +  X
)  <  ( 0  +  X ) )
92recnd 9634 . . . . . . . . . 10  |-  ( ph  ->  X  e.  CC )
109addid2d 9792 . . . . . . . . 9  |-  ( ph  ->  ( 0  +  X
)  =  X )
118, 10breqtrd 4477 . . . . . . . 8  |-  ( ph  ->  ( A  +  X
)  <  X )
123, 2, 11ltled 9744 . . . . . . 7  |-  ( ph  ->  ( A  +  X
)  <_  X )
1310eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  X  =  ( 0  +  X ) )
14 fourierdlem51.bgt0 . . . . . . . . . 10  |-  ( ph  ->  0  <  B )
156, 4, 2, 14ltadd1dd 10175 . . . . . . . . 9  |-  ( ph  ->  ( 0  +  X
)  <  ( B  +  X ) )
1613, 15eqbrtrd 4473 . . . . . . . 8  |-  ( ph  ->  X  <  ( B  +  X ) )
172, 5, 16ltled 9744 . . . . . . 7  |-  ( ph  ->  X  <_  ( B  +  X ) )
183, 5, 2, 12, 17eliccd 31425 . . . . . 6  |-  ( ph  ->  X  e.  ( ( A  +  X ) [,] ( B  +  X ) ) )
194, 2resubcld 9999 . . . . . . . . 9  |-  ( ph  ->  ( B  -  X
)  e.  RR )
20 fourierdlem51.t . . . . . . . . . 10  |-  T  =  ( B  -  A
)
214, 1resubcld 9999 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
2220, 21syl5eqel 2559 . . . . . . . . 9  |-  ( ph  ->  T  e.  RR )
231, 6, 4, 7, 14lttrd 9754 . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
241, 4posdifd 10151 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
2523, 24mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
2620eqcomi 2480 . . . . . . . . . . . 12  |-  ( B  -  A )  =  T
2726a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  A
)  =  T )
2825, 27breqtrd 4477 . . . . . . . . . 10  |-  ( ph  ->  0  <  T )
296, 28gtned 9731 . . . . . . . . 9  |-  ( ph  ->  T  =/=  0 )
3019, 22, 29redivcld 10384 . . . . . . . 8  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
3130flcld 11915 . . . . . . 7  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
32 fourierdlem51.e . . . . . . . . . . 11  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
3332a1i 11 . . . . . . . . . 10  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
34 id 22 . . . . . . . . . . . 12  |-  ( x  =  X  ->  x  =  X )
35 oveq2 6303 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
3635oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
3736fveq2d 5876 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
3837oveq1d 6310 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
3934, 38oveq12d 6313 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
4039adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  x  =  X )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) ) )
4131zred 10978 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
4241, 22remulcld 9636 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
432, 42readdcld 9635 . . . . . . . . . 10  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  RR )
4433, 40, 2, 43fvmptd 5962 . . . . . . . . 9  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
4544eqcomd 2475 . . . . . . . 8  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  =  ( E `
 X ) )
46 fourierdlem51.exc . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  e.  C )
4745, 46eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  C )
48 oveq1 6302 . . . . . . . . . 10  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
k  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
4948oveq2d 6311 . . . . . . . . 9  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  ( X  +  ( k  x.  T ) )  =  ( X  +  ( ( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) ) )
5049eleq1d 2536 . . . . . . . 8  |-  ( k  =  ( |_ `  ( ( B  -  X )  /  T
) )  ->  (
( X  +  ( k  x.  T ) )  e.  C  <->  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )  e.  C ) )
5150rspcev 3219 . . . . . . 7  |-  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ  /\  ( X  +  (
( |_ `  (
( B  -  X
)  /  T ) )  x.  T ) )  e.  C )  ->  E. k  e.  ZZ  ( X  +  (
k  x.  T ) )  e.  C )
5231, 47, 51syl2anc 661 . . . . . 6  |-  ( ph  ->  E. k  e.  ZZ  ( X  +  (
k  x.  T ) )  e.  C )
5318, 52jca 532 . . . . 5  |-  ( ph  ->  ( X  e.  ( ( A  +  X
) [,] ( B  +  X ) )  /\  E. k  e.  ZZ  ( X  +  ( k  x.  T
) )  e.  C
) )
54 oveq1 6302 . . . . . . . 8  |-  ( y  =  X  ->  (
y  +  ( k  x.  T ) )  =  ( X  +  ( k  x.  T
) ) )
5554eleq1d 2536 . . . . . . 7  |-  ( y  =  X  ->  (
( y  +  ( k  x.  T ) )  e.  C  <->  ( X  +  ( k  x.  T ) )  e.  C ) )
5655rexbidv 2978 . . . . . 6  |-  ( y  =  X  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C  <->  E. k  e.  ZZ  ( X  +  ( k  x.  T
) )  e.  C
) )
5756elrab 3266 . . . . 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
) )
5853, 57sylibr 212 . . . 4  |-  ( ph  ->  X  e.  { y  e.  ( ( A  +  X ) [,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C } )
59 elun2 3677 . . . 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 } ) )
6058, 59syl 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 } ) )
61 fourierdlem51.d . . . 4  |-  D  =  ( { ( A  +  X ) ,  ( B  +  X
) }  u.  {
y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)
6261eqcomi 2480 . . 3  |-  ( { ( A  +  X
) ,  ( B  +  X ) }  u.  { y  e.  ( ( A  +  X ) [,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )  =  D
6360, 62syl6eleq 2565 . 2  |-  ( ph  ->  X  e.  D )
64 prfi 7807 . . . . . . . 8  |-  { ( A  +  X ) ,  ( B  +  X ) }  e.  Fin
6564a1i 11 . . . . . . 7  |-  ( ph  ->  { ( A  +  X ) ,  ( B  +  X ) }  e.  Fin )
66 snfi 7608 . . . . . . . . . 10  |-  { ( A  +  X ) }  e.  Fin
6766a1i 11 . . . . . . . . 9  |-  ( ph  ->  { ( A  +  X ) }  e.  Fin )
68 fourierdlem51.cfi . . . . . . . . . 10  |-  ( ph  ->  C  e.  Fin )
69 fvres 5886 . . . . . . . . . . . . . . . 16  |-  ( 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 ) )
7069adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
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 ) )
71 oveq1 6302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  x  ->  (
y  +  ( k  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
7271eleq1d 2536 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  x  ->  (
( y  +  ( k  x.  T ) )  e.  C  <->  ( x  +  ( k  x.  T ) )  e.  C ) )
7372rexbidv 2978 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C  <->  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
) )
7473elrab 3266 . . . . . . . . . . . . . . . . . 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 ) )  /\  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  C
) )
7574simprbi 464 . . . . . . . . . . . . . . . . 17  |-  ( 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 )
7675adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
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
)
77 nfv 1683 . . . . . . . . . . . . . . . . . 18  |-  F/ k
ph
78 nfcv 2629 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k
x
79 nfre1 2928 . . . . . . . . . . . . . . . . . . . 20  |-  F/ k E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C
80 nfcv 2629 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ k
( ( A  +  X ) (,] ( B  +  X )
)
8179, 80nfrab 3048 . . . . . . . . . . . . . . . . . . 19  |-  F/_ k { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
8278, 81nfel 2642 . . . . . . . . . . . . . . . . . 18  |-  F/ k  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }
8377, 82nfan 1875 . . . . . . . . . . . . . . . . 17  |-  F/ k ( ph  /\  x  e.  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C } )
84 nfv 1683 . . . . . . . . . . . . . . . . 17  |-  F/ k ( E `  x
)  e.  C
85 simpl 457 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ph )
863rexrd 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A  +  X
)  e.  RR* )
87 iocssre 11616 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  +  X
)  e.  RR*  /\  ( B  +  X )  e.  RR )  ->  (
( A  +  X
) (,] ( B  +  X ) ) 
C_  RR )
8886, 5, 87syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( A  +  X ) (,] ( B  +  X )
)  C_  RR )
8988adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 )
9074simplbi 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  x  e.  ( ( A  +  X
) (,] ( B  +  X ) ) )
9190adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 )
) )
9289, 91sseldd 3510 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  x  e.  RR )
93 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
944adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  B  e.  RR )
9594, 93resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  ( B  -  x )  e.  RR )
9622adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
9729adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  T  =/=  0 )
9895, 96, 97redivcld 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( B  -  x )  /  T )  e.  RR )
9998flcld 11915 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  ZZ )
10099zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( |_
`  ( ( B  -  x )  /  T ) )  e.  RR )
101100, 96remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
10293, 101readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  RR )
10332fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )  e.  RR )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
10493, 102, 103syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  =  ( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
105104ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
106 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ ) )
10799ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )
108106, 107jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( |_ `  ( ( B  -  x )  /  T ) )  e.  ZZ ) )
109 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  =  A )
1101rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  A  e.  RR* )
1114rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  B  e.  RR* )
1121, 4, 23ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  A  <_  B )
113 lbicc2 11648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
114110, 111, 112, 113syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  A  e.  ( A [,] B ) )
115114adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  A  e.  ( A [,] B
) )
116109, 115eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
117116adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  ( k  x.  T ) )  =  A )  -> 
( x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
118117adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( k  x.  T ) )  e.  ( A [,] B
) )
119108, 118jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 ) ) )
120104eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( E `  x
) )
121 iocssicc 11624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A (,] B )  C_  ( A [,] B )
122121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( A (,] B )  C_  ( A [,] B ) )
1231, 4, 23, 20, 32fourierdlem4 31734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  E : RR --> ( A (,] B ) )
124123ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  e.  ( A (,] B
) )
125122, 124sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  ( E `
 x )  e.  ( A [,] B
) )
126120, 125eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) )
127126ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) )
128110adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  A  e. 
RR* )
12994rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  RR )  ->  B  e. 
RR* )
130 iocgtlb 31422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( E `
 x )  e.  ( A (,] B
) )  ->  A  <  ( E `  x
) )
131128, 129, 124, 130syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  RR )  ->  A  < 
( E `  x
) )
132131ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  A  <  ( E `  x ) )
133 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  (
x  +  ( k  x.  T ) )  =  A )
134133eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  A  =  ( x  +  ( k  x.  T
) ) )
135134adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  A  =  ( x  +  (
k  x.  T ) ) )
136135, 105breq12d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( A  <  ( E `  x
)  <->  ( x  +  ( k  x.  T
) )  <  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
137132, 136mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( k  x.  T ) )  < 
( x  +  ( ( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
138 zre 10880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  e.  ZZ  ->  k  e.  RR )
139138adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  RR )
14022adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  RR )
141139, 140remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  x.  T )  e.  RR )
142141adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  RR )
143106, 142syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  x.  T )  e.  RR )
144101ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  e.  RR )
14593adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  x  e.  RR )
146106, 145syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  x  e.  RR )
147143, 144, 146ltadd2d 9749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 ) ) ) )
148137, 147mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  x.  T )  <  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) )
149138ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  k  e.  RR )
150100ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  RR )
15122, 28elrpd 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  T  e.  RR+ )
152151adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR+ )
153152ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  T  e.  RR+ )
154149, 150, 153ltmul1d 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( k  <  ( |_ `  (
( B  -  x
)  /  T ) )  <->  ( k  x.  T )  <  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
155148, 154mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) )
156 fvex 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( |_
`  ( ( B  -  x )  /  T ) )  e. 
_V
157 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  e.  ZZ  <->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ ) )
158157anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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 ) ) )
159158anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) ) )
160 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  x.  T )  =  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )
161160oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
x  +  ( j  x.  T ) )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
162161eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
( x  +  ( j  x.  T ) )  e.  ( A [,] B )  <->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A [,] B
) ) )
163159, 162anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) ) )
164 breq2 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
k  <  j  <->  k  <  ( |_ `  ( ( B  -  x )  /  T ) ) ) )
165163, 164anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) ) )
166 eqeq1 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  ( |_ `  ( ( B  -  x )  /  T
) )  ->  (
j  =  ( k  +  1 )  <->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) ) )
167165, 166imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) )
168 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  =  k  ->  (
i  e.  ZZ  <->  k  e.  ZZ ) )
169168anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  =  k  ->  (
( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ ) 
<->  ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ ) ) )
170169anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  =  k  ->  (
( ( ( ph  /\  x  e.  RR )  /\  i  e.  ZZ )  /\  j  e.  ZZ ) 
<->  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  j  e.  ZZ ) ) )
171 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  =  k  ->  (
i  x.  T )  =  ( k  x.  T ) )
172171oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  =  k  ->  (
x  +  ( i  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
173172eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  =  k  ->  (
( x  +  ( i  x.  T ) )  e.  ( A [,] B )  <->  ( x  +  ( k  x.  T ) )  e.  ( A [,] B
) ) )
174170, 173anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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 ) ) ) )
175174anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) ) )
176 breq1 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  k  ->  (
i  <  j  <->  k  <  j ) )
177175, 176anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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
) ) )
178 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  k  ->  (
i  +  1 )  =  ( k  +  1 ) )
179178eqeq2d 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  k  ->  (
j  =  ( i  +  1 )  <->  j  =  ( k  +  1 ) ) )
180177, 179imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) )
181 simp-6l 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( 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 )
182181, 1syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
183181, 4syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
184181, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
18593ad5antr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
186 simp-5r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
187 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
188 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )
189 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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
) )
190 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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
) )
191182, 183, 184, 20, 185, 186, 187, 188, 189, 190fourierdlem6 31736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( 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 ) )
192180, 191chvarv 1983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( 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 ) )
193167, 192vtoclg 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( |_ `  ( ( B  -  x )  /  T ) )  e.  _V  ->  (
( ( ( ( ( ( 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 ) ) )
194156, 193ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( 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 ) )
195119, 127, 155, 194syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  ( k  +  1 ) )
196195oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  =  ( ( k  +  1 )  x.  T ) )
197196oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( x  +  ( ( k  +  1 )  x.  T ) ) )
198139recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  CC )
19922recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  T  e.  CC )
200199adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  ZZ )  ->  T  e.  CC )
201198, 200adddirp1d 31386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( ( k  +  1 )  x.  T )  =  ( ( k  x.  T )  +  T
) )
202201oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T
)  +  T ) ) )
203202adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T )  +  T
) ) )
204203adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  ( x  +  ( ( k  x.  T
)  +  T ) ) )
20593recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
206205adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  x  e.  CC )
207142recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
k  x.  T )  e.  CC )
208199adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
209208adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  T  e.  CC )
210206, 207, 209addassd 9630 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
( x  +  ( k  x.  T ) )  +  T )  =  ( x  +  ( ( k  x.  T )  +  T
) ) )
211210eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( ( k  x.  T )  +  T ) )  =  ( ( x  +  ( k  x.  T ) )  +  T ) )
212211adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  x.  T )  +  T ) )  =  ( ( x  +  ( k  x.  T
) )  +  T
) )
213 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  +  ( k  x.  T ) )  =  A  ->  (
( x  +  ( k  x.  T ) )  +  T )  =  ( A  +  T ) )
214213adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
x  +  ( k  x.  T ) )  +  T )  =  ( A  +  T
) )
2154recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  B  e.  CC )
2161recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A  e.  CC )
217215, 216, 199subaddd 9960 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( B  -  A )  =  T  <-> 
( A  +  T
)  =  B ) )
21827, 217mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  +  T
)  =  B )
219218ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( A  +  T )  =  B )
220214, 219eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( (
x  +  ( k  x.  T ) )  +  T )  =  B )
221204, 212, 2203eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( x  +  ( ( k  +  1 )  x.  T ) )  =  B )
222105, 197, 2213eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  =  B )
223 fourierdlem51.bc . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  C )
224223ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  B  e.  C )
225222, 224eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  e.  C
)
2262253adantl3 1154 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  ( x  +  ( k  x.  T
) )  =  A )  ->  ( E `  x )  e.  C
)
227 simpl1 999 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  ( ph  /\  x  e.  RR ) )
228 simpl2 1000 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  k  e.  ZZ )
229 fourierdlem51.css . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  C  C_  ( A [,] B ) )
230229sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
231230adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  ( k  x.  T ) )  e.  C )  -> 
( x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
2322313adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  ( A [,] B ) )
233232adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) )
234 neqne 31339 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  ( x  +  ( k  x.  T ) )  =  A  -> 
( x  +  ( k  x.  T ) )  =/=  A )
235234adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  =/=  A )
236233, 235jca 532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) )  =/=  A ) )
2371adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  RR )  ->  A  e.  RR )
238227, 237syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  A  e.  RR )
239227, 94syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  B  e.  RR )
240145, 142readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( k  x.  T ) )  e.  RR )
241240rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  ->  (
x  +  ( k  x.  T ) )  e.  RR* )
242227, 228, 241syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  RR* )
243238, 239, 242eliccelioc 31448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) ) )
244236, 243mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) )
245104ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( E `  x )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
246237ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  A  e.  RR )
24794ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  B  e.  RR )
24823ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  A  <  B )
249145adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  x  e.  RR )
25099ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  e.  ZZ )
251 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  k  e.  ZZ )
252120, 124eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A (,] B
) )
253252ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  e.  ( A (,] B
) )
254 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( x  +  ( k  x.  T ) )  e.  ( A (,] B
) )
255246, 247, 248, 20, 249, 250, 251, 253, 254fourierdlem35 31765 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( |_ `  ( ( B  -  x )  /  T
) )  =  k )
256255oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T )  =  ( k  x.  T ) )
257256oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( x  +  ( k  x.  T ) ) )
258245, 257eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ )  /\  ( x  +  ( k  x.  T
) )  e.  ( A (,] B ) )  ->  ( E `  x )  =  ( x  +  ( k  x.  T ) ) )
259227, 228, 244, 258syl21anc 1227 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  ( E `  x )  =  ( x  +  ( k  x.  T
) ) )
260 simp3 998 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  (
x  +  ( k  x.  T ) )  e.  C )
261260adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  (
x  +  ( k  x.  T ) )  e.  C )
262259, 261eqeltrd 2555 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  /\  -.  ( x  +  ( k  x.  T ) )  =  A )  ->  ( E `  x )  e.  C )
263226, 262pm2.61dan 789 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  RR )  /\  k  e.  ZZ  /\  ( x  +  ( k  x.  T ) )  e.  C )  ->  ( E `  x )  e.  C )
2642633exp 1195 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( k  e.  ZZ  ->  (
( x  +  ( k  x.  T ) )  e.  C  -> 
( E `  x
)  e.  C ) ) )
26585, 92, 264syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) ) )
26683, 84, 265rexlimd 2951 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) )
26776, 266mpd 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  ( E `  x )  e.  C
)
26870, 267eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( (
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 )
269 eqid 2467 . . . . . . . . . . . . . 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
) )  =  ( 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 ) )
270268, 269fmptd 6056 . . . . . . . . . . . . 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
) ) : {
y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C } --> C )
271 iocssre 11616 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
272110, 4, 271syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A (,] B
)  C_  RR )
273123, 272fssd 5746 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E : RR --> RR )
27490ssriv 3513 . . . . . . . . . . . . . . . . . 18  |-  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }  C_  ( ( A  +  X ) (,] ( B  +  X )
)
275274a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  C_  ( ( A  +  X ) (,] ( B  +  X
) ) )
276275, 88sstrd 3519 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  C_  RR )
277273, 276fssresd 5758 . . . . . . . . . . . . . . 15  |-  ( 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 )
278277feqmptd 5927 . . . . . . . . . . . . . 14  |-  ( 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
) ) )
279278feq1d 5723 . . . . . . . . . . . . 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 } --> 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 ) )
280270, 279mpbird 232 . . . . . . . . . . . 12  |-  ( 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 )
281 simplll 757 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
282 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 }
)
283 fourierdlem51.h . . . . . . . . . . . . . . . . . . . . . . 23  |-  H  =  { y  e.  ( ( A  +  X
) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }
284283eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  { y  e.  ( ( A  +  X ) (,] ( B  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  C }  =  H
285282, 284syl6eleq 2565 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  w  e.  H
)
286285adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }
)  ->  w  e.  H )
287286ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
288281, 287jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) )
289 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 }
)
290289, 284syl6eleq 2565 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  C }  ->  z  e.  H
)
291290ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
292288, 291jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )  /\  z  e.  H ) )
293 fvres 5886 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )
294293eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
295294ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) )
296 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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
) )
297296eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) )
298297adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) )
299 fvres 5886 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )
300299adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  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 ) )
301300ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) )
302295, 298, 3013eqtrd 2512 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) )
303292, 302jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) ) )
3041ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  A  e.  RR )
3054ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  B  e.  RR )
30623ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  A  <  B )
3072ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  X  e.  RR )
308 simpllr 758 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  e.  H )
309 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  z  e.  H )
310 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( E `  z )  =  ( E `  w ) )
311304, 305, 306, 307, 283, 20, 32, 308, 309, 310fourierdlem19 31749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  -.  w  <  z )
312310eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( E `  w )  =  ( E `  z ) )
313304, 305, 306, 307, 283, 20, 32, 309, 308, 312fourierdlem19 31749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  -.  z  <  w )
314311, 313jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( -.  w  <  z  /\  -.  z  <  w ) )
315283, 276syl5eqss 3553 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  H  C_  RR )
316315adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  H )  ->  H  C_  RR )
317 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  H )  ->  w  e.  H )
318316, 317sseldd 3510 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  w  e.  H )  ->  w  e.  RR )
319318ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  e.  RR )
320316sselda 3509 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  w  e.  H )  /\  z  e.  H )  ->  z  e.  RR )
321320adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  z  e.  RR )
322319, 321lttri3d 9736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  ( w  =  z  <->  ( -.  w  <  z  /\  -.  z  <  w ) ) )
323314, 322mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  H )  /\  z  e.  H
)  /\  ( E `  z )  =  ( E `  w ) )  ->  w  =  z )
324303, 323syl 16 . . . . . . . . . . . . . . 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  =  z )
325324ex 434 . . . . . . . . . . . . . 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
)  ->  w  =  z ) )
326325ralrimiva 2881 . . . . . . . . . . . . 13  |-  ( (
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 ) )
327326ralrimiva 2881 . . . . . . . . . . . 12  |-  ( 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 ) )
328280, 327jca 532 . . . . . . . . . . 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