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

Theorem fourierdlem48 31891
Description: The given periodic function  F has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem48.a  |-  ( ph  ->  A  e.  RR )
fourierdlem48.b  |-  ( ph  ->  B  e.  RR )
fourierdlem48.altb  |-  ( ph  ->  A  <  B )
fourierdlem48.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem48.t  |-  T  =  ( B  -  A
)
fourierdlem48.m  |-  ( ph  ->  M  e.  NN )
fourierdlem48.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem48.f  |-  ( ph  ->  F : D --> RR )
fourierdlem48.dper  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T
) )  e.  D
)
fourierdlem48.per  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( F `  ( x  +  (
k  x.  T ) ) )  =  ( F `  x ) )
fourierdlem48.cn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem48.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem48.x  |-  ( ph  ->  X  e.  RR )
fourierdlem48.z  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
fourierdlem48.e  |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )
fourierdlem48.ch  |-  ( ch  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i ) [,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ZZ )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )
Assertion
Ref Expression
fourierdlem48  |-  ( ph  ->  ( ( F  |`  ( X (,) +oo )
) lim CC  X )  =/=  (/) )
Distinct variable groups:    A, i, x    A, m, p, i    B, i, k, x    B, m, p    D, k, x   
i, E, k, y   
i, F, k, x, y    i, M, k   
m, M, p    y, M    Q, i, k, x    Q, p    y, Q    T, i, k, x, y    i, X, k, x, y    x, Z    ch, x    ph, i, k, x, y
Allowed substitution hints:    ph( m, p)    ch( y, i, k, m, p)    A( y, k)    B( y)    D( y, i, m, p)    P( x, y, i, k, m, p)    Q( m)    R( x, y, i, k, m, p)    T( m, p)    E( x, m, p)    F( m, p)    M( x)    X( m, p)    Z( y, i, k, m, p)

Proof of Theorem fourierdlem48
Dummy variables  j  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 457 . . 3  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ph )
2 0zd 10883 . . . . . 6  |-  ( ph  ->  0  e.  ZZ )
3 fourierdlem48.m . . . . . . 7  |-  ( ph  ->  M  e.  NN )
43nnzd 10975 . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
53nngt0d 10586 . . . . . 6  |-  ( ph  ->  0  <  M )
6 fzolb 11816 . . . . . 6  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
72, 4, 5, 6syl3anbrc 1181 . . . . 5  |-  ( ph  ->  0  e.  ( 0..^ M ) )
87adantr 465 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  0  e.  ( 0..^ M ) )
9 fourierdlem48.b . . . . . . . . . 10  |-  ( ph  ->  B  e.  RR )
10 fourierdlem48.x . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
119, 10resubcld 9994 . . . . . . . . 9  |-  ( ph  ->  ( B  -  X
)  e.  RR )
12 fourierdlem48.t . . . . . . . . . 10  |-  T  =  ( B  -  A
)
13 fourierdlem48.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
149, 13resubcld 9994 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
1512, 14syl5eqel 2535 . . . . . . . . 9  |-  ( ph  ->  T  e.  RR )
16 fourierdlem48.altb . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
1713, 9posdifd 10146 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
1816, 17mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
1918, 12syl6breqr 4477 . . . . . . . . . 10  |-  ( ph  ->  0  <  T )
2019gt0ne0d 10124 . . . . . . . . 9  |-  ( ph  ->  T  =/=  0 )
2111, 15, 20redivcld 10379 . . . . . . . 8  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
2221adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( B  -  X )  /  T )  e.  RR )
2322flcld 11917 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( |_ `  ( ( B  -  X )  /  T
) )  e.  ZZ )
24 1zzd 10902 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  1  e.  ZZ )
2523, 24zsubcld 10981 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  - 
1 )  e.  ZZ )
26 id 22 . . . . . . . 8  |-  ( ( E `  X )  =  B  ->  ( E `  X )  =  B )
2712a1i 11 . . . . . . . 8  |-  ( ( E `  X )  =  B  ->  T  =  ( B  -  A ) )
2826, 27oveq12d 6299 . . . . . . 7  |-  ( ( E `  X )  =  B  ->  (
( E `  X
)  -  T )  =  ( B  -  ( B  -  A
) ) )
299recnd 9625 . . . . . . . 8  |-  ( ph  ->  B  e.  CC )
3013recnd 9625 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3129, 30nncand 9941 . . . . . . 7  |-  ( ph  ->  ( B  -  ( B  -  A )
)  =  A )
3228, 31sylan9eqr 2506 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  A )
33 fourierdlem48.q . . . . . . . . . . . . . 14  |-  ( ph  ->  Q  e.  ( P `
 M ) )
34 fourierdlem48.p . . . . . . . . . . . . . . . 16  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
3534fourierdlem2 31845 . . . . . . . . . . . . . . 15  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
363, 35syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
3733, 36mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
3837simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
39 elmapi 7442 . . . . . . . . . . . 12  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
4038, 39syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
413nnnn0d 10859 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  NN0 )
42 nn0uz 11126 . . . . . . . . . . . . 13  |-  NN0  =  ( ZZ>= `  0 )
4341, 42syl6eleq 2541 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
44 eluzfz1 11704 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
4543, 44syl 16 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 ... M ) )
4640, 45ffvelrnd 6017 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  e.  RR )
4746rexrd 9646 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
48 1zzd 10902 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  ZZ )
492, 4, 483jca 1177 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )
)
50 0le1 10083 . . . . . . . . . . . . . 14  |-  0  <_  1
5150a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  1 )
523nnge1d 10585 . . . . . . . . . . . . 13  |-  ( ph  ->  1  <_  M )
5349, 51, 52jca32 535 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
54 elfz2 11690 . . . . . . . . . . . 12  |-  ( 1  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
5553, 54sylibr 212 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  ( 0 ... M ) )
5640, 55ffvelrnd 6017 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  1
)  e.  RR )
5756rexrd 9646 . . . . . . . . 9  |-  ( ph  ->  ( Q `  1
)  e.  RR* )
5813rexrd 9646 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR* )
5937simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
6059simplld 754 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  =  A )
6113leidd 10126 . . . . . . . . . 10  |-  ( ph  ->  A  <_  A )
6260, 61eqbrtrd 4457 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  <_  A )
6360eqcomd 2451 . . . . . . . . . 10  |-  ( ph  ->  A  =  ( Q `
 0 ) )
64 0re 9599 . . . . . . . . . . . . 13  |-  0  e.  RR
65 eleq1 2515 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
6665anbi2d 703 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
67 fveq2 5856 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
68 oveq1 6288 . . . . . . . . . . . . . . . . 17  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
6968fveq2d 5860 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
7067, 69breq12d 4450 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
7166, 70imbi12d 320 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) ) ) )
7237simprrd 758 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
7372r19.21bi 2812 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
7471, 73vtoclg 3153 . . . . . . . . . . . . 13  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
7564, 74ax-mp 5 . . . . . . . . . . . 12  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) )
767, 75mpdan 668 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
77 1e0p1 11014 . . . . . . . . . . . 12  |-  1  =  ( 0  +  1 )
7877fveq2i 5859 . . . . . . . . . . 11  |-  ( Q `
 1 )  =  ( Q `  (
0  +  1 ) )
7976, 78syl6breqr 4477 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
8063, 79eqbrtrd 4457 . . . . . . . . 9  |-  ( ph  ->  A  <  ( Q `
 1 ) )
8147, 57, 58, 62, 80elicod 31505 . . . . . . . 8  |-  ( ph  ->  A  e.  ( ( Q `  0 ) [,) ( Q ` 
1 ) ) )
8278oveq2i 6292 . . . . . . . 8  |-  ( ( Q `  0 ) [,) ( Q ` 
1 ) )  =  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) )
8381, 82syl6eleq 2541 . . . . . . 7  |-  ( ph  ->  A  e.  ( ( Q `  0 ) [,) ( Q `  ( 0  +  1 ) ) ) )
8483adantr 465 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  A  e.  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) ) )
8532, 84eqeltrd 2531 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  e.  ( ( Q `  0
) [,) ( Q `
 ( 0  +  1 ) ) ) )
86 fourierdlem48.e . . . . . . . . . . 11  |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x )
) )
8786a1i 11 . . . . . . . . . 10  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) ) )
88 id 22 . . . . . . . . . . . 12  |-  ( x  =  X  ->  x  =  X )
89 fveq2 5856 . . . . . . . . . . . 12  |-  ( x  =  X  ->  ( Z `  x )  =  ( Z `  X ) )
9088, 89oveq12d 6299 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
9190adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  x  =  X )  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
92 fourierdlem48.z . . . . . . . . . . . . . 14  |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) )
9392a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  Z  =  ( x  e.  RR  |->  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )
94 oveq2 6289 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
9594oveq1d 6296 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
9695fveq2d 5860 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
9796oveq1d 6296 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
9897adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  =  X )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
9921flcld 11917 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
10099zred 10976 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
101100, 15remulcld 9627 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
10293, 98, 10, 101fvmptd 5946 . . . . . . . . . . . 12  |-  ( ph  ->  ( Z `  X
)  =  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
103102, 101eqeltrd 2531 . . . . . . . . . . 11  |-  ( ph  ->  ( Z `  X
)  e.  RR )
10410, 103readdcld 9626 . . . . . . . . . 10  |-  ( ph  ->  ( X  +  ( Z `  X ) )  e.  RR )
10587, 91, 10, 104fvmptd 5946 . . . . . . . . 9  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( Z `  X ) ) )
106102oveq2d 6297 . . . . . . . . 9  |-  ( ph  ->  ( X  +  ( Z `  X ) )  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
107105, 106eqtrd 2484 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
108107oveq1d 6296 . . . . . . 7  |-  ( ph  ->  ( ( E `  X )  -  T
)  =  ( ( X  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  -  T ) )
10910recnd 9625 . . . . . . . 8  |-  ( ph  ->  X  e.  CC )
110101recnd 9625 . . . . . . . 8  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  CC )
11115recnd 9625 . . . . . . . 8  |-  ( ph  ->  T  e.  CC )
112109, 110, 111addsubassd 9956 . . . . . . 7  |-  ( ph  ->  ( ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  -  T
)  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  -  T ) ) )
11399zcnd 10977 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  CC )
114113, 111mulsubfacd 10023 . . . . . . . 8  |-  ( ph  ->  ( ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  -  T
)  =  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) )
115114oveq2d 6297 . . . . . . 7  |-  ( ph  ->  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  -  T ) )  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  -  1 )  x.  T ) ) )
116108, 112, 1153eqtrd 2488 . . . . . 6  |-  ( ph  ->  ( ( E `  X )  -  T
)  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  -  1 )  x.  T ) ) )
117116adantr 465 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( X  +  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) ) )
118 oveq1 6288 . . . . . . . . 9  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  (
k  x.  T )  =  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  -  1 )  x.  T ) )
119118oveq2d 6297 . . . . . . . 8  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  ( X  +  ( k  x.  T ) )  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T
) )  -  1 )  x.  T ) ) )
120119eqeq2d 2457 . . . . . . 7  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  (
( ( E `  X )  -  T
)  =  ( X  +  ( k  x.  T ) )  <->  ( ( E `  X )  -  T )  =  ( X  +  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) ) ) )
121120anbi2d 703 . . . . . 6  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  (
( ( ( E `
 X )  -  T )  e.  ( ( Q `  0
) [,) ( Q `
 ( 0  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) )  <->  ( ( ( E `  X )  -  T )  e.  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) )  /\  ( ( E `  X )  -  T )  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T
) )  -  1 )  x.  T ) ) ) ) )
122121rspcev 3196 . . . . 5  |-  ( ( ( ( |_ `  ( ( B  -  X )  /  T
) )  -  1 )  e.  ZZ  /\  ( ( ( E `
 X )  -  T )  e.  ( ( Q `  0
) [,) ( Q `
 ( 0  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) ) ) )  ->  E. k  e.  ZZ  ( ( ( E `  X )  -  T )  e.  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) )  /\  ( ( E `  X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )
12325, 85, 117, 122syl12anc 1227 . . . 4  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  E. k  e.  ZZ  ( ( ( E `  X )  -  T )  e.  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) )  /\  ( ( E `  X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )
12467, 69oveq12d 6299 . . . . . . . 8  |-  ( i  =  0  ->  (
( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 0 ) [,) ( Q `  (
0  +  1 ) ) ) )
125124eleq2d 2513 . . . . . . 7  |-  ( i  =  0  ->  (
( ( E `  X )  -  T
)  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  <->  ( ( E `  X )  -  T )  e.  ( ( Q `  0
) [,) ( Q `
 ( 0  +  1 ) ) ) ) )
126125anbi1d 704 . . . . . 6  |-  ( i  =  0  ->  (
( ( ( E `
 X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) )  <->  ( ( ( E `  X )  -  T )  e.  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) )  /\  ( ( E `  X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) ) )
127126rexbidv 2954 . . . . 5  |-  ( i  =  0  ->  ( E. k  e.  ZZ  ( ( ( E `
 X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) )  <->  E. k  e.  ZZ  ( ( ( E `
 X )  -  T )  e.  ( ( Q `  0
) [,) ( Q `
 ( 0  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) ) )
128127rspcev 3196 . . . 4  |-  ( ( 0  e.  ( 0..^ M )  /\  E. k  e.  ZZ  (
( ( E `  X )  -  T
)  e.  ( ( Q `  0 ) [,) ( Q `  ( 0  +  1 ) ) )  /\  ( ( E `  X )  -  T
)  =  ( X  +  ( k  x.  T ) ) ) )  ->  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( ( ( E `
 X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )
1298, 123, 128syl2anc 661 . . 3  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( ( ( E `
 X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )
130 ovex 6309 . . . 4  |-  ( ( E `  X )  -  T )  e. 
_V
131 eleq1 2515 . . . . . . . 8  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  <->  ( ( E `  X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) ) )
132 eqeq1 2447 . . . . . . . 8  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
y  =  ( X  +  ( k  x.  T ) )  <->  ( ( E `  X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )
133131, 132anbi12d 710 . . . . . . 7  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
( y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) )  <->  ( ( ( E `  X )  -  T )  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  ( ( E `  X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) ) )
1341332rexbidv 2961 . . . . . 6  |-  ( y  =  ( ( E `
 X )  -  T )  ->  ( E. i  e.  (
0..^ M ) E. k  e.  ZZ  (
y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) )  <->  E. i  e.  (
0..^ M ) E. k  e.  ZZ  (
( ( E `  X )  -  T
)  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  ( ( E `  X )  -  T
)  =  ( X  +  ( k  x.  T ) ) ) ) )
135134anbi2d 703 . . . . 5  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
( ph  /\  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  <->  ( ph  /\ 
E. i  e.  ( 0..^ M ) E. k  e.  ZZ  (
( ( E `  X )  -  T
)  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  ( ( E `  X )  -  T
)  =  ( X  +  ( k  x.  T ) ) ) ) ) )
136135imbi1d 317 . . . 4  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
( ( ph  /\  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  -> 
( ( F  |`  ( X (,) +oo )
) lim CC  X )  =/=  (/) )  <->  ( ( ph  /\  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( ( ( E `
 X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  ( ( E `
 X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )  ->  (
( F  |`  ( X (,) +oo ) ) lim
CC  X )  =/=  (/) ) ) )
137 simpr 461 . . . . 5  |-  ( (
ph  /\  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  ->  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )
138 nfv 1694 . . . . . . 7  |-  F/ i
ph
139 nfre1 2904 . . . . . . 7  |-  F/ i E. i  e.  ( 0..^ M ) E. k  e.  ZZ  (
y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) )
140138, 139nfan 1914 . . . . . 6  |-  F/ i ( ph  /\  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )
141 nfv 1694 . . . . . . 7  |-  F/ k
ph
142 nfcv 2605 . . . . . . . 8  |-  F/_ k
( 0..^ M )
143 nfre1 2904 . . . . . . . 8  |-  F/ k E. k  e.  ZZ  ( y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) )
144142, 143nfrex 2906 . . . . . . 7  |-  F/ k E. i  e.  ( 0..^ M ) E. k  e.  ZZ  (
y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) )
145141, 144nfan 1914 . . . . . 6  |-  F/ k ( ph  /\  E. i  e.  ( 0..^ M ) E. k  e.  ZZ  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )
146 simp1 997 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  ->  ph )
147 simp2l 1023 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  -> 
i  e.  ( 0..^ M ) )
148 simp3l 1025 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  -> 
y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )
149146, 147, 148jca31 534 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  -> 
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i ) [,) ( Q `  (
i  +  1 ) ) ) ) )
150 simp2r 1024 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  -> 
k  e.  ZZ )
151 simp3r 1026 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  -> 
y  =  ( X  +  ( k  x.  T ) ) )
152 fourierdlem48.ch . . . . . . . . . 10  |-  ( ch  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i ) [,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ZZ )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )
153152biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) )  /\  k  e.  ZZ )  /\  y  =  ( X  +  ( k  x.  T
) ) ) )
154153simplld 754 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i ) [,) ( Q `  (
i  +  1 ) ) ) ) )
155154simplld 754 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ph )
156 fourierdlem48.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : D --> RR )
157 frel 5724 . . . . . . . . . . . . . . . 16  |-  ( F : D --> RR  ->  Rel 
F )
158155, 156, 1573syl 20 . . . . . . . . . . . . . . 15  |-  ( ch 
->  Rel  F )
159 resindm 5308 . . . . . . . . . . . . . . . 16  |-  ( Rel 
F  ->  ( F  |`  ( ( X (,) +oo )  i^i  dom  F
) )  =  ( F  |`  ( X (,) +oo ) ) )
160159eqcomd 2451 . . . . . . . . . . . . . . 15  |-  ( Rel 
F  ->  ( F  |`  ( X (,) +oo ) )  =  ( F  |`  ( ( X (,) +oo )  i^i 
dom  F ) ) )
161158, 160syl 16 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F  |`  ( X (,) +oo ) )  =  ( F  |`  ( ( X (,) +oo )  i^i  dom  F
) ) )
162 fdm 5725 . . . . . . . . . . . . . . . . 17  |-  ( F : D --> RR  ->  dom 
F  =  D )
163155, 156, 1623syl 20 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  dom  F  =  D )
164163ineq2d 3685 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( X (,) +oo )  i^i  dom  F
)  =  ( ( X (,) +oo )  i^i  D ) )
165164reseq2d 5263 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F  |`  (
( X (,) +oo )  i^i  dom  F )
)  =  ( F  |`  ( ( X (,) +oo )  i^i  D ) ) )
166161, 165eqtrd 2484 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F  |`  ( X (,) +oo ) )  =  ( F  |`  ( ( X (,) +oo )  i^i  D ) ) )
167166oveq1d 6296 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( F  |`  ( X (,) +oo )
) lim CC  X )  =  ( ( F  |`  ( ( X (,) +oo )  i^i  D ) ) lim CC  X ) )
168155, 156syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  F : D --> RR )
169 ax-resscn 9552 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
170169a1i 11 . . . . . . . . . . . . . . 15  |-  ( ch 
->  RR  C_  CC )
171168, 170fssd 5730 . . . . . . . . . . . . . 14  |-  ( ch 
->  F : D --> CC )
172 inss2 3704 . . . . . . . . . . . . . . 15  |-  ( ( X (,) +oo )  i^i  D )  C_  D
173172a1i 11 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( X (,) +oo )  i^i  D ) 
C_  D )
174171, 173fssresd 5742 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F  |`  (
( X (,) +oo )  i^i  D ) ) : ( ( X (,) +oo )  i^i 
D ) --> CC )
175 pnfxr 11332 . . . . . . . . . . . . . . . 16  |- +oo  e.  RR*
176175a1i 11 . . . . . . . . . . . . . . 15  |-  ( ch 
-> +oo  e.  RR* )
177154simplrd 31380 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  i  e.  (
0..^ M ) )
17840adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
179 fzofzp1 11891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
180179adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
181178, 180ffvelrnd 6017 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
182155, 177, 181syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
183153simplrd 31380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  k  e.  ZZ )
184183zred 10976 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  k  e.  RR )
185155, 15syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  T  e.  RR )
186184, 185remulcld 9627 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( k  x.  T
)  e.  RR )
187182, 186resubcld 9994 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR )
188187rexrd 9646 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )
189187ltpnfd 31434 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  < +oo )
190188, 176, 189xrltled 31410 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  <_ +oo )
191 iooss2 11576 . . . . . . . . . . . . . . 15  |-  ( ( +oo  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  <_ +oo )  ->  ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  C_  ( X (,) +oo )
)
192176, 190, 191syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  ( X (,) +oo ) )
193183adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  k  e.  ZZ )
194193zcnd 10977 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  k  e.  CC )
195185recnd 9625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  T  e.  CC )
196195adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  T  e.  CC )
197194, 196mulneg1d 10016 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( -u k  x.  T )  =  -u ( k  x.  T ) )
198197oveq2d 6297 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  =  ( ( w  +  ( k  x.  T ) )  +  -u ( k  x.  T ) ) )
199 elioore 11570 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  w  e.  RR )
200199recnd 9625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  w  e.  CC )
201200adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  CC )
202194, 196mulcld 9619 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  CC )
203201, 202addcld 9618 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  CC )
204203, 202negsubd 9942 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  -u (
k  x.  T ) )  =  ( ( w  +  ( k  x.  T ) )  -  ( k  x.  T ) ) )
205201, 202pncand 9937 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  -  ( k  x.  T ) )  =  w )
206198, 204, 2053eqtrrd 2489 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
207155adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ph )
208154simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ph  /\  i  e.  ( 0..^ M ) ) )
209 fourierdlem48.cn . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
210 cncff 21375 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
211 fdm 5725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
212209, 210, 2113syl 20 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
213 ssdmres 5285 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  F  <->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
214212, 213sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
215156, 162syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  F  =  D )
216215adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  F  =  D )
217214, 216sseqtrd 3525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
218208, 217syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
219218adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  D )
220 elfzofz 11825 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
221220adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
222178, 221ffvelrnd 6017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
223155, 177, 222syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( Q `  i
)  e.  RR )
224223rexrd 9646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
225224adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  e.  RR* )
226182rexrd 9646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
227226adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
228199adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  RR )
229193zred 10976 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  k  e.  RR )
230207, 15syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  T  e.  RR )
231229, 230remulcld 9627 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  RR )
232228, 231readdcld 9626 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  RR )
233223adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  e.  RR )
234155, 10syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  X  e.  RR )
235234, 186readdcld 9626 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( X  +  ( k  x.  T ) )  e.  RR )
236235adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( X  +  ( k  x.  T ) )  e.  RR )
237152simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  y  =  ( X  +  ( k  x.  T ) ) )
238237eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( X  +  ( k  x.  T ) )  =  y )
239154simprd 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  y  e.  (
( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) )
240238, 239eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( X  +  ( k  x.  T ) )  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )
241 icogelb 31496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  ( X  +  ( k  x.  T ) )  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <_  ( X  +  ( k  x.  T ) ) )
242224, 226, 240, 241syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( Q `  i
)  <_  ( X  +  ( k  x.  T ) ) )
243242adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  <_  ( X  +  ( k  x.  T ) ) )
244207, 10syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  e.  RR )
245244rexrd 9646 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  e.  RR* )
246182adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
247246, 231resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR )
248247rexrd 9646 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR* )
249 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
250 ioogtlb 31482 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR*  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  <  w )
251245, 248, 249, 250syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  <  w )
252244, 228, 231, 251ltadd1dd 10170 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( X  +  ( k  x.  T ) )  < 
( w  +  ( k  x.  T ) ) )
253233, 236, 232, 243, 252lelttrd 9743 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  <  ( w  +  ( k  x.  T ) ) )
254 iooltub 31502 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR*  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  <  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )
255245, 248, 249, 254syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  <  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )
256228, 247, 231, 255ltadd1dd 10170 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  <  ( ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) )  +  ( k  x.  T
) ) )
257182recnd 9625 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  CC )
258186recnd 9625 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( k  x.  T
)  e.  CC )
259257, 258npcand 9940 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) )  +  ( k  x.  T ) )  =  ( Q `
 ( i  +  1 ) ) )
260259adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  +  ( k  x.  T ) )  =  ( Q `  ( i  +  1 ) ) )
261256, 260breqtrd 4461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  <  ( Q `  ( i  +  1 ) ) )
262225, 227, 232, 253, 261eliood 31485 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
263219, 262sseldd 3490 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  D )
264193znegcld 10978 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  -u k  e.  ZZ )
265 ovex 6309 . . . . . . . . . . . . . . . . . . 19  |-  ( w  +  ( k  x.  T ) )  e. 
_V
266 eleq1 2515 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
x  e.  D  <->  ( w  +  ( k  x.  T ) )  e.  D ) )
2672663anbi2d 1305 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( ph  /\  x  e.  D  /\  -u k  e.  ZZ )  <->  ( ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  -u k  e.  ZZ ) ) )
268 oveq1 6288 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
x  +  ( -u k  x.  T )
)  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
269268eleq1d 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( x  +  (
-u k  x.  T
) )  e.  D  <->  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D ) )
270267, 269imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( ( ph  /\  x  e.  D  /\  -u k  e.  ZZ )  ->  ( x  +  ( -u k  x.  T
) )  e.  D
)  <->  ( ( ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  -u k  e.  ZZ )  ->  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) )  e.  D ) ) )
271 negex 9823 . . . . . . . . . . . . . . . . . . . 20  |-  -u k  e.  _V
272 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  -u k  ->  (
j  e.  ZZ  <->  -u k  e.  ZZ ) )
2732723anbi3d 1306 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  -u k  ->  (
( ph  /\  x  e.  D  /\  j  e.  ZZ )  <->  ( ph  /\  x  e.  D  /\  -u k  e.  ZZ ) ) )
274 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  -u k  ->  (
j  x.  T )  =  ( -u k  x.  T ) )
275274oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  -u k  ->  (
x  +  ( j  x.  T ) )  =  ( x  +  ( -u k  x.  T
) ) )
276275eleq1d 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  -u k  ->  (
( x  +  ( j  x.  T ) )  e.  D  <->  ( x  +  ( -u k  x.  T ) )  e.  D ) )
277273, 276imbi12d 320 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  -u k  ->  (
( ( ph  /\  x  e.  D  /\  j  e.  ZZ )  ->  ( x  +  ( j  x.  T ) )  e.  D )  <-> 
( ( ph  /\  x  e.  D  /\  -u k  e.  ZZ )  ->  ( x  +  ( -u k  x.  T
) )  e.  D
) ) )
278 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
k  e.  ZZ  <->  j  e.  ZZ ) )
2792783anbi3d 1306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( ph  /\  x  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  x  e.  D  /\  j  e.  ZZ )
) )
280 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
281280oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
x  +  ( k  x.  T ) )  =  ( x  +  ( j  x.  T
) ) )
282281eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( x  +  ( k  x.  T ) )  e.  D  <->  ( x  +  ( j  x.  T ) )  e.  D ) )
283279, 282imbi12d 320 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
( ( ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T ) )  e.  D )  <-> 
( ( ph  /\  x  e.  D  /\  j  e.  ZZ )  ->  ( x  +  ( j  x.  T ) )  e.  D ) ) )
284 fourierdlem48.dper . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T
) )  e.  D
)
285283, 284chvarv 2000 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  D  /\  j  e.  ZZ )  ->  ( x  +  ( j  x.  T
) )  e.  D
)
286271, 277, 285vtocl 3147 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  D  /\  -u k  e.  ZZ )  ->  ( x  +  ( -u k  x.  T
) )  e.  D
)
287265, 270, 286vtocl 3147 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  -u k  e.  ZZ )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D )
288207, 263, 264, 287syl3anc 1229 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D )
289206, 288eqeltrd 2531 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  D )
290289ralrimiva 2857 . . . . . . . . . . . . . . 15  |-  ( ch 
->  A. w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) w  e.  D )
291 dfss3 3479 . . . . . . . . . . . . . . 15  |-  ( ( X (,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) 
C_  D  <->  A. w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) w  e.  D
)
292290, 291sylibr 212 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  D )
293192, 292ssind 3707 . . . . . . . . . . . . 13  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  ( ( X (,) +oo )  i^i 
D ) )
294 ioosscn 31481 . . . . . . . . . . . . . 14  |-  ( X (,) +oo )  C_  CC
295 ssinss1 3711 . . . . . . . . . . . . . 14  |-  ( ( X (,) +oo )  C_  CC  ->  ( ( X (,) +oo )  i^i 
D )  C_  CC )
296294, 295mp1i 12 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( X (,) +oo )  i^i  D ) 
C_  CC )
297 eqid 2443 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
298 eqid 2443 . . . . . . . . . . . . 13  |-  ( (
TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  =  ( ( TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i  D )  u.  { X } ) )
299234rexrd 9646 . . . . . . . . . . . . . . 15  |-  ( ch 
->  X  e.  RR* )
300234leidd 10126 . . . . . . . . . . . . . . 15  |-  ( ch 
->  X  <_  X )
301237oveq1d 6296 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( y  -  (
k  x.  T ) )  =  ( ( X  +  ( k  x.  T ) )  -  ( k  x.  T ) ) )
302234recnd 9625 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  X  e.  CC )
303302, 258pncand 9937 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( X  +  ( k  x.  T
) )  -  (
k  x.  T ) )  =  X )
304301, 303eqtr2d 2485 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  X  =  (
y  -  ( k  x.  T ) ) )
305 icossre 11616 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) 
C_  RR )
306223, 226, 305syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  C_  RR )
307306, 239sseldd 3490 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  y  e.  RR )
308 icoltub 31499 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )  ->  y  <  ( Q `  (
i  +  1 ) ) )
309224, 226, 239, 308syl3anc 1229 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  y  <  ( Q `
 ( i  +  1 ) ) )
310307, 182, 186, 309ltsub1dd 10171 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( y  -  (
k  x.  T ) )  <  ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) )
311304, 310eqbrtrd 4457 . . . . . . . . . . . . . . 15  |-  ( ch 
->  X  <  ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) )
312299, 188, 299, 300, 311elicod 31505 . . . . . . . . . . . . . 14  |-  ( ch 
->  X  e.  ( X [,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) ) )
313 snunioo1 31506 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR*  /\  X  < 
( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  (
( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  u.  { X } )  =  ( X [,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) )
314299, 188, 311, 313syl3anc 1229 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  u.  { X } )  =  ( X [,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) )
315314fveq2d 5860 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( int `  (
( TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i  D )  u.  { X } ) ) ) `
 ( ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  u. 
{ X } ) )  =  ( ( int `  ( (
TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) ) ) `
 ( X [,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) ) ) )
316297cnfldtop 21269 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  Top
317 ovex 6309 . . . . . . . . . . . . . . . . . . . 20  |-  ( X (,) +oo )  e. 
_V
318317inex1 4578 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X (,) +oo )  i^i  D )  e.  _V
319 snex 4678 . . . . . . . . . . . . . . . . . . 19  |-  { X }  e.  _V
320318, 319unex 6583 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } )  e.  _V
321 resttop 19639 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } )  e.  _V )  ->  ( ( TopOpen ` fld )t  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  e.  Top )
322316, 320, 321mp2an 672 . . . . . . . . . . . . . . . . 17  |-  ( (
TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  e. 
Top
323322a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i  D )  u.  { X } ) )  e. 
Top )
324 retop 21246 . . . . . . . . . . . . . . . . . . 19  |-  ( topGen ` 
ran  (,) )  e.  Top
325324a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( topGen `  ran  (,) )  e.  Top )
326320a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } )  e.  _V )
327 iooretop 21251 . . . . . . . . . . . . . . . . . . 19  |-  ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  e.  (
topGen `  ran  (,) )
328327a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( -oo (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  e.  ( topGen ` 
ran  (,) ) )
329 elrestr 14808 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } )  e.  _V  /\  ( -oo (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  e.  ( topGen `  ran  (,) )
)  ->  ( ( -oo (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  i^i  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  e.  ( ( topGen `  ran  (,) )t  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) ) )
330325, 326, 328, 329syl3anc 1229 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  e.  ( ( topGen `  ran  (,) )t  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )
331 mnfxr 11334 . . . . . . . . . . . . . . . . . . . . . 22  |- -oo  e.  RR*
332331a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  -> -oo  e.  RR* )
333188adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR* )
334 icossre 11616 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  e.  RR  /\  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )  ->  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  RR )
335234, 188, 334syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  RR )
336335sselda 3489 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  RR )
337336mnfltd 31445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  -> -oo  <  x )
338299adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  e.  RR* )
339 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
340 icoltub 31499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR*  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  <  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )
341338, 333, 339, 340syl3anc 1229 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  <  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )
342332, 333, 336, 337, 341eliood 31485 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( -oo (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
343 ssnid 4043 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  x  e. 
{ x }
344343a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  X  ->  x  e.  { x } )
345 sneq 4024 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  X  ->  { x }  =  { X } )
346344, 345eleqtrd 2533 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  X  ->  x  e.  { X } )
347 elun2 3657 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  { X }  ->  x  e.  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } ) )
348346, 347syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  X  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
349348adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  x  =  X )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
350299ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  e.  RR* )
351175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  -> +oo  e.  RR* )
352336adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  RR )
353234ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  e.  RR )
354 icogelb 31496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( X  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR*  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  <_  x )
355338, 333, 339, 354syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  <_  x )
356355adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  <_  x )
357 neqne 31388 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  x  =  X  ->  x  =/=  X )
358357adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  =/=  X )
359353, 352, 356, 358leneltd 31448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  <  x )
360352ltpnfd 31434 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  < +oo )
361350, 351, 352, 359, 360eliood 31485 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( X (,) +oo ) )
362183zcnd 10977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ch 
->  k  e.  CC )
363362, 195mulneg1d 10016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ch 
->  ( -u k  x.  T )  =  -u ( k  x.  T
) )
364363oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ch 
->  ( ( w  +  ( k  x.  T
) )  +  (
-u k  x.  T
) )  =  ( ( w  +  ( k  x.  T ) )  +  -u (
k  x.  T ) ) )
365364adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  =  ( ( w  +  ( k  x.  T ) )  +  -u ( k  x.  T ) ) )
366 ioosscn 31481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  C_  CC
367366sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  w  e.  CC )
368367adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  CC )
369258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  CC )
370368, 369addcld 9618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  CC )
371370, 369negsubd 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  -u (
k  x.  T ) )  =  ( ( w  +  ( k  x.  T ) )  -  ( k  x.  T ) ) )
372368, 369pncand 9937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  -  ( k  x.  T ) )  =  w )
373365, 371, 3723eqtrrd 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
374186adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  RR )
375228, 374readdcld 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  RR )
376225, 227, 375, 253, 261eliood 31485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
377219, 376sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  D )
3782723anbi3d 1306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  -u k  ->  (
( ph  /\  (
w  +  ( k  x.  T ) )  e.  D  /\  j  e.  ZZ )  <->  ( ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  -u k  e.  ZZ ) ) )
379274oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  -u k  ->  (
( w  +  ( k  x.  T ) )  +  ( j  x.  T ) )  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
380379eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  -u k  ->  (
( ( w  +  ( k  x.  T
) )  +  ( j  x.  T ) )  e.  D  <->  ( (
w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) )  e.  D ) )
381378, 380imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  -u k  ->  (
( ( ph  /\  ( w  +  (
k  x.  T ) )  e.  D  /\  j  e.  ZZ )  ->  ( ( w  +  ( k  x.  T
) )  +  ( j  x.  T ) )  e.  D )  <-> 
( ( ph  /\  ( w  +  (
k  x.  T ) )  e.  D  /\  -u k  e.  ZZ )  ->  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) )  e.  D ) ) )
3822663anbi2d 1305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( ph  /\  x  e.  D  /\  j  e.  ZZ )  <->  ( ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  j  e.  ZZ )
) )
383 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
x  +  ( j  x.  T ) )  =  ( ( w  +  ( k  x.  T ) )  +  ( j  x.  T
) ) )
384383eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( x  +  ( j  x.  T ) )  e.  D  <->  ( (
w  +  ( k  x.  T ) )  +  ( j  x.  T ) )  e.  D ) )
385382, 384imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( ( ph  /\  x  e.  D  /\  j  e.  ZZ )  ->  ( x  +  ( j  x.  T ) )  e.  D )  <-> 
( ( ph  /\  ( w  +  (
k  x.  T ) )  e.  D  /\  j  e.  ZZ )  ->  ( ( w  +  ( k  x.  T
) )  +  ( j  x.  T ) )  e.  D ) ) )
386265, 385, 285vtocl 3147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  j  e.  ZZ )  ->  (
( w  +  ( k  x.  T ) )  +  ( j  x.  T ) )  e.  D )
387271, 381, 386vtocl 3147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  -u k  e.  ZZ )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D )
388207, 377, 264, 387syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D )
389373, 388eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  D )
390389ralrimiva 2857 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  A. w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) w  e.  D )
391390, 291sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  D )
392391ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  D )
393188ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )
394341adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  <  ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) )
395350, 393, 352, 359, 394eliood 31485 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) ) )
396392, 395sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  D )
397361, 396elind 3673 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( ( X (,) +oo )  i^i  D ) )
398 elun1 3656 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( X (,) +oo )  i^i 
D )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
399397, 398syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } ) )
400349, 399pm2.61dan 791 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
401342, 400elind 3673 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )
402299adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )  ->  X  e.  RR* )
403188adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )  -> 
( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )
404 elinel1 31378 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  ->  x  e.  ( -oo (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
405 elioore 11570 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  x  e.  RR )
406404, 405syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  ->  x  e.  RR )
407406rexrd 9646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  ->  x  e.  RR* )
408407adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )  ->  x  e.  RR* )
409 elinel2 31377 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
410234adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  =  X )  ->  X  e.  RR )
41188eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  X  ->  X  =  x )
412411adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  =  X )  ->  X  =  x )
413410, 412eqled 31408 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  x  =  X )  ->  X  <_  x )
414413adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  x  =  X )  ->  X  <_  x )
415 simpll 753 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  ch )
416 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
417 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  x  =  X  ->  -.  x  =  X
)
418 elsn 4028 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  { X }  <->  x  =  X )
419417, 418sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  x  =  X  ->  -.  x  e.  { X } )
420419adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  -.  x  e.  { X } )
421 elunnel2 31369 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } )  /\  -.  x  e. 
{ X } )  ->  x  e.  ( ( X (,) +oo )  i^i  D ) )
422416, 420, 421syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  x  e.  ( ( X (,) +oo )  i^i  D ) )
423 elinel1 31378 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( ( X (,) +oo )  i^i 
D )  ->  x  e.  ( X (,) +oo ) )
424422, 423syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  x  e.  ( X (,) +oo )
)
425234adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  e.  RR )
426 elioore 11570 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( X (,) +oo )  ->  x  e.  RR )
427426adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  x  e.  RR )
428299adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  e.  RR* )
429175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  -> +oo  e.  RR* )
430 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  x  e.  ( X (,) +oo ) )
431 ioogtlb 31482 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( X  e.  RR*  /\ +oo  e.  RR*  /\  x  e.  ( X (,) +oo ) )  ->  X  <  x )
432428, 429, 430, 431syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  <  x )
433425, 427, 432ltled 9736 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  <_  x )
434415, 424, 433syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  X  <_  x )
435414, 434pm2.61dan 791 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  ->  X  <_  x )
436409, 435sylan2 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )  ->  X  <_  x )
437331a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  x  e.  ( -oo (,) (
( Q `  (
i  +  1 ) )  -  ( k