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

Theorem fourierdlem48 37837
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 458 . . 3  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ph )
2 0zd 10949 . . . . . 6  |-  ( ph  ->  0  e.  ZZ )
3 fourierdlem48.m . . . . . . 7  |-  ( ph  ->  M  e.  NN )
43nnzd 11039 . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
53nngt0d 10653 . . . . . 6  |-  ( ph  ->  0  <  M )
6 fzolb 11926 . . . . . 6  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
72, 4, 5, 6syl3anbrc 1189 . . . . 5  |-  ( ph  ->  0  e.  ( 0..^ M ) )
87adantr 466 . . . 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 10047 . . . . . . . . 9  |-  ( ph  ->  ( B  -  X
)  e.  RR )
12 fourierdlem48.t . . . . . . . . . 10  |-  T  =  ( B  -  A
)
13 fourierdlem48.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
149, 13resubcld 10047 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
1512, 14syl5eqel 2514 . . . . . . . . 9  |-  ( ph  ->  T  e.  RR )
16 fourierdlem48.altb . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
1713, 9posdifd 10200 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
1816, 17mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
1918, 12syl6breqr 4461 . . . . . . . . . 10  |-  ( ph  ->  0  <  T )
2019gt0ne0d 10178 . . . . . . . . 9  |-  ( ph  ->  T  =/=  0 )
2111, 15, 20redivcld 10435 . . . . . . . 8  |-  ( ph  ->  ( ( B  -  X )  /  T
)  e.  RR )
2221adantr 466 . . . . . . 7  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( B  -  X )  /  T )  e.  RR )
2322flcld 12033 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( |_ `  ( ( B  -  X )  /  T
) )  e.  ZZ )
24 1zzd 10968 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  1  e.  ZZ )
2523, 24zsubcld 11045 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( |_ `  ( ( B  -  X )  /  T ) )  - 
1 )  e.  ZZ )
26 id 23 . . . . . . . 8  |-  ( ( E `  X )  =  B  ->  ( E `  X )  =  B )
2712a1i 11 . . . . . . . 8  |-  ( ( E `  X )  =  B  ->  T  =  ( B  -  A ) )
2826, 27oveq12d 6319 . . . . . . 7  |-  ( ( E `  X )  =  B  ->  (
( E `  X
)  -  T )  =  ( B  -  ( B  -  A
) ) )
299recnd 9669 . . . . . . . 8  |-  ( ph  ->  B  e.  CC )
3013recnd 9669 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3129, 30nncand 9991 . . . . . . 7  |-  ( ph  ->  ( B  -  ( B  -  A )
)  =  A )
3228, 31sylan9eqr 2485 . . . . . 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 37790 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . 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 460 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
39 elmapi 7497 . . . . . . . . . . . 12  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
4038, 39syl 17 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
413nnnn0d 10925 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  NN0 )
42 nn0uz 11193 . . . . . . . . . . . . 13  |-  NN0  =  ( ZZ>= `  0 )
4341, 42syl6eleq 2520 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
44 eluzfz1 11806 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
4543, 44syl 17 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 ... M ) )
4640, 45ffvelrnd 6034 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  e.  RR )
4746rexrd 9690 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  e.  RR* )
48 1zzd 10968 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  ZZ )
492, 4, 483jca 1185 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )
)
50 0le1 10137 . . . . . . . . . . . . . 14  |-  0  <_  1
5150a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  1 )
523nnge1d 10652 . . . . . . . . . . . . 13  |-  ( ph  ->  1  <_  M )
5349, 51, 52jca32 537 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
54 elfz2 11791 . . . . . . . . . . . 12  |-  ( 1  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  1  e.  ZZ )  /\  (
0  <_  1  /\  1  <_  M ) ) )
5553, 54sylibr 215 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  ( 0 ... M ) )
5640, 55ffvelrnd 6034 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  1
)  e.  RR )
5756rexrd 9690 . . . . . . . . 9  |-  ( ph  ->  ( Q `  1
)  e.  RR* )
5813rexrd 9690 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR* )
5937simprd 464 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
6059simplld 759 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  =  A )
6113leidd 10180 . . . . . . . . . 10  |-  ( ph  ->  A  <_  A )
6260, 61eqbrtrd 4441 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  <_  A )
6360eqcomd 2430 . . . . . . . . . 10  |-  ( ph  ->  A  =  ( Q `
 0 ) )
64 0re 9643 . . . . . . . . . . . . 13  |-  0  e.  RR
65 eleq1 2494 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
6665anbi2d 708 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
67 fveq2 5877 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
68 oveq1 6308 . . . . . . . . . . . . . . . . 17  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
6968fveq2d 5881 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
7067, 69breq12d 4433 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
7166, 70imbi12d 321 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) ) ) )
7237simprrd 765 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
7372r19.21bi 2794 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
7471, 73vtoclg 3139 . . . . . . . . . . . . 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 672 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
77 1e0p1 11079 . . . . . . . . . . . 12  |-  1  =  ( 0  +  1 )
7877fveq2i 5880 . . . . . . . . . . 11  |-  ( Q `
 1 )  =  ( Q `  (
0  +  1 ) )
7976, 78syl6breqr 4461 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
8063, 79eqbrtrd 4441 . . . . . . . . 9  |-  ( ph  ->  A  <  ( Q `
 1 ) )
8147, 57, 58, 62, 80elicod 11685 . . . . . . . 8  |-  ( ph  ->  A  e.  ( ( Q `  0 ) [,) ( Q ` 
1 ) ) )
8278oveq2i 6312 . . . . . . . 8  |-  ( ( Q `  0 ) [,) ( Q ` 
1 ) )  =  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) )
8381, 82syl6eleq 2520 . . . . . . 7  |-  ( ph  ->  A  e.  ( ( Q `  0 ) [,) ( Q `  ( 0  +  1 ) ) ) )
8483adantr 466 . . . . . 6  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  A  e.  ( ( Q ` 
0 ) [,) ( Q `  ( 0  +  1 ) ) ) )
8532, 84eqeltrd 2510 . . . . 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 23 . . . . . . . . . . . 12  |-  ( x  =  X  ->  x  =  X )
89 fveq2 5877 . . . . . . . . . . . 12  |-  ( x  =  X  ->  ( Z `  x )  =  ( Z `  X ) )
9088, 89oveq12d 6319 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  +  ( Z `
 x ) )  =  ( X  +  ( Z `  X ) ) )
9190adantl 467 . . . . . . . . . 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 6309 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  ( B  -  x )  =  ( B  -  X ) )
9594oveq1d 6316 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  X )  /  T ) )
9695fveq2d 5881 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  X
)  /  T ) ) )
9796oveq1d 6316 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
9897adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  =  X )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) )
9921flcld 12033 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  ZZ )
10099zred 11040 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  RR )
101100, 15remulcld 9671 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  RR )
10293, 98, 10, 101fvmptd 5966 . . . . . . . . . . . 12  |-  ( ph  ->  ( Z `  X
)  =  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )
103102, 101eqeltrd 2510 . . . . . . . . . . 11  |-  ( ph  ->  ( Z `  X
)  e.  RR )
10410, 103readdcld 9670 . . . . . . . . . 10  |-  ( ph  ->  ( X  +  ( Z `  X ) )  e.  RR )
10587, 91, 10, 104fvmptd 5966 . . . . . . . . 9  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( Z `  X ) ) )
106102oveq2d 6317 . . . . . . . . 9  |-  ( ph  ->  ( X  +  ( Z `  X ) )  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
107105, 106eqtrd 2463 . . . . . . . 8  |-  ( ph  ->  ( E `  X
)  =  ( X  +  ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T ) ) )
108107oveq1d 6316 . . . . . . 7  |-  ( ph  ->  ( ( E `  X )  -  T
)  =  ( ( X  +  ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T ) )  -  T ) )
10910recnd 9669 . . . . . . . 8  |-  ( ph  ->  X  e.  CC )
110101recnd 9669 . . . . . . . 8  |-  ( ph  ->  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  e.  CC )
11115recnd 9669 . . . . . . . 8  |-  ( ph  ->  T  e.  CC )
112109, 110, 111addsubassd 10006 . . . . . . 7  |-  ( ph  ->  ( ( X  +  ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
) )  -  T
)  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  x.  T )  -  T ) ) )
11399zcnd 11041 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  (
( B  -  X
)  /  T ) )  e.  CC )
114113, 111mulsubfacd 10078 . . . . . . . 8  |-  ( ph  ->  ( ( ( |_
`  ( ( B  -  X )  /  T ) )  x.  T )  -  T
)  =  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) )
115114oveq2d 6317 . . . . . . 7  |-  ( ph  ->  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T
) )  x.  T
)  -  T ) )  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  -  1 )  x.  T ) ) )
116108, 112, 1153eqtrd 2467 . . . . . 6  |-  ( ph  ->  ( ( E `  X )  -  T
)  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  -  1 )  x.  T ) ) )
117116adantr 466 . . . . 5  |-  ( (
ph  /\  ( E `  X )  =  B )  ->  ( ( E `  X )  -  T )  =  ( X  +  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) ) )
118 oveq1 6308 . . . . . . . . 9  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  (
k  x.  T )  =  ( ( ( |_ `  ( ( B  -  X )  /  T ) )  -  1 )  x.  T ) )
119118oveq2d 6317 . . . . . . . 8  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  ( X  +  ( k  x.  T ) )  =  ( X  +  ( ( ( |_ `  ( ( B  -  X )  /  T
) )  -  1 )  x.  T ) ) )
120119eqeq2d 2436 . . . . . . 7  |-  ( k  =  ( ( |_
`  ( ( B  -  X )  /  T ) )  - 
1 )  ->  (
( ( E `  X )  -  T
)  =  ( X  +  ( k  x.  T ) )  <->  ( ( E `  X )  -  T )  =  ( X  +  ( ( ( |_ `  (
( B  -  X
)  /  T ) )  -  1 )  x.  T ) ) ) )
121120anbi2d 708 . . . . . 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 3182 . . . . 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 1262 . . . 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 6319 . . . . . . . 8  |-  ( i  =  0  ->  (
( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 0 ) [,) ( Q `  (
0  +  1 ) ) ) )
125124eleq2d 2492 . . . . . . 7  |-  ( i  =  0  ->  (
( ( E `  X )  -  T
)  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  <->  ( ( E `  X )  -  T )  e.  ( ( Q `  0
) [,) ( Q `
 ( 0  +  1 ) ) ) ) )
126125anbi1d 709 . . . . . 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 2939 . . . . 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 3182 . . . 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 665 . . 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 6329 . . . 4  |-  ( ( E `  X )  -  T )  e. 
_V
131 eleq1 2494 . . . . . . . 8  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  <->  ( ( E `  X )  -  T )  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) ) )
132 eqeq1 2426 . . . . . . . 8  |-  ( y  =  ( ( E `
 X )  -  T )  ->  (
y  =  ( X  +  ( k  x.  T ) )  <->  ( ( E `  X )  -  T )  =  ( X  +  ( k  x.  T ) ) ) )
133131, 132anbi12d 715 . . . . . . 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 2946 . . . . . 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 708 . . . . 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 318 . . . 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 462 . . . . 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 1751 . . . . . . 7  |-  F/ i
ph
139 nfre1 2886 . . . . . . 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 1984 . . . . . 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 1751 . . . . . . 7  |-  F/ k
ph
142 nfcv 2584 . . . . . . . 8  |-  F/_ k
( 0..^ M )
143 nfre1 2886 . . . . . . . 8  |-  F/ k E. k  e.  ZZ  ( y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) )
144142, 143nfrex 2888 . . . . . . 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 1984 . . . . . 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 1005 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  k  e.  ZZ )  /\  ( y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  /\  y  =  ( X  +  ( k  x.  T ) ) ) )  ->  ph )
147 simp2l 1031 . . . . . . . . . 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 1033 . . . . . . . . . 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 536 . . . . . . . . 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 1032 . . . . . . . . 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 1034 . . . . . . . . 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 197 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) )  /\  k  e.  ZZ )  /\  y  =  ( X  +  ( k  x.  T
) ) ) )
154153simplld 759 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i ) [,) ( Q `  (
i  +  1 ) ) ) ) )
155154simplld 759 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ph )
156 fourierdlem48.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : D --> RR )
157 frel 5745 . . . . . . . . . . . . . . . 16  |-  ( F : D --> RR  ->  Rel 
F )
158155, 156, 1573syl 18 . . . . . . . . . . . . . . 15  |-  ( ch 
->  Rel  F )
159 resindm 5164 . . . . . . . . . . . . . . . 16  |-  ( Rel 
F  ->  ( F  |`  ( ( X (,) +oo )  i^i  dom  F
) )  =  ( F  |`  ( X (,) +oo ) ) )
160159eqcomd 2430 . . . . . . . . . . . . . . 15  |-  ( Rel 
F  ->  ( F  |`  ( X (,) +oo ) )  =  ( F  |`  ( ( X (,) +oo )  i^i 
dom  F ) ) )
161158, 160syl 17 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F  |`  ( X (,) +oo ) )  =  ( F  |`  ( ( X (,) +oo )  i^i  dom  F
) ) )
162 fdm 5746 . . . . . . . . . . . . . . . . 17  |-  ( F : D --> RR  ->  dom 
F  =  D )
163155, 156, 1623syl 18 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  dom  F  =  D )
164163ineq2d 3664 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( X (,) +oo )  i^i  dom  F
)  =  ( ( X (,) +oo )  i^i  D ) )
165164reseq2d 5120 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F  |`  (
( X (,) +oo )  i^i  dom  F )
)  =  ( F  |`  ( ( X (,) +oo )  i^i  D ) ) )
166161, 165eqtrd 2463 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F  |`  ( X (,) +oo ) )  =  ( F  |`  ( ( X (,) +oo )  i^i  D ) ) )
167166oveq1d 6316 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( F  |`  ( X (,) +oo )
) lim CC  X )  =  ( ( F  |`  ( ( X (,) +oo )  i^i  D ) ) lim CC  X ) )
168155, 156syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  F : D --> RR )
169 ax-resscn 9596 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
170169a1i 11 . . . . . . . . . . . . . . 15  |-  ( ch 
->  RR  C_  CC )
171168, 170fssd 5751 . . . . . . . . . . . . . 14  |-  ( ch 
->  F : D --> CC )
172 inss2 3683 . . . . . . . . . . . . . . 15  |-  ( ( X (,) +oo )  i^i  D )  C_  D
173172a1i 11 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( X (,) +oo )  i^i  D ) 
C_  D )
174171, 173fssresd 5763 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F  |`  (
( X (,) +oo )  i^i  D ) ) : ( ( X (,) +oo )  i^i 
D ) --> CC )
175 pnfxr 11412 . . . . . . . . . . . . . . . 16  |- +oo  e.  RR*
176175a1i 11 . . . . . . . . . . . . . . 15  |-  ( ch 
-> +oo  e.  RR* )
177154simplrd 761 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  i  e.  (
0..^ M ) )
17840adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
179 fzofzp1 12007 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
180179adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
181178, 180ffvelrnd 6034 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
182155, 177, 181syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
183153simplrd 761 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  k  e.  ZZ )
184183zred 11040 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  k  e.  RR )
185155, 15syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  T  e.  RR )
186184, 185remulcld 9671 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( k  x.  T
)  e.  RR )
187182, 186resubcld 10047 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR )
188187rexrd 9690 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )
189187ltpnfd 11423 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  < +oo )
190188, 176, 189xrltled 37325 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  <_ +oo )
191 iooss2 11672 . . . . . . . . . . . . . . 15  |-  ( ( +oo  e.  RR*  /\  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  <_ +oo )  ->  ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  C_  ( X (,) +oo )
)
192176, 190, 191syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  ( X (,) +oo ) )
193183adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  k  e.  ZZ )
194193zcnd 11041 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  k  e.  CC )
195185recnd 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  T  e.  CC )
196195adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  T  e.  CC )
197194, 196mulneg1d 10071 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( -u k  x.  T )  =  -u ( k  x.  T ) )
198197oveq2d 6317 . . . . . . . . . . . . . . . . . 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 11666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  w  e.  RR )
200199recnd 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  w  e.  CC )
201200adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  CC )
202194, 196mulcld 9663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  CC )
203201, 202addcld 9662 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  CC )
204203, 202negsubd 9992 . . . . . . . . . . . . . . . . . 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 9987 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  -  ( k  x.  T ) )  =  w )
206198, 204, 2053eqtrrd 2468 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
207155adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ph )
208154simpld 460 . . . . . . . . . . . . . . . . . . . . 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 21911 . . . . . . . . . . . . . . . . . . . . . . . 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 5746 . . . . . . . . . . . . . . . . . . . . . . . 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 18 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
213 ssdmres 5141 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  F  <->  dom  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
214212, 213sylibr 215 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  F )
215156, 162syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  F  =  D )
216215adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  dom  F  =  D )
217214, 216sseqtrd 3500 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  D
)
218208, 217syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  D )
219218adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  D )
220 elfzofz 11935 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
221220adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
222178, 221ffvelrnd 6034 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
223155, 177, 222syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( Q `  i
)  e.  RR )
224223rexrd 9690 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
225224adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  e.  RR* )
226182rexrd 9690 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
227226adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
228199adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  RR )
229193zred 11040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  k  e.  RR )
230207, 15syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  T  e.  RR )
231229, 230remulcld 9671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  RR )
232228, 231readdcld 9670 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  RR )
233223adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  e.  RR )
234155, 10syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  X  e.  RR )
235234, 186readdcld 9670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( X  +  ( k  x.  T ) )  e.  RR )
236235adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( X  +  ( k  x.  T ) )  e.  RR )
237152simprbi 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  y  =  ( X  +  ( k  x.  T ) ) )
238237eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( X  +  ( k  x.  T ) )  =  y )
239154simprd 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  y  e.  (
( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) )
240238, 239eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( X  +  ( k  x.  T ) )  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )
241 icogelb 11686 . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( Q `  i
)  <_  ( X  +  ( k  x.  T ) ) )
243242adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  <_  ( X  +  ( k  x.  T ) ) )
244207, 10syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  e.  RR )
245244rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  e.  RR* )
246182adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
247246, 231resubcld 10047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR )
248247rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR* )
249 simpr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
250 ioogtlb 37422 . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  <  w )
252244, 228, 231, 251ltadd1dd 10224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( X  +  ( k  x.  T ) )  < 
( w  +  ( k  x.  T ) ) )
253233, 236, 232, 243, 252lelttrd 9793 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  ( Q `  i )  <  ( w  +  ( k  x.  T ) ) )
254 iooltub 37440 . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  <  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )
256228, 247, 231, 255ltadd1dd 10224 . . . . . . . . . . . . . . . . . . . . 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 9669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  CC )
258186recnd 9669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( k  x.  T
)  e.  CC )
259257, 258npcand 9990 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) )  +  ( k  x.  T ) )  =  ( Q `
 ( i  +  1 ) ) )
260259adantr 466 . . . . . . . . . . . . . . . . . . . . 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 4445 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  <  ( Q `  ( i  +  1 ) ) )
262225, 227, 232, 253, 261eliood 37425 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
263219, 262sseldd 3465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  D )
264193znegcld 11042 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  -u k  e.  ZZ )
265 ovex 6329 . . . . . . . . . . . . . . . . . . 19  |-  ( w  +  ( k  x.  T ) )  e. 
_V
266 eleq1 2494 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
x  e.  D  <->  ( w  +  ( k  x.  T ) )  e.  D ) )
2672663anbi2d 1340 . . . . . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
x  +  ( -u k  x.  T )
)  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
269268eleq1d 2491 . . . . . . . . . . . . . . . . . . . 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 321 . . . . . . . . . . . . . . . . . . 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 9873 . . . . . . . . . . . . . . . . . . . 20  |-  -u k  e.  _V
272 eleq1 2494 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  -u k  ->  (
j  e.  ZZ  <->  -u k  e.  ZZ ) )
2732723anbi3d 1341 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  -u k  ->  (
( ph  /\  x  e.  D  /\  j  e.  ZZ )  <->  ( ph  /\  x  e.  D  /\  -u k  e.  ZZ ) ) )
274 oveq1 6308 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  -u k  ->  (
j  x.  T )  =  ( -u k  x.  T ) )
275274oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  -u k  ->  (
x  +  ( j  x.  T ) )  =  ( x  +  ( -u k  x.  T
) ) )
276275eleq1d 2491 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  -u k  ->  (
( x  +  ( j  x.  T ) )  e.  D  <->  ( x  +  ( -u k  x.  T ) )  e.  D ) )
277273, 276imbi12d 321 . . . . . . . . . . . . . . . . . . . 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 2494 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
k  e.  ZZ  <->  j  e.  ZZ ) )
2792783anbi3d 1341 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( ph  /\  x  e.  D  /\  k  e.  ZZ )  <->  ( ph  /\  x  e.  D  /\  j  e.  ZZ )
) )
280 oveq1 6308 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
281280oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  j  ->  (
x  +  ( k  x.  T ) )  =  ( x  +  ( j  x.  T
) ) )
282281eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
( x  +  ( k  x.  T ) )  e.  D  <->  ( x  +  ( j  x.  T ) )  e.  D ) )
283279, 282imbi12d 321 . . . . . . . . . . . . . . . . . . . . 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 2068 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  D  /\  j  e.  ZZ )  ->  ( x  +  ( j  x.  T
) )  e.  D
)
286271, 277, 285vtocl 3133 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  D  /\  -u k  e.  ZZ )  ->  ( x  +  ( -u k  x.  T
) )  e.  D
)
287265, 270, 286vtocl 3133 . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D )
289206, 288eqeltrd 2510 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  D )
290289ralrimiva 2839 . . . . . . . . . . . . . . 15  |-  ( ch 
->  A. w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) w  e.  D )
291 dfss3 3454 . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  D )
293192, 292ssind 3686 . . . . . . . . . . . . 13  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  ( ( X (,) +oo )  i^i 
D ) )
294 ioosscn 37421 . . . . . . . . . . . . . 14  |-  ( X (,) +oo )  C_  CC
295 ssinss1 3690 . . . . . . . . . . . . . 14  |-  ( ( X (,) +oo )  C_  CC  ->  ( ( X (,) +oo )  i^i 
D )  C_  CC )
296294, 295mp1i 13 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( X (,) +oo )  i^i  D ) 
C_  CC )
297 eqid 2422 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
298 eqid 2422 . . . . . . . . . . . . 13  |-  ( (
TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  =  ( ( TopOpen ` fld )t  ( ( ( X (,) +oo )  i^i  D )  u.  { X } ) )
299234rexrd 9690 . . . . . . . . . . . . . . 15  |-  ( ch 
->  X  e.  RR* )
300234leidd 10180 . . . . . . . . . . . . . . 15  |-  ( ch 
->  X  <_  X )
301237oveq1d 6316 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( y  -  (
k  x.  T ) )  =  ( ( X  +  ( k  x.  T ) )  -  ( k  x.  T ) ) )
302234recnd 9669 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  X  e.  CC )
303302, 258pncand 9987 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( X  +  ( k  x.  T
) )  -  (
k  x.  T ) )  =  X )
304301, 303eqtr2d 2464 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  X  =  (
y  -  ( k  x.  T ) ) )
305 icossre 11715 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  i
)  e.  RR  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
( Q `  i
) [,) ( Q `
 ( i  +  1 ) ) ) 
C_  RR )
306223, 226, 305syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) )  C_  RR )
307306, 239sseldd 3465 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  y  e.  RR )
308 icoltub 37437 . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  y  <  ( Q `
 ( i  +  1 ) ) )
310307, 182, 186, 309ltsub1dd 10225 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( y  -  (
k  x.  T ) )  <  ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) )
311304, 310eqbrtrd 4441 . . . . . . . . . . . . . . 15  |-  ( ch 
->  X  <  ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) )
312299, 188, 299, 300, 311elicod 11685 . . . . . . . . . . . . . 14  |-  ( ch 
->  X  e.  ( X [,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) ) )
313 snunioo1 37443 . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  u.  { X } )  =  ( X [,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) )
315314fveq2d 5881 . . . . . . . . . . . . . . 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 21790 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  Top
317 ovex 6329 . . . . . . . . . . . . . . . . . . . 20  |-  ( X (,) +oo )  e. 
_V
318317inex1 4561 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X (,) +oo )  i^i  D )  e.  _V
319 snex 4658 . . . . . . . . . . . . . . . . . . 19  |-  { X }  e.  _V
320318, 319unex 6599 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } )  e.  _V
321 resttop 20162 . . . . . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . . . . . 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 21768 . . . . . . . . . . . . . . . . . . 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 21772 . . . . . . . . . . . . . . . . . . 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 15314 . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . 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 11414 . . . . . . . . . . . . . . . . . . . . . 22  |- -oo  e.  RR*
332331a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  -> -oo  e.  RR* )
333188adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) )  e.  RR* )
334 icossre 11715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  e.  RR  /\  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )  ->  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  RR )
335234, 188, 334syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  RR )
336335sselda 3464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  RR )
337336mnfltd 11426 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  -> -oo  <  x )
338299adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  e.  RR* )
339 simpr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
340 icoltub 37437 . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  <  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )
342332, 333, 336, 337, 341eliood 37425 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( -oo (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )
343 ssnid 4025 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  x  e. 
{ x }
344343a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  X  ->  x  e.  { x } )
345 sneq 4006 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  X  ->  { x }  =  { X } )
346344, 345eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  X  ->  x  e.  { X } )
347 elun2 3634 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  { X }  ->  x  e.  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } ) )
348346, 347syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  X  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
349348adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  x  =  X )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
350299ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  RR )
353234ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  e.  RR )
354 icogelb 11686 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  X  <_  x )
356355adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  <_  x )
357 neqne 37234 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  x  =  X  ->  x  =/=  X )
358357adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  =/=  X )
359353, 352, 356, 358leneltd 9789 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  X  <  x )
360352ltpnfd 11423 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  < +oo )
361350, 351, 352, 359, 360eliood 37425 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( X (,) +oo ) )
362183zcnd 11041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ch 
->  k  e.  CC )
363362, 195mulneg1d 10071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ch 
->  ( -u k  x.  T )  =  -u ( k  x.  T
) )
364363oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ch 
->  ( ( w  +  ( k  x.  T
) )  +  (
-u k  x.  T
) )  =  ( ( w  +  ( k  x.  T ) )  +  -u (
k  x.  T ) ) )
365364adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 37421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) )  C_  CC
367366sseli 3460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  w  e.  CC )
368367adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  CC )
369258adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  CC )
370368, 369addcld 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  CC )
371370, 369negsubd 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  -  ( k  x.  T ) )  =  w )
373365, 371, 3723eqtrrd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
374186adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
k  x.  T )  e.  RR )
375228, 374readdcld 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  RR )
376225, 227, 375, 253, 261eliood 37425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
377219, 376sseldd 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
w  +  ( k  x.  T ) )  e.  D )
3782723anbi3d 1341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  -u k  ->  (
( w  +  ( k  x.  T ) )  +  ( j  x.  T ) )  =  ( ( w  +  ( k  x.  T ) )  +  ( -u k  x.  T ) ) )
380379eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
x  +  ( j  x.  T ) )  =  ( ( w  +  ( k  x.  T ) )  +  ( j  x.  T
) ) )
384383eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  ( w  +  ( k  x.  T
) )  ->  (
( x  +  ( j  x.  T ) )  e.  D  <->  ( (
w  +  ( k  x.  T ) )  +  ( j  x.  T ) )  e.  D ) )
385382, 384imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( w  +  ( k  x.  T ) )  e.  D  /\  j  e.  ZZ )  ->  (
( w  +  ( k  x.  T ) )  +  ( j  x.  T ) )  e.  D )
387271, 381, 386vtocl 3133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  (
( w  +  ( k  x.  T ) )  +  ( -u k  x.  T )
)  e.  D )
389373, 388eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ch  /\  w  e.  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  w  e.  D )
390389ralrimiva 2839 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  A. w  e.  ( X (,) ( ( Q `  ( i  +  1 ) )  -  ( k  x.  T ) ) ) w  e.  D )
391390, 291sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  D )
392391ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  ( X (,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) )  C_  D )
393188ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) )  e.  RR* )
394341adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 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 37425 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( X (,) ( ( Q `
 ( i  +  1 ) )  -  ( k  x.  T
) ) ) )
396392, 395sseldd 3465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  D )
397361, 396elind 3650 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  /\  -.  x  =  X )  ->  x  e.  ( ( X (,) +oo )  i^i  D ) )
398 elun1 3633 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( X (,) +oo )  i^i 
D )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
399397, 398syl 17 . . . . . . . . . . . . . . . . . . . . 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 798 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( X [,) (
( Q `  (
i  +  1 ) )  -  ( k  x.  T ) ) ) )  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
401342, 400elind 3650 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) ) )  ->  X  e.  RR* )
403188adantr 466 . . . . . . . . . . . . . . . . . . . 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 3651 . . . . . . . . . . . . . . . . . . . . . . 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 11666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  ->  x  e.  RR )
406404, 405syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  ->  x  e.  RR )
407406rexrd 9690 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( ( -oo (,) ( ( Q `  ( i  +  1 ) )  -  (
k  x.  T ) ) )  i^i  (
( ( X (,) +oo )  i^i  D )  u.  { X }
) )  ->  x  e.  RR* )
408407adantl 467 . . . . . . . . . . . . . . . . . . . 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 3652 . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  =  X )  ->  X  e.  RR )
41188eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  X  ->  X  =  x )
412411adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  =  X )  ->  X  =  x )
413410, 412eqled 9737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  x  =  X )  ->  X  <_  x )
414413adantlr 719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  x  =  X )  ->  X  <_  x )
415 simpll 758 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  ch )
416 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )
417 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  x  =  X  ->  -.  x  =  X
)
418 elsn 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  { X }  <->  x  =  X )
419417, 418sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  x  =  X  ->  -.  x  e.  { X } )
420419adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  -.  x  e.  { X } )
421 elunnel2 37220 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( ( ( X (,) +oo )  i^i  D )  u. 
{ X } )  /\  -.  x  e. 
{ X } )  ->  x  e.  ( ( X (,) +oo )  i^i  D ) )
422416, 420, 421syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  x  e.  ( ( X (,) +oo )  i^i  D ) )
423 elinel1 3651 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( ( X (,) +oo )  i^i 
D )  ->  x  e.  ( X (,) +oo ) )
424422, 423syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  x  e.  ( X (,) +oo )
)
425234adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  e.  RR )
426 elioore 11666 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( X (,) +oo )  ->  x  e.  RR )
427426adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  x  e.  RR )
428299adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  e.  RR* )
429175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  -> +oo  e.  RR* )
430 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  x  e.  ( X (,) +oo ) )
431 ioogtlb 37422 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( X  e.  RR*  /\ +oo  e.  RR*  /\  x  e.  ( X (,) +oo ) )  ->  X  <  x )
432428, 429, 430, 431syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  <  x )
433425, 427, 432ltled 9783 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  x  e.  ( X (,) +oo ) )  ->  X  <_  x )
434415, 424, 433syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  /\  -.  x  =  X
)  ->  X  <_  x )
435414, 434pm2.61dan 798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  x  e.  ( ( ( X (,) +oo )  i^i 
D )  u.  { X } ) )  ->  X  <_  x )
436409, 435sylan2 476 . . . . . . . . . . . . . . . . . . . 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  x.