Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem6 Unicode version

Theorem heiborlem6 26216
Description: Lemma for heibor 26221. Since the sequence of balls connected by the function  T ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most  3  /  2 times the size of the larger, and so if we expand each ball by a factor of  3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)
Hypotheses
Ref Expression
heibor.1  |-  J  =  ( MetOpen `  D )
heibor.3  |-  K  =  { u  |  -.  E. v  e.  ( ~P U  i^i  Fin )
u  C_  U. v }
heibor.4  |-  G  =  { <. y ,  n >.  |  ( n  e. 
NN0  /\  y  e.  ( F `  n )  /\  ( y B n )  e.  K
) }
heibor.5  |-  B  =  ( z  e.  X ,  m  e.  NN0  |->  ( z ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
heibor.6  |-  ( ph  ->  D  e.  ( CMet `  X ) )
heibor.7  |-  ( ph  ->  F : NN0 --> ( ~P X  i^i  Fin )
)
heibor.8  |-  ( ph  ->  A. n  e.  NN0  X  =  U_ y  e.  ( F `  n
) ( y B n ) )
heibor.9  |-  ( ph  ->  A. x  e.  G  ( ( T `  x ) G ( ( 2nd `  x
)  +  1 )  /\  ( ( B `
 x )  i^i  ( ( T `  x ) B ( ( 2nd `  x
)  +  1 ) ) )  e.  K
) )
heibor.10  |-  ( ph  ->  C G 0 )
heibor.11  |-  S  =  seq  0 ( T ,  ( m  e. 
NN0  |->  if ( m  =  0 ,  C ,  ( m  - 
1 ) ) ) )
heibor.12  |-  M  =  ( n  e.  NN  |->  <. ( S `  n
) ,  ( 3  /  ( 2 ^ n ) ) >.
)
Assertion
Ref Expression
heiborlem6  |-  ( ph  ->  A. k  e.  NN  ( ( ball `  D
) `  ( M `  ( k  +  1 ) ) )  C_  ( ( ball `  D
) `  ( M `  k ) ) )
Distinct variable groups:    x, n, y, k, u, F    k, G, x    ph, k, x   
k, m, v, z, D, n, u, x, y    k, M, m, u, x, y, z    T, m, n, x, y, z    B, n, u, v, y    k, J, m, n, u, v, x, y, z    U, n, u, v, x, y, z    S, k, m, n, u, v, x, y, z    k, X, m, n, u, v, x, y, z    C, m, n, u, v, y   
n, K, x, y, z    x, B
Allowed substitution hints:    ph( y, z, v, u, m, n)    B( z, k, m)    C( x, z, k)    T( v, u, k)    U( k, m)    F( z, v, m)    G( y, z, v, u, m, n)    K( v, u, k, m)    M( v, n)

Proof of Theorem heiborlem6
StepHypRef Expression
1 nnnn0 10160 . . . 4  |-  ( k  e.  NN  ->  k  e.  NN0 )
2 heibor.6 . . . . . . . 8  |-  ( ph  ->  D  e.  ( CMet `  X ) )
3 cmetmet 19110 . . . . . . . 8  |-  ( D  e.  ( CMet `  X
)  ->  D  e.  ( Met `  X ) )
42, 3syl 16 . . . . . . 7  |-  ( ph  ->  D  e.  ( Met `  X ) )
5 metxmet 18273 . . . . . . 7  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( * Met `  X
) )
64, 5syl 16 . . . . . 6  |-  ( ph  ->  D  e.  ( * Met `  X ) )
76adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  D  e.  ( * Met `  X
) )
8 heibor.7 . . . . . . . . 9  |-  ( ph  ->  F : NN0 --> ( ~P X  i^i  Fin )
)
9 inss1 3504 . . . . . . . . 9  |-  ( ~P X  i^i  Fin )  C_ 
~P X
10 fss 5539 . . . . . . . . 9  |-  ( ( F : NN0 --> ( ~P X  i^i  Fin )  /\  ( ~P X  i^i  Fin )  C_  ~P X
)  ->  F : NN0
--> ~P X )
118, 9, 10sylancl 644 . . . . . . . 8  |-  ( ph  ->  F : NN0 --> ~P X
)
12 peano2nn0 10192 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
13 ffvelrn 5807 . . . . . . . 8  |-  ( ( F : NN0 --> ~P X  /\  ( k  +  1 )  e.  NN0 )  ->  ( F `  (
k  +  1 ) )  e.  ~P X
)
1411, 12, 13syl2an 464 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  ( k  +  1 ) )  e.  ~P X )
1514elpwid 3751 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  ( k  +  1 ) )  C_  X
)
16 heibor.1 . . . . . . . . 9  |-  J  =  ( MetOpen `  D )
17 heibor.3 . . . . . . . . 9  |-  K  =  { u  |  -.  E. v  e.  ( ~P U  i^i  Fin )
u  C_  U. v }
18 heibor.4 . . . . . . . . 9  |-  G  =  { <. y ,  n >.  |  ( n  e. 
NN0  /\  y  e.  ( F `  n )  /\  ( y B n )  e.  K
) }
19 heibor.5 . . . . . . . . 9  |-  B  =  ( z  e.  X ,  m  e.  NN0  |->  ( z ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
20 heibor.8 . . . . . . . . 9  |-  ( ph  ->  A. n  e.  NN0  X  =  U_ y  e.  ( F `  n
) ( y B n ) )
21 heibor.9 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  G  ( ( T `  x ) G ( ( 2nd `  x
)  +  1 )  /\  ( ( B `
 x )  i^i  ( ( T `  x ) B ( ( 2nd `  x
)  +  1 ) ) )  e.  K
) )
22 heibor.10 . . . . . . . . 9  |-  ( ph  ->  C G 0 )
23 heibor.11 . . . . . . . . 9  |-  S  =  seq  0 ( T ,  ( m  e. 
NN0  |->  if ( m  =  0 ,  C ,  ( m  - 
1 ) ) ) )
2416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 26214 . . . . . . . 8  |-  ( (
ph  /\  ( k  +  1 )  e. 
NN0 )  ->  ( S `  ( k  +  1 ) ) G ( k  +  1 ) )
2512, 24sylan2 461 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) ) G ( k  +  1 ) )
26 fvex 5682 . . . . . . . . 9  |-  ( S `
 ( k  +  1 ) )  e. 
_V
27 ovex 6045 . . . . . . . . 9  |-  ( k  +  1 )  e. 
_V
2816, 17, 18, 26, 27heiborlem2 26212 . . . . . . . 8  |-  ( ( S `  ( k  +  1 ) ) G ( k  +  1 )  <->  ( (
k  +  1 )  e.  NN0  /\  ( S `  ( k  +  1 ) )  e.  ( F `  ( k  +  1 ) )  /\  (
( S `  (
k  +  1 ) ) B ( k  +  1 ) )  e.  K ) )
2928simp2bi 973 . . . . . . 7  |-  ( ( S `  ( k  +  1 ) ) G ( k  +  1 )  ->  ( S `  ( k  +  1 ) )  e.  ( F `  ( k  +  1 ) ) )
3025, 29syl 16 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  e.  ( F `  ( k  +  1 ) ) )
3115, 30sseldd 3292 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  e.  X
)
3211ffvelrnda 5809 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  e.  ~P X )
3332elpwid 3751 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  C_  X
)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 26214 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k ) G k )
35 fvex 5682 . . . . . . . . 9  |-  ( S `
 k )  e. 
_V
36 vex 2902 . . . . . . . . 9  |-  k  e. 
_V
3716, 17, 18, 35, 36heiborlem2 26212 . . . . . . . 8  |-  ( ( S `  k ) G k  <->  ( k  e.  NN0  /\  ( S `
 k )  e.  ( F `  k
)  /\  ( ( S `  k ) B k )  e.  K ) )
3837simp2bi 973 . . . . . . 7  |-  ( ( S `  k ) G k  ->  ( S `  k )  e.  ( F `  k
) )
3934, 38syl 16 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k )  e.  ( F `  k ) )
4033, 39sseldd 3292 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k )  e.  X
)
41 3re 10003 . . . . . 6  |-  3  e.  RR
42 2nn 10065 . . . . . . . . 9  |-  2  e.  NN
43 nnexpcl 11321 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  ( k  +  1 )  e.  NN0 )  ->  ( 2 ^ (
k  +  1 ) )  e.  NN )
4442, 12, 43sylancr 645 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  e.  NN )
4544nnrpd 10579 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  e.  RR+ )
4645adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2 ^ ( k  +  1 ) )  e.  RR+ )
47 rerpdivcl 10571 . . . . . 6  |-  ( ( 3  e.  RR  /\  ( 2 ^ (
k  +  1 ) )  e.  RR+ )  ->  ( 3  /  (
2 ^ ( k  +  1 ) ) )  e.  RR )
4841, 46, 47sylancr 645 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 3  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR )
49 nnexpcl 11321 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  k  e.  NN0 )  -> 
( 2 ^ k
)  e.  NN )
5042, 49mpan 652 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  NN )
5150nnrpd 10579 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  RR+ )
5251adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2 ^ k )  e.  RR+ )
53 rerpdivcl 10571 . . . . . 6  |-  ( ( 3  e.  RR  /\  ( 2 ^ k
)  e.  RR+ )  ->  ( 3  /  (
2 ^ k ) )  e.  RR )
5441, 52, 53sylancr 645 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 3  /  ( 2 ^ k ) )  e.  RR )
55 oveq1 6027 . . . . . . . . . . . 12  |-  ( z  =  ( S `  k )  ->  (
z ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
56 oveq2 6028 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
2 ^ m )  =  ( 2 ^ k ) )
5756oveq2d 6036 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  (
1  /  ( 2 ^ m ) )  =  ( 1  / 
( 2 ^ k
) ) )
5857oveq2d 6036 . . . . . . . . . . . 12  |-  ( m  =  k  ->  (
( S `  k
) ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) ) )
59 ovex 6045 . . . . . . . . . . . 12  |-  ( ( S `  k ) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  e. 
_V
6055, 58, 19, 59ovmpt2 6148 . . . . . . . . . . 11  |-  ( ( ( S `  k
)  e.  X  /\  k  e.  NN0 )  -> 
( ( S `  k ) B k )  =  ( ( S `  k ) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) ) )
6140, 60sylancom 649 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) B k )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) ) )
62 df-br 4154 . . . . . . . . . . . . . . . . 17  |-  ( ( S `  k ) G k  <->  <. ( S `
 k ) ,  k >.  e.  G
)
63 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( T `  x )  =  ( T `  <. ( S `  k ) ,  k >. )
)
64 df-ov 6023 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S `  k ) T k )  =  ( T `  <. ( S `  k ) ,  k >. )
6563, 64syl6eqr 2437 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( T `  x )  =  ( ( S `  k
) T k ) )
6635, 36op2ndd 6297 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( 2nd `  x
)  =  k )
6766oveq1d 6035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( 2nd `  x )  +  1 )  =  ( k  +  1 ) )
6865, 67breq12d 4166 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( T `
 x ) G ( ( 2nd `  x
)  +  1 )  <-> 
( ( S `  k ) T k ) G ( k  +  1 ) ) )
69 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( B `  x )  =  ( B `  <. ( S `  k ) ,  k >. )
)
70 df-ov 6023 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S `  k ) B k )  =  ( B `  <. ( S `  k ) ,  k >. )
7169, 70syl6eqr 2437 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( B `  x )  =  ( ( S `  k
) B k ) )
7265, 67oveq12d 6038 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( T `
 x ) B ( ( 2nd `  x
)  +  1 ) )  =  ( ( ( S `  k
) T k ) B ( k  +  1 ) ) )
7371, 72ineq12d 3486 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( B `
 x )  i^i  ( ( T `  x ) B ( ( 2nd `  x
)  +  1 ) ) )  =  ( ( ( S `  k ) B k )  i^i  ( ( ( S `  k
) T k ) B ( k  +  1 ) ) ) )
7473eleq1d 2453 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( ( B `  x )  i^i  ( ( T `
 x ) B ( ( 2nd `  x
)  +  1 ) ) )  e.  K  <->  ( ( ( S `  k ) B k )  i^i  ( ( ( S `  k
) T k ) B ( k  +  1 ) ) )  e.  K ) )
7568, 74anbi12d 692 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( ( T `  x ) G ( ( 2nd `  x )  +  1 )  /\  ( ( B `  x )  i^i  ( ( T `
 x ) B ( ( 2nd `  x
)  +  1 ) ) )  e.  K
)  <->  ( ( ( S `  k ) T k ) G ( k  +  1 )  /\  ( ( ( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K ) ) )
7675rspccv 2992 . . . . . . . . . . . . . . . . . 18  |-  ( A. x  e.  G  (
( T `  x
) G ( ( 2nd `  x )  +  1 )  /\  ( ( B `  x )  i^i  (
( T `  x
) B ( ( 2nd `  x )  +  1 ) ) )  e.  K )  ->  ( <. ( S `  k ) ,  k >.  e.  G  ->  ( ( ( S `
 k ) T k ) G ( k  +  1 )  /\  ( ( ( S `  k ) B k )  i^i  ( ( ( S `
 k ) T k ) B ( k  +  1 ) ) )  e.  K
) ) )
7721, 76syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( <. ( S `  k ) ,  k
>.  e.  G  ->  (
( ( S `  k ) T k ) G ( k  +  1 )  /\  ( ( ( S `
 k ) B k )  i^i  (
( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K ) ) )
7862, 77syl5bi 209 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( S `  k ) G k  ->  ( ( ( S `  k ) T k ) G ( k  +  1 )  /\  ( ( ( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K ) ) )
7978adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) G k  ->  (
( ( S `  k ) T k ) G ( k  +  1 )  /\  ( ( ( S `
 k ) B k )  i^i  (
( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K ) ) )
8034, 79mpd 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) T k ) G ( k  +  1 )  /\  (
( ( S `  k ) B k )  i^i  ( ( ( S `  k
) T k ) B ( k  +  1 ) ) )  e.  K ) )
8180simpld 446 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k ) G ( k  +  1 ) )
82 ovex 6045 . . . . . . . . . . . . . . 15  |-  ( ( S `  k ) T k )  e. 
_V
8316, 17, 18, 82, 27heiborlem2 26212 . . . . . . . . . . . . . 14  |-  ( ( ( S `  k
) T k ) G ( k  +  1 )  <->  ( (
k  +  1 )  e.  NN0  /\  (
( S `  k
) T k )  e.  ( F `  ( k  +  1 ) )  /\  (
( ( S `  k ) T k ) B ( k  +  1 ) )  e.  K ) )
8483simp2bi 973 . . . . . . . . . . . . 13  |-  ( ( ( S `  k
) T k ) G ( k  +  1 )  ->  (
( S `  k
) T k )  e.  ( F `  ( k  +  1 ) ) )
8581, 84syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k )  e.  ( F `  (
k  +  1 ) ) )
8615, 85sseldd 3292 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k )  e.  X )
8712adantl 453 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( k  +  1 )  e. 
NN0 )
88 oveq1 6027 . . . . . . . . . . . 12  |-  ( z  =  ( ( S `
 k ) T k )  ->  (
z ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
89 oveq2 6028 . . . . . . . . . . . . . 14  |-  ( m  =  ( k  +  1 )  ->  (
2 ^ m )  =  ( 2 ^ ( k  +  1 ) ) )
9089oveq2d 6036 . . . . . . . . . . . . 13  |-  ( m  =  ( k  +  1 )  ->  (
1  /  ( 2 ^ m ) )  =  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )
9190oveq2d 6036 . . . . . . . . . . . 12  |-  ( m  =  ( k  +  1 )  ->  (
( ( S `  k ) T k ) ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
92 ovex 6045 . . . . . . . . . . . 12  |-  ( ( ( S `  k
) T k ) ( ball `  D
) ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e. 
_V
9388, 91, 19, 92ovmpt2 6148 . . . . . . . . . . 11  |-  ( ( ( ( S `  k ) T k )  e.  X  /\  ( k  +  1 )  e.  NN0 )  ->  ( ( ( S `
 k ) T k ) B ( k  +  1 ) )  =  ( ( ( S `  k
) T k ) ( ball `  D
) ( 1  / 
( 2 ^ (
k  +  1 ) ) ) ) )
9486, 87, 93syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) T k ) B ( k  +  1 ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
9561, 94ineq12d 3486 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  =  ( ( ( S `
 k ) (
ball `  D )
( 1  /  (
2 ^ k ) ) )  i^i  (
( ( S `  k ) T k ) ( ball `  D
) ( 1  / 
( 2 ^ (
k  +  1 ) ) ) ) ) )
9680simprd 450 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K )
97 0elpw 4310 . . . . . . . . . . . . 13  |-  (/)  e.  ~P U
98 0fin 7272 . . . . . . . . . . . . 13  |-  (/)  e.  Fin
99 elin 3473 . . . . . . . . . . . . 13  |-  ( (/)  e.  ( ~P U  i^i  Fin )  <->  ( (/)  e.  ~P U  /\  (/)  e.  Fin )
)
10097, 98, 99mpbir2an 887 . . . . . . . . . . . 12  |-  (/)  e.  ( ~P U  i^i  Fin )
101 0ss 3599 . . . . . . . . . . . 12  |-  (/)  C_  U. (/)
102 unieq 3966 . . . . . . . . . . . . . 14  |-  ( v  =  (/)  ->  U. v  =  U. (/) )
103102sseq2d 3319 . . . . . . . . . . . . 13  |-  ( v  =  (/)  ->  ( (/)  C_ 
U. v  <->  (/)  C_  U. (/) ) )
104103rspcev 2995 . . . . . . . . . . . 12  |-  ( (
(/)  e.  ( ~P U  i^i  Fin )  /\  (/)  C_  U. (/) )  ->  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
)
105100, 101, 104mp2an 654 . . . . . . . . . . 11  |-  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
106 0ex 4280 . . . . . . . . . . . . 13  |-  (/)  e.  _V
107 sseq1 3312 . . . . . . . . . . . . . . 15  |-  ( u  =  (/)  ->  ( u 
C_  U. v  <->  (/)  C_  U. v
) )
108107rexbidv 2670 . . . . . . . . . . . . . 14  |-  ( u  =  (/)  ->  ( E. v  e.  ( ~P U  i^i  Fin )
u  C_  U. v  <->  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v ) )
109108notbid 286 . . . . . . . . . . . . 13  |-  ( u  =  (/)  ->  ( -. 
E. v  e.  ( ~P U  i^i  Fin ) u  C_  U. v  <->  -. 
E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
) )
110106, 109, 17elab2 3028 . . . . . . . . . . . 12  |-  ( (/)  e.  K  <->  -.  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
)
111110con2bii 323 . . . . . . . . . . 11  |-  ( E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v  <->  -.  (/)  e.  K
)
112105, 111mpbi 200 . . . . . . . . . 10  |-  -.  (/)  e.  K
113 nelne2 2640 . . . . . . . . . 10  |-  ( ( ( ( ( S `
 k ) B k )  i^i  (
( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K  /\  -.  (/)  e.  K )  ->  ( ( ( S `  k ) B k )  i^i  ( ( ( S `
 k ) T k ) B ( k  +  1 ) ) )  =/=  (/) )
11496, 112, 113sylancl 644 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  =/=  (/) )
11595, 114eqnetrrd 2570 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  i^i  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )  =/=  (/) )
11651rpreccld 10590 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ k ) )  e.  RR+ )
117116adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e.  RR+ )
118117rpred 10580 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e.  RR )
11945rpreccld 10590 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR+ )
120119adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR+ )
121120rpred 10580 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR )
122 rexadd 10750 . . . . . . . . . . . 12  |-  ( ( ( 1  /  (
2 ^ k ) )  e.  RR  /\  ( 1  /  (
2 ^ ( k  +  1 ) ) )  e.  RR )  ->  ( ( 1  /  ( 2 ^ k ) ) + e ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
123118, 121, 122syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) ) + e ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  =  ( ( 1  /  ( 2 ^ k ) )  +  ( 1  /  (
2 ^ ( k  +  1 ) ) ) ) )
124123breq1d 4163 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( 1  /  (
2 ^ k ) ) + e ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `  k ) D ( ( S `
 k ) T k ) )  <->  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  <_ 
( ( S `  k ) D ( ( S `  k
) T k ) ) ) )
125117rpxrd 10581 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e. 
RR* )
126120rpxrd 10581 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e. 
RR* )
127 bldisj 18329 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( S `  k )  e.  X  /\  ( ( S `  k ) T k )  e.  X )  /\  ( ( 1  /  ( 2 ^ k ) )  e. 
RR*  /\  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e. 
RR*  /\  ( (
1  /  ( 2 ^ k ) ) + e ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `
 k ) D ( ( S `  k ) T k ) ) ) )  ->  ( ( ( S `  k ) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  i^i  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )  =  (/) )
1281273exp2 1171 . . . . . . . . . . . 12  |-  ( ( D  e.  ( * Met `  X )  /\  ( S `  k )  e.  X  /\  ( ( S `  k ) T k )  e.  X )  ->  ( ( 1  /  ( 2 ^ k ) )  e. 
RR*  ->  ( ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e. 
RR*  ->  ( ( ( 1  /  ( 2 ^ k ) ) + e ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `
 k ) D ( ( S `  k ) T k ) )  ->  (
( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) )  i^i  ( ( ( S `  k ) T k ) (
ball `  D )
( 1  /  (
2 ^ ( k  +  1 ) ) ) ) )  =  (/) ) ) ) )
129128imp32 423 . . . . . . . . . . 11  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( S `  k )  e.  X  /\  ( ( S `  k ) T k )  e.  X )  /\  ( ( 1  /  ( 2 ^ k ) )  e. 
RR*  /\  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e. 
RR* ) )  -> 
( ( ( 1  /  ( 2 ^ k ) ) + e ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  <_ 
( ( S `  k ) D ( ( S `  k
) T k ) )  ->  ( (
( S `  k
) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  i^i  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )  =  (/) ) )
1307, 40, 86, 125, 126, 129syl32anc 1192 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( 1  /  (
2 ^ k ) ) + e ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `  k ) D ( ( S `
 k ) T k ) )  -> 
( ( ( S `
 k ) (
ball `  D )
( 1  /  (
2 ^ k ) ) )  i^i  (
( ( S `  k ) T k ) ( ball `  D
) ( 1  / 
( 2 ^ (
k  +  1 ) ) ) ) )  =  (/) ) )
131124, 130sylbird 227 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( 1  /  (
2 ^ k ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `
 k ) D ( ( S `  k ) T k ) )  ->  (
( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) )  i^i  ( ( ( S `  k ) T k ) (
ball `  D )
( 1  /  (
2 ^ ( k  +  1 ) ) ) ) )  =  (/) ) )
132131necon3ad 2586 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) )  i^i  ( ( ( S `  k ) T k ) (
ball `  D )
( 1  /  (
2 ^ ( k  +  1 ) ) ) ) )  =/=  (/)  ->  -.  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  <_ 
( ( S `  k ) D ( ( S `  k
) T k ) ) ) )
133115, 132mpd 15 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  -.  (
( 1  /  (
2 ^ k ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `
 k ) D ( ( S `  k ) T k ) ) )
134117, 120rpaddcld 10595 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e.  RR+ )
135134rpred 10580 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e.  RR )
1364adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  D  e.  ( Met `  X ) )
137 metcl 18271 . . . . . . . . . 10  |-  ( ( D  e.  ( Met `  X )  /\  ( S `  k )  e.  X  /\  (
( S `  k
) T k )  e.  X )  -> 
( ( S `  k ) D ( ( S `  k
) T k ) )  e.  RR )
138136, 40, 86, 137syl3anc 1184 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) D ( ( S `
 k ) T k ) )  e.  RR )
139135, 138letrid 9155 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( 1  /  (
2 ^ k ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `
 k ) D ( ( S `  k ) T k ) )  \/  (
( S `  k
) D ( ( S `  k ) T k ) )  <_  ( ( 1  /  ( 2 ^ k ) )  +  ( 1  /  (
2 ^ ( k  +  1 ) ) ) ) ) )
140139ord 367 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( -.  ( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `  k ) D ( ( S `
 k ) T k ) )  -> 
( ( S `  k ) D ( ( S `  k
) T k ) )  <_  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) ) ) )
141133, 140mpd 15 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) D ( ( S `
 k ) T k ) )  <_ 
( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
142 seqp1 11265 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  0
)  ->  (  seq  0 ( T , 
( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  ( k  +  1 ) )  =  ( (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  k
) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) ) )
143 nn0uz 10452 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
144142, 143eleq2s 2479 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  (  seq  0 ( T , 
( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  ( k  +  1 ) )  =  ( (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  k
) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) ) )
14523fveq1i 5669 . . . . . . . . . . 11  |-  ( S `
 ( k  +  1 ) )  =  (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  (
k  +  1 ) )
14623fveq1i 5669 . . . . . . . . . . . 12  |-  ( S `
 k )  =  (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  k
)
147146oveq1i 6030 . . . . . . . . . . 11  |-  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) )  =  ( (  seq  0 ( T ,  ( m  e. 
NN0  |->  if ( m  =  0 ,  C ,  ( m  - 
1 ) ) ) ) `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) )
148144, 145, 1473eqtr4g 2444 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  (
k  +  1 ) ) ) )
149 nn0p1nn 10191 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  NN )
150 nnne0 9964 . . . . . . . . . . . . . . . . 17  |-  ( ( k  +  1 )  e.  NN  ->  (
k  +  1 )  =/=  0 )
151150neneqd 2566 . . . . . . . . . . . . . . . 16  |-  ( ( k  +  1 )  e.  NN  ->  -.  ( k  +  1 )  =  0 )
152149, 151syl 16 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  -.  (
k  +  1 )  =  0 )
153 iffalse 3689 . . . . . . . . . . . . . . 15  |-  ( -.  ( k  +  1 )  =  0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  =  ( ( k  +  1 )  -  1 ) )
154152, 153syl 16 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  =  ( ( k  +  1 )  - 
1 ) )
155 ovex 6045 . . . . . . . . . . . . . 14  |-  ( ( k  +  1 )  -  1 )  e. 
_V
156154, 155syl6eqel 2475 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  e.  _V )
157 eqeq1 2393 . . . . . . . . . . . . . . 15  |-  ( m  =  ( k  +  1 )  ->  (
m  =  0  <->  (
k  +  1 )  =  0 ) )
158 oveq1 6027 . . . . . . . . . . . . . . 15  |-  ( m  =  ( k  +  1 )  ->  (
m  -  1 )  =  ( ( k  +  1 )  - 
1 ) )
159157, 158ifbieq2d 3702 . . . . . . . . . . . . . 14  |-  ( m  =  ( k  +  1 )  ->  if ( m  =  0 ,  C ,  ( m  -  1 ) )  =  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  - 
1 ) ) )
160 eqid 2387 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) )  =  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) )
161159, 160fvmptg 5743 . . . . . . . . . . . . 13  |-  ( ( ( k  +  1 )  e.  NN0  /\  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  e.  _V )  ->  ( ( m  e. 
NN0  |->  if ( m  =  0 ,  C ,  ( m  - 
1 ) ) ) `
 ( k  +  1 ) )  =  if ( ( k  +  1 )  =  0 ,  C , 
( ( k  +  1 )  -  1 ) ) )
16212, 156, 161syl2anc 643 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) )  =  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  - 
1 ) ) )
163 nn0cn 10163 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  k  e.  CC )
164 ax-1cn 8981 . . . . . . . . . . . . 13  |-  1  e.  CC
165 pncan 9243 . . . . . . . . . . . . 13  |-  ( ( k  e.  CC  /\  1  e.  CC )  ->  ( ( k  +  1 )  -  1 )  =  k )
166163, 164, 165sylancl 644 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( ( k  +  1 )  -  1 )  =  k )
167162, 154, 1663eqtrd 2423 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) )  =  k )
168167oveq2d 6036 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) )  =  ( ( S `  k ) T k ) )
169148, 168eqtrd 2419 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k ) T k ) )
170169adantl 453 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  =  ( ( S `  k
) T k ) )
171170oveq1d 6035 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  =  ( ( ( S `
 k ) T k ) D ( S `  k ) ) )
172 metsym 18288 . . . . . . . 8  |-  ( ( D  e.  ( Met `  X )  /\  (
( S `  k
) T k )  e.  X  /\  ( S `  k )  e.  X )  ->  (
( ( S `  k ) T k ) D ( S `
 k ) )  =  ( ( S `
 k ) D ( ( S `  k ) T k ) ) )
173136, 86, 40, 172syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) T k ) D ( S `  k ) )  =  ( ( S `  k ) D ( ( S `  k
) T k ) ) )
174171, 173eqtrd 2419 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  =  ( ( S `  k ) D ( ( S `  k
) T k ) ) )
175 3cn 10004 . . . . . . . . . . . . 13  |-  3  e.  CC
1761752timesi 10033 . . . . . . . . . . . 12  |-  ( 2  x.  3 )  =  ( 3  +  3 )
177176oveq1i 6030 . . . . . . . . . . 11  |-  ( ( 2  x.  3 )  -  3 )  =  ( ( 3  +  3 )  -  3 )
178 pncan 9243 . . . . . . . . . . . 12  |-  ( ( 3  e.  CC  /\  3  e.  CC )  ->  ( ( 3  +  3 )  -  3 )  =  3 )
179175, 175, 178mp2an 654 . . . . . . . . . . 11  |-  ( ( 3  +  3 )  -  3 )  =  3
180 df-3 9991 . . . . . . . . . . 11  |-  3  =  ( 2  +  1 )
181177, 179, 1803eqtri 2411 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  -  3 )  =  ( 2  +  1 )
182181oveq1i 6030 . . . . . . . . 9  |-  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  +  1 )  /  (
2 ^ ( k  +  1 ) ) )
183 rpcn 10552 . . . . . . . . . . 11  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( 2 ^ ( k  +  1 ) )  e.  CC )
184 rpne0 10559 . . . . . . . . . . 11  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( 2 ^ ( k  +  1 ) )  =/=  0 )
185 2cn 10002 . . . . . . . . . . . . 13  |-  2  e.  CC
186185, 175mulcli 9028 . . . . . . . . . . . 12  |-  ( 2  x.  3 )  e.  CC
187 divsubdir 9642 . . . . . . . . . . . 12  |-  ( ( ( 2  x.  3 )  e.  CC  /\  3  e.  CC  /\  (
( 2 ^ (
k  +  1 ) )  e.  CC  /\  ( 2 ^ (
k  +  1 ) )  =/=  0 ) )  ->  ( (
( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
188186, 175, 187mp3an12 1269 . . . . . . . . . . 11  |-  ( ( ( 2 ^ (
k  +  1 ) )  e.  CC  /\  ( 2 ^ (
k  +  1 ) )  =/=  0 )  ->  ( ( ( 2  x.  3 )  -  3 )  / 
( 2 ^ (
k  +  1 ) ) )  =  ( ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) )  -  ( 3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
189183, 184, 188syl2anc 643 . . . . . . . . . 10  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
19045, 189syl 16 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
191 divdir 9633 . . . . . . . . . . . 12  |-  ( ( 2  e.  CC  /\  1  e.  CC  /\  (
( 2 ^ (
k  +  1 ) )  e.  CC  /\  ( 2 ^ (
k  +  1 ) )  =/=  0 ) )  ->  ( (
2  +  1 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
192185, 164, 191mp3an12 1269 . . . . . . . . . . 11  |-  ( ( ( 2 ^ (
k  +  1 ) )  e.  CC  /\  ( 2 ^ (
k  +  1 ) )  =/=  0 )  ->  ( ( 2  +  1 )  / 
( 2 ^ (
k  +  1 ) ) )  =  ( ( 2  /  (
2 ^ ( k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
193183, 184, 192syl2anc 643 . . . . . . . . . 10  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( ( 2  +  1 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
19445, 193syl 16 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( ( 2  +  1 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
195182, 190, 1943eqtr3a 2443 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  3 )  /  ( 2 ^ ( k  +  1 ) ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
196 rpcn 10552 . . . . . . . . . . . 12  |-  ( ( 2 ^ k )  e.  RR+  ->  ( 2 ^ k )  e.  CC )
197 rpne0 10559 . . . . . . . . . . . 12  |-  ( ( 2 ^ k )  e.  RR+  ->  ( 2 ^ k )  =/=  0 )
198 2ne0 10015 . . . . . . . . . . . . . 14  |-  2  =/=  0
199185, 198pm3.2i 442 . . . . . . . . . . . . 13  |-  ( 2  e.  CC  /\  2  =/=  0 )
200 divcan5 9648 . . . . . . . . . . . . 13  |-  ( ( 3  e.  CC  /\  ( ( 2 ^ k )  e.  CC  /\  ( 2 ^ k
)  =/=  0 )  /\  ( 2  e.  CC  /\  2  =/=  0 ) )  -> 
( ( 2  x.  3 )  /  (
2  x.  ( 2 ^ k ) ) )  =  ( 3  /  ( 2 ^ k ) ) )
201175, 199, 200mp3an13 1270 . . . . . . . . . . . 12  |-  ( ( ( 2 ^ k
)  e.  CC  /\  ( 2 ^ k
)  =/=  0 )  ->  ( ( 2  x.  3 )  / 
( 2  x.  (
2 ^ k ) ) )  =  ( 3  /  ( 2 ^ k ) ) )
202196, 197, 201syl2anc 643 . . . . . . . . . . 11  |-  ( ( 2 ^ k )  e.  RR+  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 3  /  (
2 ^ k ) ) )
20351, 202syl 16 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 3  /  (
2 ^ k ) ) )
20451, 196syl 16 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  CC )
205 mulcom 9009 . . . . . . . . . . . . 13  |-  ( ( 2  e.  CC  /\  ( 2 ^ k
)  e.  CC )  ->  ( 2  x.  ( 2 ^ k
) )  =  ( ( 2 ^ k
)  x.  2 ) )
206185, 204, 205sylancr 645 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( 2  x.  ( 2 ^ k ) )  =  ( ( 2 ^ k )  x.  2 ) )
207 expp1 11315 . . . . . . . . . . . . 13  |-  ( ( 2  e.  CC  /\  k  e.  NN0 )  -> 
( 2 ^ (
k  +  1 ) )  =  ( ( 2 ^ k )  x.  2 ) )
208185, 207mpan 652 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  =  ( ( 2 ^ k )  x.  2 ) )
209206, 208eqtr4d 2422 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( 2  x.  ( 2 ^ k ) )  =  ( 2 ^ (
k  +  1 ) ) )
210209oveq2d 6036 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) ) )
211203, 210eqtr3d 2421 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( 3  /  ( 2 ^ k ) )  =  ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) ) )
212211oveq1d 6035 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
213 divcan5 9648 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  ( ( 2 ^ k )  e.  CC  /\  ( 2 ^ k
)  =/=  0 )  /\  ( 2  e.  CC  /\  2  =/=  0 ) )  -> 
( ( 2  x.  1 )  /  (
2  x.  ( 2 ^ k ) ) )  =  ( 1  /  ( 2 ^ k ) ) )
214164, 199, 213mp3an13 1270 . . . . . . . . . . . 12  |-  ( ( ( 2 ^ k
)  e.  CC  /\  ( 2 ^ k
)  =/=  0 )  ->  ( ( 2  x.  1 )  / 
( 2  x.  (
2 ^ k ) ) )  =  ( 1  /  ( 2 ^ k ) ) )
215196, 197, 214syl2anc 643 . . . . . . . . . . 11  |-  ( ( 2 ^ k )  e.  RR+  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 1  /  (
2 ^ k ) ) )
21651, 215syl 16 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 1  /  (
2 ^ k ) ) )
217185mulid1i 9025 . . . . . . . . . . . 12  |-  ( 2  x.  1 )  =  2
218217a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( 2  x.  1 )  =  2 )
219218, 209oveq12d 6038 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 2  /  (
2 ^ ( k  +  1 ) ) ) )
220216, 219eqtr3d 2421 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ k ) )  =  ( 2  /  (
2 ^ ( k  +  1 ) ) ) )
221220oveq1d 6035 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
222195, 212, 2213eqtr4d 2429 . . . . . . 7  |-  ( k  e.  NN0  ->  ( ( 3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
223222adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
224141, 174, 2233brtr4d 4183 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  <_ 
( ( 3  / 
( 2 ^ k
) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
225 blss2 18333 . . . . 5  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( S `  ( k  +  1 ) )  e.  X  /\  ( S `  k
)  e.  X )  /\  ( ( 3  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR  /\  ( 3  /  ( 2 ^ k ) )  e.  RR  /\  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  <_ 
( ( 3  / 
( 2 ^ k
) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) ) )  -> 
( ( S `  ( k  +  1 ) ) ( ball `  D ) ( 3  /  ( 2 ^ ( k  +  1 ) ) ) ) 
C_  ( ( S `
 k ) (
ball `  D )
( 3  /  (
2 ^ k ) ) ) )
2267, 31, 40, 48, 54, 224, 225syl33anc 1199 . . . 4  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  C_  ( ( S `  k ) ( ball `  D ) ( 3  /  ( 2 ^ k ) ) ) )
2271, 226sylan2 461 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  C_  ( ( S `  k ) ( ball `  D ) ( 3  /  ( 2 ^ k ) ) ) )
228 peano2nn 9944 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
229 fveq2 5668 . . . . . . . . 9  |-  ( n  =  ( k  +  1 )  ->  ( S `  n )  =  ( S `  ( k  +  1 ) ) )
230 oveq2 6028 . . . . . . . . . 10  |-  ( n  =  ( k  +  1 )  ->  (
2 ^ n )  =  ( 2 ^ ( k  +  1 ) ) )
231230oveq2d 6036 . . . . . . . . 9  |-  ( n  =  ( k  +  1 )  ->  (
3  /  ( 2 ^ n ) )  =  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )
232229, 231opeq12d 3934 . . . . . . . 8  |-  ( n  =  ( k  +  1 )  ->  <. ( S `  n ) ,  ( 3  / 
( 2 ^ n
) ) >.  =  <. ( S `  ( k  +  1 ) ) ,  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) >. )
233 heibor.12 . . . . . . . 8  |-  M  =  ( n  e.  NN  |->  <. ( S `  n
) ,  ( 3  /  ( 2 ^ n ) ) >.
)
234 opex 4368 . . . . . . . 8  |-  <. ( S `  ( k  +  1 ) ) ,  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) >.  e.  _V
235232, 233, 234fvmpt 5745 . . . . . . 7  |-  ( ( k  +  1 )  e.  NN  ->  ( M `  ( k  +  1 ) )  =  <. ( S `  ( k  +  1 ) ) ,  ( 3  /  ( 2 ^ ( k  +  1 ) ) )
>. )
236228, 235syl 16 . . . . . 6  |-  ( k  e.  NN  ->  ( M `  ( k  +  1 ) )  =  <. ( S `  ( k  +  1 ) ) ,  ( 3  /  ( 2 ^ ( k  +  1 ) ) )
>. )
237236adantl 453 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( M `
 ( k  +  1 ) )  = 
<. ( S `  (
k  +  1 ) ) ,  ( 3  /  ( 2 ^ ( k  +  1 ) ) ) >.
)
238237fveq2d 5672 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  =  ( ( ball `  D
) `  <. ( S `
 ( k  +  1 ) ) ,  ( 3  /  (
2 ^ ( k  +  1 ) ) ) >. ) )
239 df-ov 6023 . . . 4  |-  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( ball `  D
) `  <. ( S `
 ( k  +  1 ) ) ,  ( 3  /  (
2 ^ ( k  +  1 ) ) ) >. )
240238, 239syl6eqr 2437 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) ) )
241 fveq2 5668 . . . . . . . 8  |-  ( n  =  k  ->  ( S `  n )  =  ( S `  k ) )
242 oveq2 6028 . . . . . . . . 9  |-  ( n  =  k  ->  (
2 ^ n )  =  ( 2 ^ k ) )
243242oveq2d 6036 . . . . . . . 8  |-  ( n  =  k  ->  (
3  /  ( 2 ^ n ) )  =  ( 3  / 
( 2 ^ k
) ) )
244241, 243opeq12d 3934 . . . . . . 7  |-  ( n  =  k  ->  <. ( S `  n ) ,  ( 3  / 
( 2 ^ n
) ) >.  =  <. ( S `  k ) ,  ( 3  / 
( 2 ^ k
) ) >. )
245 opex 4368 . . . . . . 7  |-  <. ( S `  k ) ,  ( 3  / 
( 2 ^ k
) ) >.  e.  _V
246244, 233, 245fvmpt 5745 . . . . . 6  |-  ( k  e.  NN  ->  ( M `  k )  =  <. ( S `  k ) ,  ( 3  /  ( 2 ^ k ) )
>. )
247246fveq2d 5672 . . . . 5  |-  ( k  e.  NN  ->  (
( ball `  D ) `  ( M `  k
) )  =  ( ( ball `  D
) `  <. ( S `
 k ) ,  ( 3  /  (
2 ^ k ) ) >. ) )
248 df-ov 6023 . . . . 5  |-  ( ( S `  k ) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) )  =  ( ( ball `  D
) `  <. ( S `
 k ) ,  ( 3  /  (
2 ^ k ) ) >. )
249247, 248syl6eqr 2437 . . . 4  |-  ( k  e.  NN  ->  (
( ball `  D ) `  ( M `  k
) )  =  ( ( S `  k
) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) ) )
250249adantl 453 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  k
) )  =  ( ( S `  k
) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) ) )
251227, 240, 2503sstr4d 3334 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  C_  (
( ball `  D ) `  ( M `  k
) ) )
252251ralrimiva 2732 1  |-  ( ph  ->  A. k  e.  NN  ( ( ball `  D
) `  ( M `  ( k  +  1 ) ) )  C_  ( ( ball `  D
) `  ( M `  k ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1717   {cab 2373    =/= wne 2550   A.wral 2649   E.wrex 2650   _Vcvv 2899    i^i cin 3262    C_ wss 3263   (/)c0 3571   ifcif 3682   ~Pcpw 3742   <.cop 3760   U.cuni 3957   U_ciun 4035   class class class wbr 4153   {copab 4206    e. cmpt 4207   -->wf 5390   ` cfv 5394  (class class class)co 6020    e. cmpt2 6022   2ndc2nd 6287   Fincfn 7045   CCcc 8921   RRcr 8922   0cc0 8923   1c1 8924    + caddc 8926    x. cmul 8928   RR*cxr 9052    <_ cle 9054    - cmin 9223    / cdiv 9609   NNcn 9932   2c2 9981   3c3 9982   NN0cn0 10153   ZZ>=cuz 10420   RR+crp 10544   + ecxad 10640    seq cseq 11250   ^cexp 11309   * Metcxmt 16612   Metcme 16613   ballcbl 16614   MetOpencmopn 16617   CMetcms 19078
This theorem is referenced by:  heiborlem8  26218  heiborlem9  26219
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-cnex 8979  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-1st 6288  df-2nd 6289  df-riota 6485  df-recs 6569  df-rdg 6604  df-er 6841  df-map 6956  df-en 7046  df-dom 7047  df-sdom 7048  df-fin 7049  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-div 9610  df-nn 9933  df-2 9990  df-3 9991  df-n0 10154  df-z 10215  df-uz 10421  df-rp 10545  df-xneg 10642  df-xadd 10643  df-xmul 10644  df-seq 11251  df-exp 11310  df-xmet 16619  df-met 16620  df-bl 16621  df-cmet 19081
  Copyright terms: Public domain W3C validator