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

Theorem heiborlem6 26540
Description: Lemma for heibor 26545. 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 9972 . . . 4  |-  ( k  e.  NN  ->  k  e.  NN0 )
2 heibor.6 . . . . . . . 8  |-  ( ph  ->  D  e.  ( CMet `  X ) )
3 cmetmet 18712 . . . . . . . 8  |-  ( D  e.  ( CMet `  X
)  ->  D  e.  ( Met `  X ) )
42, 3syl 15 . . . . . . 7  |-  ( ph  ->  D  e.  ( Met `  X ) )
5 metxmet 17899 . . . . . . 7  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( * Met `  X
) )
64, 5syl 15 . . . . . 6  |-  ( ph  ->  D  e.  ( * Met `  X ) )
76adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  D  e.  ( * Met `  X
) )
8 heibor.7 . . . . . . . . 9  |-  ( ph  ->  F : NN0 --> ( ~P X  i^i  Fin )
)
9 inss1 3389 . . . . . . . . 9  |-  ( ~P X  i^i  Fin )  C_ 
~P X
10 fss 5397 . . . . . . . . 9  |-  ( ( F : NN0 --> ( ~P X  i^i  Fin )  /\  ( ~P X  i^i  Fin )  C_  ~P X
)  ->  F : NN0
--> ~P X )
118, 9, 10sylancl 643 . . . . . . . 8  |-  ( ph  ->  F : NN0 --> ~P X
)
12 peano2nn0 10004 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( k  +  1 )  e. 
NN0 )
13 ffvelrn 5663 . . . . . . . 8  |-  ( ( F : NN0 --> ~P X  /\  ( k  +  1 )  e.  NN0 )  ->  ( F `  (
k  +  1 ) )  e.  ~P X
)
1411, 12, 13syl2an 463 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  ( k  +  1 ) )  e.  ~P X )
15 elpwi 3633 . . . . . . 7  |-  ( ( F `  ( k  +  1 ) )  e.  ~P X  -> 
( F `  (
k  +  1 ) )  C_  X )
1614, 15syl 15 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  ( k  +  1 ) )  C_  X
)
17 heibor.1 . . . . . . . . 9  |-  J  =  ( MetOpen `  D )
18 heibor.3 . . . . . . . . 9  |-  K  =  { u  |  -.  E. v  e.  ( ~P U  i^i  Fin )
u  C_  U. v }
19 heibor.4 . . . . . . . . 9  |-  G  =  { <. y ,  n >.  |  ( n  e. 
NN0  /\  y  e.  ( F `  n )  /\  ( y B n )  e.  K
) }
20 heibor.5 . . . . . . . . 9  |-  B  =  ( z  e.  X ,  m  e.  NN0  |->  ( z ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
21 heibor.8 . . . . . . . . 9  |-  ( ph  ->  A. n  e.  NN0  X  =  U_ y  e.  ( F `  n
) ( y B n ) )
22 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
) )
23 heibor.10 . . . . . . . . 9  |-  ( ph  ->  C G 0 )
24 heibor.11 . . . . . . . . 9  |-  S  =  seq  0 ( T ,  ( m  e. 
NN0  |->  if ( m  =  0 ,  C ,  ( m  - 
1 ) ) ) )
2517, 18, 19, 20, 2, 8, 21, 22, 23, 24heiborlem4 26538 . . . . . . . 8  |-  ( (
ph  /\  ( k  +  1 )  e. 
NN0 )  ->  ( S `  ( k  +  1 ) ) G ( k  +  1 ) )
2612, 25sylan2 460 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) ) G ( k  +  1 ) )
27 fvex 5539 . . . . . . . . 9  |-  ( S `
 ( k  +  1 ) )  e. 
_V
28 ovex 5883 . . . . . . . . 9  |-  ( k  +  1 )  e. 
_V
2917, 18, 19, 27, 28heiborlem2 26536 . . . . . . . 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 ) )
3029simp2bi 971 . . . . . . 7  |-  ( ( S `  ( k  +  1 ) ) G ( k  +  1 )  ->  ( S `  ( k  +  1 ) )  e.  ( F `  ( k  +  1 ) ) )
3126, 30syl 15 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  e.  ( F `  ( k  +  1 ) ) )
3216, 31sseldd 3181 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  e.  X
)
33 ffvelrn 5663 . . . . . . . 8  |-  ( ( F : NN0 --> ~P X  /\  k  e.  NN0 )  ->  ( F `  k )  e.  ~P X )
3411, 33sylan 457 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  e.  ~P X )
35 elpwi 3633 . . . . . . 7  |-  ( ( F `  k )  e.  ~P X  -> 
( F `  k
)  C_  X )
3634, 35syl 15 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  C_  X
)
3717, 18, 19, 20, 2, 8, 21, 22, 23, 24heiborlem4 26538 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k ) G k )
38 fvex 5539 . . . . . . . . 9  |-  ( S `
 k )  e. 
_V
39 vex 2791 . . . . . . . . 9  |-  k  e. 
_V
4017, 18, 19, 38, 39heiborlem2 26536 . . . . . . . 8  |-  ( ( S `  k ) G k  <->  ( k  e.  NN0  /\  ( S `
 k )  e.  ( F `  k
)  /\  ( ( S `  k ) B k )  e.  K ) )
4140simp2bi 971 . . . . . . 7  |-  ( ( S `  k ) G k  ->  ( S `  k )  e.  ( F `  k
) )
4237, 41syl 15 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k )  e.  ( F `  k ) )
4336, 42sseldd 3181 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  k )  e.  X
)
44 3re 9817 . . . . . 6  |-  3  e.  RR
45 2nn 9877 . . . . . . . . 9  |-  2  e.  NN
46 nnexpcl 11116 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  ( k  +  1 )  e.  NN0 )  ->  ( 2 ^ (
k  +  1 ) )  e.  NN )
4745, 12, 46sylancr 644 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  e.  NN )
4847nnrpd 10389 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  e.  RR+ )
4948adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2 ^ ( k  +  1 ) )  e.  RR+ )
50 rerpdivcl 10381 . . . . . 6  |-  ( ( 3  e.  RR  /\  ( 2 ^ (
k  +  1 ) )  e.  RR+ )  ->  ( 3  /  (
2 ^ ( k  +  1 ) ) )  e.  RR )
5144, 49, 50sylancr 644 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 3  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR )
52 nnexpcl 11116 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  k  e.  NN0 )  -> 
( 2 ^ k
)  e.  NN )
5345, 52mpan 651 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  NN )
5453nnrpd 10389 . . . . . . 7  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  RR+ )
5554adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 2 ^ k )  e.  RR+ )
56 rerpdivcl 10381 . . . . . 6  |-  ( ( 3  e.  RR  /\  ( 2 ^ k
)  e.  RR+ )  ->  ( 3  /  (
2 ^ k ) )  e.  RR )
5744, 55, 56sylancr 644 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 3  /  ( 2 ^ k ) )  e.  RR )
58 oveq1 5865 . . . . . . . . . . . 12  |-  ( z  =  ( S `  k )  ->  (
z ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
59 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
2 ^ m )  =  ( 2 ^ k ) )
6059oveq2d 5874 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  (
1  /  ( 2 ^ m ) )  =  ( 1  / 
( 2 ^ k
) ) )
6160oveq2d 5874 . . . . . . . . . . . 12  |-  ( m  =  k  ->  (
( S `  k
) ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) ) )
62 ovex 5883 . . . . . . . . . . . 12  |-  ( ( S `  k ) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  e. 
_V
6358, 61, 20, 62ovmpt2 5983 . . . . . . . . . . 11  |-  ( ( ( S `  k
)  e.  X  /\  k  e.  NN0 )  -> 
( ( S `  k ) B k )  =  ( ( S `  k ) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) ) )
6443, 63sylancom 648 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) B k )  =  ( ( S `  k ) ( ball `  D ) ( 1  /  ( 2 ^ k ) ) ) )
65 df-br 4024 . . . . . . . . . . . . . . . . 17  |-  ( ( S `  k ) G k  <->  <. ( S `
 k ) ,  k >.  e.  G
)
66 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( T `  x )  =  ( T `  <. ( S `  k ) ,  k >. )
)
67 df-ov 5861 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S `  k ) T k )  =  ( T `  <. ( S `  k ) ,  k >. )
6866, 67syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( T `  x )  =  ( ( S `  k
) T k ) )
6938, 39op2ndd 6131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( 2nd `  x
)  =  k )
7069oveq1d 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( 2nd `  x )  +  1 )  =  ( k  +  1 ) )
7168, 70breq12d 4036 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( T `
 x ) G ( ( 2nd `  x
)  +  1 )  <-> 
( ( S `  k ) T k ) G ( k  +  1 ) ) )
72 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( B `  x )  =  ( B `  <. ( S `  k ) ,  k >. )
)
73 df-ov 5861 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S `  k ) B k )  =  ( B `  <. ( S `  k ) ,  k >. )
7472, 73syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( B `  x )  =  ( ( S `  k
) B k ) )
7568, 70oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  <. ( S `  k ) ,  k
>.  ->  ( ( T `
 x ) B ( ( 2nd `  x
)  +  1 ) )  =  ( ( ( S `  k
) T k ) B ( k  +  1 ) ) )
7674, 75ineq12d 3371 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
7776eleq1d 2349 . . . . . . . . . . . . . . . . . . . 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 ) )
7871, 77anbi12d 691 . . . . . . . . . . . . . . . . . . 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 ) ) )
7978rspccv 2881 . . . . . . . . . . . . . . . . . 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
) ) )
8022, 79syl 15 . . . . . . . . . . . . . . . . 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 ) ) )
8165, 80syl5bi 208 . . . . . . . . . . . . . . . 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 ) ) )
8281adantr 451 . . . . . . . . . . . . . . 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 ) ) )
8337, 82mpd 14 . . . . . . . . . . . . . 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 ) )
8483simpld 445 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k ) G ( k  +  1 ) )
85 ovex 5883 . . . . . . . . . . . . . . 15  |-  ( ( S `  k ) T k )  e. 
_V
8617, 18, 19, 85, 28heiborlem2 26536 . . . . . . . . . . . . . 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 ) )
8786simp2bi 971 . . . . . . . . . . . . 13  |-  ( ( ( S `  k
) T k ) G ( k  +  1 )  ->  (
( S `  k
) T k )  e.  ( F `  ( k  +  1 ) ) )
8884, 87syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k )  e.  ( F `  (
k  +  1 ) ) )
8916, 88sseldd 3181 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) T k )  e.  X )
9012adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( k  +  1 )  e. 
NN0 )
91 oveq1 5865 . . . . . . . . . . . 12  |-  ( z  =  ( ( S `
 k ) T k )  ->  (
z ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ m ) ) ) )
92 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( m  =  ( k  +  1 )  ->  (
2 ^ m )  =  ( 2 ^ ( k  +  1 ) ) )
9392oveq2d 5874 . . . . . . . . . . . . 13  |-  ( m  =  ( k  +  1 )  ->  (
1  /  ( 2 ^ m ) )  =  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )
9493oveq2d 5874 . . . . . . . . . . . 12  |-  ( m  =  ( k  +  1 )  ->  (
( ( S `  k ) T k ) ( ball `  D
) ( 1  / 
( 2 ^ m
) ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
95 ovex 5883 . . . . . . . . . . . 12  |-  ( ( ( S `  k
) T k ) ( ball `  D
) ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e. 
_V
9691, 94, 20, 95ovmpt2 5983 . . . . . . . . . . 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 ) ) ) ) )
9789, 90, 96syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) T k ) B ( k  +  1 ) )  =  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
9864, 97ineq12d 3371 . . . . . . . . 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 ) ) ) ) ) )
9983simprd 449 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  e.  K )
100 0elpw 4180 . . . . . . . . . . . . 13  |-  (/)  e.  ~P U
101 0fin 7087 . . . . . . . . . . . . 13  |-  (/)  e.  Fin
102 elin 3358 . . . . . . . . . . . . 13  |-  ( (/)  e.  ( ~P U  i^i  Fin )  <->  ( (/)  e.  ~P U  /\  (/)  e.  Fin )
)
103100, 101, 102mpbir2an 886 . . . . . . . . . . . 12  |-  (/)  e.  ( ~P U  i^i  Fin )
104 0ss 3483 . . . . . . . . . . . 12  |-  (/)  C_  U. (/)
105 unieq 3836 . . . . . . . . . . . . . 14  |-  ( v  =  (/)  ->  U. v  =  U. (/) )
106105sseq2d 3206 . . . . . . . . . . . . 13  |-  ( v  =  (/)  ->  ( (/)  C_ 
U. v  <->  (/)  C_  U. (/) ) )
107106rspcev 2884 . . . . . . . . . . . 12  |-  ( (
(/)  e.  ( ~P U  i^i  Fin )  /\  (/)  C_  U. (/) )  ->  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
)
108103, 104, 107mp2an 653 . . . . . . . . . . 11  |-  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
109 0ex 4150 . . . . . . . . . . . . 13  |-  (/)  e.  _V
110 sseq1 3199 . . . . . . . . . . . . . . 15  |-  ( u  =  (/)  ->  ( u 
C_  U. v  <->  (/)  C_  U. v
) )
111110rexbidv 2564 . . . . . . . . . . . . . 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 ) )
112111notbid 285 . . . . . . . . . . . . 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
) )
113109, 112, 18elab2 2917 . . . . . . . . . . . 12  |-  ( (/)  e.  K  <->  -.  E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v
)
114113con2bii 322 . . . . . . . . . . 11  |-  ( E. v  e.  ( ~P U  i^i  Fin ) (/)  C_  U. v  <->  -.  (/)  e.  K
)
115108, 114mpbi 199 . . . . . . . . . 10  |-  -.  (/)  e.  K
116 nelne2 2536 . . . . . . . . . 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 ) ) )  =/=  (/) )
11799, 115, 116sylancl 643 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) B k )  i^i  ( ( ( S `  k ) T k ) B ( k  +  1 ) ) )  =/=  (/) )
11898, 117eqnetrrd 2466 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) ( ball `  D
) ( 1  / 
( 2 ^ k
) ) )  i^i  ( ( ( S `
 k ) T k ) ( ball `  D ) ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )  =/=  (/) )
11954rpreccld 10400 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ k ) )  e.  RR+ )
120119adantl 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e.  RR+ )
121120rpred 10390 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e.  RR )
12248rpreccld 10400 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR+ )
123122adantl 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR+ )
124123rpred 10390 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e.  RR )
125 rexadd 10559 . . . . . . . . . . . 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 ) ) ) ) )
126121, 124, 125syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) ) + e ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  =  ( ( 1  /  ( 2 ^ k ) )  +  ( 1  /  (
2 ^ ( k  +  1 ) ) ) ) )
127126breq1d 4033 . . . . . . . . . 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 ) ) ) )
128120rpxrd 10391 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ k ) )  e. 
RR* )
129123rpxrd 10391 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( 2 ^ ( k  +  1 ) ) )  e. 
RR* )
130 bldisj 17955 . . . . . . . . . . . . 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 ) ) ) ) )  =  (/) )
1311303exp2 1169 . . . . . . . . . . . 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 ) ) ) ) )  =  (/) ) ) ) )
132131imp32 422 . . . . . . . . . . 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 ) ) ) ) )  =  (/) ) )
1337, 43, 89, 128, 129, 132syl32anc 1190 . . . . . . . . . 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 ) ) ) ) )  =  (/) ) )
134127, 133sylbird 226 . . . . . . . . 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 ) ) ) ) )  =  (/) ) )
135134necon3ad 2482 . . . . . . . 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 ) ) ) )
136118, 135mpd 14 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  -.  (
( 1  /  (
2 ^ k ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) )  <_  ( ( S `
 k ) D ( ( S `  k ) T k ) ) )
137120, 123rpaddcld 10405 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e.  RR+ )
138137rpred 10390 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  e.  RR )
1394adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  D  e.  ( Met `  X ) )
140 metcl 17897 . . . . . . . . . 10  |-  ( ( D  e.  ( Met `  X )  /\  ( S `  k )  e.  X  /\  (
( S `  k
) T k )  e.  X )  -> 
( ( S `  k ) D ( ( S `  k
) T k ) )  e.  RR )
141139, 43, 89, 140syl3anc 1182 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) D ( ( S `
 k ) T k ) )  e.  RR )
142138, 141letrid 8969 . . . . . . . 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 ) ) ) ) ) )
143142ord 366 . . . . . . 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 ) ) ) ) ) )
144136, 143mpd 14 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  k ) D ( ( S `
 k ) T k ) )  <_ 
( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
145 seqp1 11061 . . . . . . . . . . . 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 ) ) ) )
146 nn0uz 10262 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
147145, 146eleq2s 2375 . . . . . . . . . . 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 ) ) ) )
14824fveq1i 5526 . . . . . . . . . . 11  |-  ( S `
 ( k  +  1 ) )  =  (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  (
k  +  1 ) )
14924fveq1i 5526 . . . . . . . . . . . 12  |-  ( S `
 k )  =  (  seq  0 ( T ,  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) ) `  k
)
150149oveq1i 5868 . . . . . . . . . . 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 ) ) )
151147, 148, 1503eqtr4g 2340 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  (
k  +  1 ) ) ) )
152 nn0p1nn 10003 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  NN )
153 nnne0 9778 . . . . . . . . . . . . . . . . 17  |-  ( ( k  +  1 )  e.  NN  ->  (
k  +  1 )  =/=  0 )
154153neneqd 2462 . . . . . . . . . . . . . . . 16  |-  ( ( k  +  1 )  e.  NN  ->  -.  ( k  +  1 )  =  0 )
155152, 154syl 15 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN0  ->  -.  (
k  +  1 )  =  0 )
156 iffalse 3572 . . . . . . . . . . . . . . 15  |-  ( -.  ( k  +  1 )  =  0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  =  ( ( k  +  1 )  -  1 ) )
157155, 156syl 15 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  =  ( ( k  +  1 )  - 
1 ) )
158 ovex 5883 . . . . . . . . . . . . . 14  |-  ( ( k  +  1 )  -  1 )  e. 
_V
159157, 158syl6eqel 2371 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  -  1 ) )  e.  _V )
160 eqeq1 2289 . . . . . . . . . . . . . . 15  |-  ( m  =  ( k  +  1 )  ->  (
m  =  0  <->  (
k  +  1 )  =  0 ) )
161 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( m  =  ( k  +  1 )  ->  (
m  -  1 )  =  ( ( k  +  1 )  - 
1 ) )
162160, 161ifbieq2d 3585 . . . . . . . . . . . . . 14  |-  ( m  =  ( k  +  1 )  ->  if ( m  =  0 ,  C ,  ( m  -  1 ) )  =  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  - 
1 ) ) )
163 eqid 2283 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) )  =  ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) )
164162, 163fvmptg 5600 . . . . . . . . . . . . 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 ) ) )
16512, 159, 164syl2anc 642 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) )  =  if ( ( k  +  1 )  =  0 ,  C ,  ( ( k  +  1 )  - 
1 ) ) )
166 nn0cn 9975 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  k  e.  CC )
167 ax-1cn 8795 . . . . . . . . . . . . 13  |-  1  e.  CC
168 pncan 9057 . . . . . . . . . . . . 13  |-  ( ( k  e.  CC  /\  1  e.  CC )  ->  ( ( k  +  1 )  -  1 )  =  k )
169166, 167, 168sylancl 643 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( ( k  +  1 )  -  1 )  =  k )
170165, 157, 1693eqtrd 2319 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) )  =  k )
171170oveq2d 5874 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( S `  k ) T ( ( m  e.  NN0  |->  if ( m  =  0 ,  C ,  ( m  -  1 ) ) ) `  ( k  +  1 ) ) )  =  ( ( S `  k ) T k ) )
172151, 171eqtrd 2315 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k ) T k ) )
173172adantl 452 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( S `  ( k  +  1 ) )  =  ( ( S `  k
) T k ) )
174173oveq1d 5873 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  =  ( ( ( S `
 k ) T k ) D ( S `  k ) ) )
175 metsym 17914 . . . . . . . 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 ) ) )
176139, 89, 43, 175syl3anc 1182 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( S `  k
) T k ) D ( S `  k ) )  =  ( ( S `  k ) D ( ( S `  k
) T k ) ) )
177174, 176eqtrd 2315 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  =  ( ( S `  k ) D ( ( S `  k
) T k ) ) )
178 3cn 9818 . . . . . . . . . . . . 13  |-  3  e.  CC
1791782timesi 9845 . . . . . . . . . . . 12  |-  ( 2  x.  3 )  =  ( 3  +  3 )
180179oveq1i 5868 . . . . . . . . . . 11  |-  ( ( 2  x.  3 )  -  3 )  =  ( ( 3  +  3 )  -  3 )
181 pncan 9057 . . . . . . . . . . . 12  |-  ( ( 3  e.  CC  /\  3  e.  CC )  ->  ( ( 3  +  3 )  -  3 )  =  3 )
182178, 178, 181mp2an 653 . . . . . . . . . . 11  |-  ( ( 3  +  3 )  -  3 )  =  3
183 df-3 9805 . . . . . . . . . . 11  |-  3  =  ( 2  +  1 )
184180, 182, 1833eqtri 2307 . . . . . . . . . 10  |-  ( ( 2  x.  3 )  -  3 )  =  ( 2  +  1 )
185184oveq1i 5868 . . . . . . . . 9  |-  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  +  1 )  /  (
2 ^ ( k  +  1 ) ) )
186 rpcn 10362 . . . . . . . . . . 11  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( 2 ^ ( k  +  1 ) )  e.  CC )
187 rpne0 10369 . . . . . . . . . . 11  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( 2 ^ ( k  +  1 ) )  =/=  0 )
188 2cn 9816 . . . . . . . . . . . . 13  |-  2  e.  CC
189188, 178mulcli 8842 . . . . . . . . . . . 12  |-  ( 2  x.  3 )  e.  CC
190 divsubdir 9456 . . . . . . . . . . . 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 ) ) ) ) )
191189, 178, 190mp3an12 1267 . . . . . . . . . . 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 ) ) ) ) )
192186, 187, 191syl2anc 642 . . . . . . . . . 10  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
19348, 192syl 15 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  3 )  -  3 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
194 divdir 9447 . . . . . . . . . . . 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 ) ) ) ) )
195188, 167, 194mp3an12 1267 . . . . . . . . . . 11  |-  ( ( ( 2 ^ (
k  +  1 ) )  e.  CC  /\  ( 2 ^ (
k  +  1 ) )  =/=  0 )  ->  ( ( 2  +  1 )  / 
( 2 ^ (
k  +  1 ) ) )  =  ( ( 2  /  (
2 ^ ( k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
196186, 187, 195syl2anc 642 . . . . . . . . . 10  |-  ( ( 2 ^ ( k  +  1 ) )  e.  RR+  ->  ( ( 2  +  1 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
19748, 196syl 15 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( ( 2  +  1 )  /  ( 2 ^ ( k  +  1 ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
198185, 193, 1973eqtr3a 2339 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( ( 2  x.  3 )  /  ( 2 ^ ( k  +  1 ) ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
199 rpcn 10362 . . . . . . . . . . . 12  |-  ( ( 2 ^ k )  e.  RR+  ->  ( 2 ^ k )  e.  CC )
200 rpne0 10369 . . . . . . . . . . . 12  |-  ( ( 2 ^ k )  e.  RR+  ->  ( 2 ^ k )  =/=  0 )
201 2ne0 9829 . . . . . . . . . . . . . 14  |-  2  =/=  0
202188, 201pm3.2i 441 . . . . . . . . . . . . 13  |-  ( 2  e.  CC  /\  2  =/=  0 )
203 divcan5 9462 . . . . . . . . . . . . 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 ) ) )
204178, 202, 203mp3an13 1268 . . . . . . . . . . . 12  |-  ( ( ( 2 ^ k
)  e.  CC  /\  ( 2 ^ k
)  =/=  0 )  ->  ( ( 2  x.  3 )  / 
( 2  x.  (
2 ^ k ) ) )  =  ( 3  /  ( 2 ^ k ) ) )
205199, 200, 204syl2anc 642 . . . . . . . . . . 11  |-  ( ( 2 ^ k )  e.  RR+  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 3  /  (
2 ^ k ) ) )
20654, 205syl 15 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 3  /  (
2 ^ k ) ) )
20754, 199syl 15 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  ( 2 ^ k )  e.  CC )
208 mulcom 8823 . . . . . . . . . . . . 13  |-  ( ( 2  e.  CC  /\  ( 2 ^ k
)  e.  CC )  ->  ( 2  x.  ( 2 ^ k
) )  =  ( ( 2 ^ k
)  x.  2 ) )
209188, 207, 208sylancr 644 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( 2  x.  ( 2 ^ k ) )  =  ( ( 2 ^ k )  x.  2 ) )
210 expp1 11110 . . . . . . . . . . . . 13  |-  ( ( 2  e.  CC  /\  k  e.  NN0 )  -> 
( 2 ^ (
k  +  1 ) )  =  ( ( 2 ^ k )  x.  2 ) )
211188, 210mpan 651 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( 2 ^ ( k  +  1 ) )  =  ( ( 2 ^ k )  x.  2 ) )
212209, 211eqtr4d 2318 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( 2  x.  ( 2 ^ k ) )  =  ( 2 ^ (
k  +  1 ) ) )
213212oveq2d 5874 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  3 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) ) )
214206, 213eqtr3d 2317 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( 3  /  ( 2 ^ k ) )  =  ( ( 2  x.  3 )  /  (
2 ^ ( k  +  1 ) ) ) )
215214oveq1d 5873 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( ( 2  x.  3 )  / 
( 2 ^ (
k  +  1 ) ) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
216 divcan5 9462 . . . . . . . . . . . . 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 ) ) )
217167, 202, 216mp3an13 1268 . . . . . . . . . . . 12  |-  ( ( ( 2 ^ k
)  e.  CC  /\  ( 2 ^ k
)  =/=  0 )  ->  ( ( 2  x.  1 )  / 
( 2  x.  (
2 ^ k ) ) )  =  ( 1  /  ( 2 ^ k ) ) )
218199, 200, 217syl2anc 642 . . . . . . . . . . 11  |-  ( ( 2 ^ k )  e.  RR+  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 1  /  (
2 ^ k ) ) )
21954, 218syl 15 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 1  /  (
2 ^ k ) ) )
220188mulid1i 8839 . . . . . . . . . . . 12  |-  ( 2  x.  1 )  =  2
221220a1i 10 . . . . . . . . . . 11  |-  ( k  e.  NN0  ->  ( 2  x.  1 )  =  2 )
222221, 212oveq12d 5876 . . . . . . . . . 10  |-  ( k  e.  NN0  ->  ( ( 2  x.  1 )  /  ( 2  x.  ( 2 ^ k
) ) )  =  ( 2  /  (
2 ^ ( k  +  1 ) ) ) )
223219, 222eqtr3d 2317 . . . . . . . . 9  |-  ( k  e.  NN0  ->  ( 1  /  ( 2 ^ k ) )  =  ( 2  /  (
2 ^ ( k  +  1 ) ) ) )
224223oveq1d 5873 . . . . . . . 8  |-  ( k  e.  NN0  ->  ( ( 1  /  ( 2 ^ k ) )  +  ( 1  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 2  / 
( 2 ^ (
k  +  1 ) ) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
225198, 215, 2243eqtr4d 2325 . . . . . . 7  |-  ( k  e.  NN0  ->  ( ( 3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
226225adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
3  /  ( 2 ^ k ) )  -  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( 1  / 
( 2 ^ k
) )  +  ( 1  /  ( 2 ^ ( k  +  1 ) ) ) ) )
227144, 177, 2263brtr4d 4053 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) D ( S `  k ) )  <_ 
( ( 3  / 
( 2 ^ k
) )  -  (
3  /  ( 2 ^ ( k  +  1 ) ) ) ) )
228 blss2 17959 . . . . 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 ) ) ) )
2297, 32, 43, 51, 57, 227, 228syl33anc 1197 . . . 4  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  C_  ( ( S `  k ) ( ball `  D ) ( 3  /  ( 2 ^ k ) ) ) )
2301, 229sylan2 460 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  C_  ( ( S `  k ) ( ball `  D ) ( 3  /  ( 2 ^ k ) ) ) )
231 peano2nn 9758 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
232 fveq2 5525 . . . . . . . . 9  |-  ( n  =  ( k  +  1 )  ->  ( S `  n )  =  ( S `  ( k  +  1 ) ) )
233 oveq2 5866 . . . . . . . . . 10  |-  ( n  =  ( k  +  1 )  ->  (
2 ^ n )  =  ( 2 ^ ( k  +  1 ) ) )
234233oveq2d 5874 . . . . . . . . 9  |-  ( n  =  ( k  +  1 )  ->  (
3  /  ( 2 ^ n ) )  =  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )
235232, 234opeq12d 3804 . . . . . . . 8  |-  ( n  =  ( k  +  1 )  ->  <. ( S `  n ) ,  ( 3  / 
( 2 ^ n
) ) >.  =  <. ( S `  ( k  +  1 ) ) ,  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) >. )
236 heibor.12 . . . . . . . 8  |-  M  =  ( n  e.  NN  |->  <. ( S `  n
) ,  ( 3  /  ( 2 ^ n ) ) >.
)
237 opex 4237 . . . . . . . 8  |-  <. ( S `  ( k  +  1 ) ) ,  ( 3  / 
( 2 ^ (
k  +  1 ) ) ) >.  e.  _V
238235, 236, 237fvmpt 5602 . . . . . . 7  |-  ( ( k  +  1 )  e.  NN  ->  ( M `  ( k  +  1 ) )  =  <. ( S `  ( k  +  1 ) ) ,  ( 3  /  ( 2 ^ ( k  +  1 ) ) )
>. )
239231, 238syl 15 . . . . . 6  |-  ( k  e.  NN  ->  ( M `  ( k  +  1 ) )  =  <. ( S `  ( k  +  1 ) ) ,  ( 3  /  ( 2 ^ ( k  +  1 ) ) )
>. )
240239adantl 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( M `
 ( k  +  1 ) )  = 
<. ( S `  (
k  +  1 ) ) ,  ( 3  /  ( 2 ^ ( k  +  1 ) ) ) >.
)
241240fveq2d 5529 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  =  ( ( ball `  D
) `  <. ( S `
 ( k  +  1 ) ) ,  ( 3  /  (
2 ^ ( k  +  1 ) ) ) >. ) )
242 df-ov 5861 . . . 4  |-  ( ( S `  ( k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) )  =  ( ( ball `  D
) `  <. ( S `
 ( k  +  1 ) ) ,  ( 3  /  (
2 ^ ( k  +  1 ) ) ) >. )
243241, 242syl6eqr 2333 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) ) ( ball `  D
) ( 3  / 
( 2 ^ (
k  +  1 ) ) ) ) )
244 fveq2 5525 . . . . . . . 8  |-  ( n  =  k  ->  ( S `  n )  =  ( S `  k ) )
245 oveq2 5866 . . . . . . . . 9  |-  ( n  =  k  ->  (
2 ^ n )  =  ( 2 ^ k ) )
246245oveq2d 5874 . . . . . . . 8  |-  ( n  =  k  ->  (
3  /  ( 2 ^ n ) )  =  ( 3  / 
( 2 ^ k
) ) )
247244, 246opeq12d 3804 . . . . . . 7  |-  ( n  =  k  ->  <. ( S `  n ) ,  ( 3  / 
( 2 ^ n
) ) >.  =  <. ( S `  k ) ,  ( 3  / 
( 2 ^ k
) ) >. )
248 opex 4237 . . . . . . 7  |-  <. ( S `  k ) ,  ( 3  / 
( 2 ^ k
) ) >.  e.  _V
249247, 236, 248fvmpt 5602 . . . . . 6  |-  ( k  e.  NN  ->  ( M `  k )  =  <. ( S `  k ) ,  ( 3  /  ( 2 ^ k ) )
>. )
250249fveq2d 5529 . . . . 5  |-  ( k  e.  NN  ->  (
( ball `  D ) `  ( M `  k
) )  =  ( ( ball `  D
) `  <. ( S `
 k ) ,  ( 3  /  (
2 ^ k ) ) >. ) )
251 df-ov 5861 . . . . 5  |-  ( ( S `  k ) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) )  =  ( ( ball `  D
) `  <. ( S `
 k ) ,  ( 3  /  (
2 ^ k ) ) >. )
252250, 251syl6eqr 2333 . . . 4  |-  ( k  e.  NN  ->  (
( ball `  D ) `  ( M `  k
) )  =  ( ( S `  k
) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) ) )
253252adantl 452 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  k
) )  =  ( ( S `  k
) ( ball `  D
) ( 3  / 
( 2 ^ k
) ) ) )
254230, 243, 2533sstr4d 3221 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ball `  D ) `  ( M `  (
k  +  1 ) ) )  C_  (
( ball `  D ) `  ( M `  k
) ) )
255254ralrimiva 2626 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 358    /\ w3a 934    = wceq 1623    e. wcel 1684   {cab 2269    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    i^i cin 3151    C_ wss 3152   (/)c0 3455   ifcif 3565   ~Pcpw 3625   <.cop 3643   U.cuni 3827   U_ciun 3905   class class class wbr 4023   {copab 4076    e. cmpt 4077   -->wf 5251   ` cfv 5255  (class class class)co 5858    e. cmpt2 5860   2ndc2nd 6121   Fincfn 6863   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742   RR*cxr 8866    <_ cle 8868    - cmin 9037    / cdiv 9423   NNcn 9746   2c2 9795   3c3 9796   NN0cn0 9965   ZZ>=cuz 10230   RR+crp 10354   + ecxad 10450    seq cseq 11046   ^cexp 11104   * Metcxmt 16369   Metcme 16370   ballcbl 16371   MetOpencmopn 16372   CMetcms 18680
This theorem is referenced by:  heiborlem8  26542  heiborlem9  26543
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-xneg 10452  df-xadd 10453  df-xmul 10454  df-seq 11047  df-exp 11105  df-xmet 16373  df-met 16374  df-bl 16375  df-cmet 18683
  Copyright terms: Public domain W3C validator