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

Theorem heiborlem6 26415
Description: Lemma for heibor 26420. 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 10184 . . . 4  |-  ( k  e.  NN  ->  k  e.  NN0 )
2 heibor.6 . . . . . . . 8  |-  ( ph  ->  D  e.  ( CMet `  X ) )
3 cmetmet 19192 . . . . . . . 8  |-  ( D  e.  ( CMet `  X
)  ->  D  e.  ( Met `  X ) )
42, 3syl 16 . . . . . . 7  |-  ( ph  ->  D  e.  ( Met `  X ) )
5 metxmet 18317 . . . . . . 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 3521 . . . . . . . . 9  |-  ( ~P X  i^i  Fin )  C_ 
~P X
10 fss 5558 . . . . . . . . 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 10216 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
13 ffvelrn 5827 . . . . . . . 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 3768 . . . . . 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 26413 . . . . . . . 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 5701 . . . . . . . . 9  |-  ( S `
 ( k  +  1 ) )  e. 
_V
27 ovex 6065 . . . . . . . . 9  |-  ( k  +  1 )  e. 
_V
2816, 17, 18, 26, 27heiborlem2 26411 . . . . . . . 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 3309 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  e.  X
)
3211ffvelrnda 5829 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  e.  ~P X )
3332elpwid 3768 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  C_  X
)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 26413 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k ) G k )
35 fvex 5701 . . . . . . . . 9  |-  ( S `
 k )  e. 
_V
36 vex 2919 . . . . . . . . 9  |-  k  e. 
_V
3716, 17, 18, 35, 36heiborlem2 26411 . . . . . . . 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 3309 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k )  e.  X
)
41 3re 10027 . . . . . 6  |-  3  e.  RR
42 2nn 10089 . . . . . . . . 9  |-  2  e.  NN
43 nnexpcl 11349 . . . . . . . . 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 10603 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  e.  RR+ )
4645adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2 ^ ( k  +  1 ) )  e.  RR+ )
47 rerpdivcl 10595 . . . . . 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 11349 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  k  e.  NN0 )  -> 
( 2 ^ k
)  e.  NN )
5042, 49mpan 652 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  NN )
5150nnrpd 10603 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  RR+ )
5251adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2 ^ k )  e.  RR+ )
53 rerpdivcl 10595 . . . . . 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 6047 . . . . . . . . . . . 12  |-  ( z  =  ( S `  k )  ->  (
z ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
56 oveq2 6048 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
2 ^ m )  =  ( 2 ^ k ) )
5756oveq2d 6056 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  (
1  /  ( 2 ^ m ) )  =  ( 1  / 
( 2 ^ k
) ) )
5857oveq2d 6056 . . . . . . . . . . . 12  |-  ( m  =  k  ->  (
( S `  k
) ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) ) )
59 ovex 6065 . . . . . . . . . . . 12  |-  ( ( S `  k ) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  e. 
_V
6055, 58, 19, 59ovmpt2 6168 . . . . . . . . . . 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 4173 . . . . . . . . . . . . . . . . 17  |-  ( ( S `  k ) G k  <->  <. ( S `
 k ) ,  k >.  e.  G
)
63 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( T `  x )  =  ( T `  <. ( S `  k ) ,  k >. )
)
64 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S `  k ) T k )  =  ( T `  <. ( S `  k ) ,  k >. )
6563, 64syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( T `  x )  =  ( ( S `  k
) T k ) )
6635, 36op2ndd 6317 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( 2nd `  x
)  =  k )
6766oveq1d 6055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( 2nd `  x )  +  1 )  =  ( k  +  1 ) )
6865, 67breq12d 4185 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( T `
 x ) G ( ( 2nd `  x
)  +  1 )  <-> 
( ( S `  k ) T k ) G ( k  +  1 ) ) )
69 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( B `  x )  =  ( B `  <. ( S `  k ) ,  k >. )
)
70 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S `  k ) B k )  =  ( B `  <. ( S `  k ) ,  k >. )
7169, 70syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( B `  x )  =  ( ( S `  k
) B k ) )
7265, 67oveq12d 6058 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( T `
 x ) B ( ( 2nd `  x
)  +  1 ) )  =  ( ( ( S `  k
) T k ) B ( k  +  1 ) ) )
7371, 72ineq12d 3503 . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . 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 3009 . . . . . . . . . . . . . . . . . 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 6065 . . . . . . . . . . . . . . 15  |-  ( ( S `  k ) T k )  e. 
_V
8316, 17, 18, 82, 27heiborlem2 26411 . . . . . . . . . . . . . 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 3309 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k )  e.  X )
8712adantl 453 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( k  +  1 )  e. 
NN0 )
88 oveq1 6047 . . . . . . . . . . . 12  |-  ( z  =  ( ( S `
 k ) T k )  ->  (
z ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
89 oveq2 6048 . . . . . . . . . . . . . 14  |-  ( m  =  ( k  +  1 )  ->  (
2 ^ m )  =  ( 2 ^ ( k  +  1 ) ) )
9089oveq2d 6056 . . . . . . . . . . . . 13  |-  ( m  =  ( k  +  1 )  ->  (
1  /  ( 2 ^ m ) )  =  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )
9190oveq2d 6056 . . . . . . . . . . . 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 6065 . . . . . . . . . . . 12  |-  ( ( ( S `  k
) T k ) ( ball `  D
) ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e. 
_V
9388, 91, 19, 92ovmpt2 6168 . . . . . . . . . . 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 3503 . . . . . . . . 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 4329 . . . . . . . . . . . . 13  |-  (/)  e.  ~P U
98 0fin 7295 . . . . . . . . . . . . 13  |-  (/)  e.  Fin
99 elin 3490 . . . . . . . . . . . . 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 3616 . . . . . . . . . . . 12  |-  (/)  C_  U. (/)
102 unieq 3984 . . . . . . . . . . . . . 14  |-  ( v  =  (/)  ->  U. v  =  U. (/) )
103102sseq2d 3336 . . . . . . . . . . . . 13  |-  ( v  =  (/)  ->  ( (/)  C_ 
U. v  <->  (/)  C_  U. (/) ) )
104103rspcev 3012 . . . . . . . . . . . 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 4299 . . . . . . . . . . . . 13  |-  (/)  e.  _V
107 sseq1 3329 . . . . . . . . . . . . . . 15  |-  ( u  =  (/)  ->  ( u 
C_  U. v  <->  (/)  C_  U. v
) )
108107rexbidv 2687 . . . . . . . . . . . . . 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 3045 . . . . . . . . . . . 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 2657 . . . . . . . . . 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 2587 . . . . . . . 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 10614 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ k ) )  e.  RR+ )
117116adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e.  RR+ )
118117rpred 10604 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e.  RR )
11945rpreccld 10614 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR+ )
120119adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR+ )
121120rpred 10604 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR )
122 rexadd 10774 . . . . . . . . . . . 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 4182 . . . . . . . . . 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 10605 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e. 
RR* )
126120rpxrd 10605 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e. 
RR* )
127 bldisj 18381 . . . . . . . . . . . . 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 2603 . . . . . . . 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 10619 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e.  RR+ )
135134rpred 10604 . . . . . . . . 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 18315 . . . . . . . . . 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 9179 . . . . . . . 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 11293 . . . . . . . . . . . 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 10476 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
144142, 143eleq2s 2496 . . . . . . . . . . 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 5688 . . . . . . . . . . 11  |-  ( S `
 ( k  +  1 ) )  =  (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  (
k  +  1 ) )
14623fveq1i 5688 . . . . . . . . . . . 12  |-  ( S `
 k )  =  (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  k
)
147146oveq1i 6050 . . . . . . . . . . 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 2461 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  (
k  +  1 ) ) ) )
149 nn0p1nn 10215 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  NN )
150 nnne0 9988 . . . . . . . . . . . . . . . . 17  |-  ( ( k  +  1 )  e.  NN  ->  (
k  +  1 )  =/=  0 )
151150neneqd 2583 . . . . . . . . . . . . . . . 16  |-  ( ( k  +  1 )  e.  NN  ->  -.  ( k  +  1 )  =  0 )
152149, 151syl 16 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  -.  (
k  +  1 )  =  0 )
153 iffalse 3706 . . . . . . . . . . . . . . 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 6065 . . . . . . . . . . . . . 14  |-  ( ( k  +  1 )  -  1 )  e. 
_V
156154, 155syl6eqel 2492 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  e.  _V )
157 eqeq1 2410 . . . . . . . . . . . . . . 15  |-  ( m  =  ( k  +  1 )  ->  (
m  =  0  <->  (
k  +  1 )  =  0 ) )
158 oveq1 6047 . . . . . . . . . . . . . . 15  |-  ( m  =  ( k  +  1 )  ->  (
m  -  1 )  =  ( ( k  +  1 )  - 
1 ) )
159157, 158ifbieq2d 3719 . . . . . . . . . . . . . 14  |-  ( m  =  ( k  +  1 )  ->  if ( m  =  0 ,  C ,  ( m  -  1 ) )  =  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  - 
1 ) ) )
160 eqid 2404 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) )  =  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) )
161159, 160fvmptg 5763 . . . . . . . . . . . . 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 10187 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  k  e.  CC )
164 ax-1cn 9004 . . . . . . . . . . . . 13  |-  1  e.  CC
165 pncan 9267 . . . . . . . . . . . . 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 2440 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) )  =  k )
168167oveq2d 6056 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) )  =  ( ( S `  k ) T k ) )
169148, 168eqtrd 2436 . . . . . . . . 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 6055 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  =  ( ( ( S `
 k ) T k ) D ( S `  k ) ) )
172 metsym 18333 . . . . . . . 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 2436 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  =  ( ( S `  k ) D ( ( S `  k
) T k ) ) )
175 3cn 10028 . . . . . . . . . . . . 13  |-  3  e.  CC
1761752timesi 10057 . . . . . . . . . . . 12  |-  ( 2  x.  3 )  =  ( 3  +  3 )
177176oveq1i 6050 . . . . . . . . . . 11  |-  ( ( 2  x.  3 )  -  3 )  =  ( ( 3  +  3 )  -  3 )
178 pncan 9267 . . . . . . . . . . . 12  |-  ( ( 3  e.  CC  /\  3  e.  CC )  ->  ( ( 3  +  3 )  -  3 )  =  3 )
179175, 175, 178mp2an 654 . . . . . . . . . . 11  |-  ( ( 3  +  3 )  -  3 )  =  3
180 df-3 10015 . . . . . . . . . . 11  |-  3  =  ( 2  +  1 )
181177, 179, 1803eqtri 2428 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  -  3 )  =  ( 2  +  1 )
182181oveq1i 6050 . . . . . . . . 9  |-  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  +  1 )  /  (
2 ^ ( k  +  1 ) ) )
183 rpcn 10576 . . . . . . . . . . 11  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( 2 ^ ( k  +  1 ) )  e.  CC )
184 rpne0 10583 . . . . . . . . . . 11  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( 2 ^ ( k  +  1 ) )  =/=  0 )
185 2cn 10026 . . . . . . . . . . . . 13  |-  2  e.  CC
186185, 175mulcli 9051 . . . . . . . . . . . 12  |-  ( 2  x.  3 )  e.  CC
187 divsubdir 9666 . . . . . . . . . . . 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 9657 . . . . . . . . . . . 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 2460 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  3 )  /  ( 2 ^ ( k  +  1 ) ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
196 rpcn 10576 . . . . . . . . . . . 12  |-  ( ( 2 ^ k )  e.  RR+  ->  ( 2 ^ k )  e.  CC )
197 rpne0 10583 . . . . . . . . . . . 12  |-  ( ( 2 ^ k )  e.  RR+  ->  ( 2 ^ k )  =/=  0 )
198 2ne0 10039 . . . . . . . . . . . . . 14  |-  2  =/=  0
199185, 198pm3.2i 442 . . . . . . . . . . . . 13  |-  ( 2  e.  CC  /\  2  =/=  0 )
200 divcan5 9672 . . . . . . . . . . . . 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 9032 . . . . . . . . . . . . 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 11343 . . . . . . . . . . . . 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 2439 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( 2  x.  ( 2 ^ k ) )  =  ( 2 ^ (
k  +  1 ) ) )
210209oveq2d 6056 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) ) )
211203, 210eqtr3d 2438 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( 3  /  ( 2 ^ k ) )  =  ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) ) )
212211oveq1d 6055 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
213 divcan5 9672 . . . . . . . . . . . . 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 9048 . . . . . . . . . . . 12  |-  ( 2  x.  1 )  =  2
218217a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( 2  x.  1 )  =  2 )
219218, 209oveq12d 6058 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 2  /  (
2 ^ ( k  +  1 ) ) ) )
220216, 219eqtr3d 2438 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ k ) )  =  ( 2  /  (
2 ^ ( k  +  1 ) ) ) )
221220oveq1d 6055 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
222195, 212, 2213eqtr4d 2446 . . . . . . 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 4202 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  <_ 
( ( 3  / 
( 2 ^ k
) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
225 blss2 18387 . . . . 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 9968 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
229 fveq2 5687 . . . . . . . . 9  |-  ( n  =  ( k  +  1 )  ->  ( S `  n )  =  ( S `  ( k  +  1 ) ) )
230 oveq2 6048 . . . . . . . . . 10  |-  ( n  =  ( k  +  1 )  ->  (
2 ^ n )  =  ( 2 ^ ( k  +  1 ) ) )
231230oveq2d 6056 . . . . . . . . 9  |-  ( n  =  ( k  +  1 )  ->  (
3  /  ( 2 ^ n ) )  =  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )
232229, 231opeq12d 3952 . . . . . . . 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 4387 . . . . . . . 8  |-  <. ( S `  ( k  +  1 ) ) ,  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) >.  e.  _V
235232, 233, 234fvmpt 5765 . . . . . . 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 5691 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  =  ( ( ball `  D
) `  <. ( S `
 ( k  +  1 ) ) ,  ( 3  /  (
2 ^ ( k  +  1 ) ) ) >. ) )
239 df-ov 6043 . . . 4  |-  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( ball `  D
) `  <. ( S `
 ( k  +  1 ) ) ,  ( 3  /  (
2 ^ ( k  +  1 ) ) ) >. )
240238, 239syl6eqr 2454 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) ) )
241 fveq2 5687 . . . . . . . 8  |-  ( n  =  k  ->  ( S `  n )  =  ( S `  k ) )
242 oveq2 6048 . . . . . . . . 9  |-  ( n  =  k  ->  (
2 ^ n )  =  ( 2 ^ k ) )
243242oveq2d 6056 . . . . . . . 8  |-  ( n  =  k  ->  (
3  /  ( 2 ^ n ) )  =  ( 3  / 
( 2 ^ k
) ) )
244241, 243opeq12d 3952 . . . . . . 7  |-  ( n  =  k  ->  <. ( S `  n ) ,  ( 3  / 
( 2 ^ n
) ) >.  =  <. ( S `  k ) ,  ( 3  / 
( 2 ^ k
) ) >. )
245 opex 4387 . . . . . . 7  |-  <. ( S `  k ) ,  ( 3  / 
( 2 ^ k
) ) >.  e.  _V
246244, 233, 245fvmpt 5765 . . . . . 6  |-  ( k  e.  NN  ->  ( M `  k )  =  <. ( S `  k ) ,  ( 3  /  ( 2 ^ k ) )
>. )
247246fveq2d 5691 . . . . 5  |-  ( k  e.  NN  ->  (
( ball `  D ) `  ( M `  k
) )  =  ( ( ball `  D
) `  <. ( S `
 k ) ,  ( 3  /  (
2 ^ k ) ) >. ) )
248 df-ov 6043 . . . . 5  |-  ( ( S `  k ) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) )  =  ( ( ball `  D
) `  <. ( S `
 k ) ,  ( 3  /  (
2 ^ k ) ) >. )
249247, 248syl6eqr 2454 . . . 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 3351 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  C_  (
( ball `  D ) `  ( M `  k
) ) )
252251ralrimiva 2749 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 1721   {cab 2390    =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916    i^i cin 3279    C_ wss 3280   (/)c0 3588   ifcif 3699   ~Pcpw 3759   <.cop 3777   U.cuni 3975   U_ciun 4053   class class class wbr 4172   {copab 4225    e. cmpt 4226   -->wf 5409   ` cfv 5413  (class class class)co 6040    e. cmpt2 6042   2ndc2nd 6307   Fincfn 7068   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947    + caddc 8949    x. cmul 8951   RR*cxr 9075    <_ cle 9077    - cmin 9247    / cdiv 9633   NNcn 9956   2c2 10005   3c3 10006   NN0cn0 10177   ZZ>=cuz 10444   RR+crp 10568   + ecxad 10664    seq cseq 11278   ^cexp 11337   * Metcxmt 16641   Metcme 16642   ballcbl 16643   MetOpencmopn 16646   CMetcms 19160
This theorem is referenced by:  heiborlem8  26417  heiborlem9  26418
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-seq 11279  df-exp 11338  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-cmet 19163
  Copyright terms: Public domain W3C validator