Theorem heiborlem6 33615

Description: Lemma for heibor 33620. 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

Step	Hyp	Ref	Expression
1		nnnn0 11299	. . . 4 |- ( k e. NN -> k e. NN0 )
2		heibor.6	. . . . . . . 8 |- ( ph -> D e. ( CMet ` X ) )
3		cmetmet 23084	. . . . . . . 8 |- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
4	2, 3	syl 17	. . . . . . 7 |- ( ph -> D e. ( Met ` X ) )
5		metxmet 22139	. . . . . . 7 |- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
6	4, 5	syl 17	. . . . . 6 |- ( ph -> D e. ( *Met ` X ) )
7	6	adantr 481	. . . . 5 |- ( ( ph /\ k e. NN0 ) -> D e. ( *Met ` X ) )
8		heibor.7	. . . . . . . . 9 |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
9		inss1 3833	. . . . . . . . 9 |- ( ~P X i^i Fin ) C_ ~P X
10		fss 6056	. . . . . . . . 9 |- ( ( F : NN0 --> ( ~P X i^i Fin ) /\ ( ~P X i^i Fin ) C_ ~P X ) -> F : NN0 --> ~P X )
11	8, 9, 10	sylancl 694	. . . . . . . 8 |- ( ph -> F : NN0 --> ~P X )
12		peano2nn0 11333	. . . . . . . 8 |- ( k e. NN0 -> ( k + 1 ) e. NN0 )
13		ffvelrn 6357	. . . . . . . 8 |- ( ( F : NN0 --> ~P X /\ ( k + 1 ) e. NN0 ) -> ( F ` ( k + 1 ) ) e. ~P X )
14	11, 12, 13	syl2an 494	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) e. ~P X )
15	14	elpwid 4170	. . . . . 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 ) ) ) )
24	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 33613	. . . . . . . 8 |- ( ( ph /\ ( k + 1 ) e. NN0 ) -> ( S ` ( k + 1 ) ) G ( k + 1 ) )
25	12, 24	sylan2 491	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> ( S ` ( k + 1 ) ) G ( k + 1 ) )
26		fvex 6201	. . . . . . . . 9 |- ( S ` ( k + 1 ) ) e. _V
27		ovex 6678	. . . . . . . . 9 |- ( k + 1 ) e. _V
28	16, 17, 18, 26, 27	heiborlem2 33611	. . . . . . . 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 ) )
29	28	simp2bi 1077	. . . . . . 7 |- ( ( S ` ( k + 1 ) ) G ( k + 1 ) -> ( S ` ( k + 1 ) ) e. ( F ` ( k + 1 ) ) )
30	25, 29	syl 17	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( S ` ( k + 1 ) ) e. ( F ` ( k + 1 ) ) )
31	15, 30	sseldd 3604	. . . . 5 |- ( ( ph /\ k e. NN0 ) -> ( S ` ( k + 1 ) ) e. X )
32	11	ffvelrnda 6359	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. ~P X )
33	32	elpwid 4170	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) C_ X )
34	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 33613	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> ( S ` k ) G k )
35		fvex 6201	. . . . . . . . 9 |- ( S ` k ) e. _V
36		vex 3203	. . . . . . . . 9 |- k e. _V
37	16, 17, 18, 35, 36	heiborlem2 33611	. . . . . . . 8 |- ( ( S ` k ) G k <-> ( k e. NN0 /\ ( S ` k ) e. ( F ` k ) /\ ( ( S ` k ) B k ) e. K ) )
38	37	simp2bi 1077	. . . . . . 7 |- ( ( S ` k ) G k -> ( S ` k ) e. ( F ` k ) )
39	34, 38	syl 17	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( S ` k ) e. ( F ` k ) )
40	33, 39	sseldd 3604	. . . . 5 |- ( ( ph /\ k e. NN0 ) -> ( S ` k ) e. X )
41		3re 11094	. . . . . 6 |- 3 e. RR
42		2nn 11185	. . . . . . . . 9 |- 2 e. NN
43		nnexpcl 12873	. . . . . . . . 9 |- ( ( 2 e. NN /\ ( k + 1 ) e. NN0 ) -> ( 2 ^ ( k + 1 ) ) e. NN )
44	42, 12, 43	sylancr 695	. . . . . . . 8 |- ( k e. NN0 -> ( 2 ^ ( k + 1 ) ) e. NN )
45	44	nnrpd 11870	. . . . . . 7 |- ( k e. NN0 -> ( 2 ^ ( k + 1 ) ) e. RR+ )
46	45	adantl 482	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( 2 ^ ( k + 1 ) ) e. RR+ )
47		rerpdivcl 11861	. . . . . 6 |- ( ( 3 e. RR /\ ( 2 ^ ( k + 1 ) ) e. RR+ ) -> ( 3 / ( 2 ^ ( k + 1 ) ) ) e. RR )
48	41, 46, 47	sylancr 695	. . . . 5 |- ( ( ph /\ k e. NN0 ) -> ( 3 / ( 2 ^ ( k + 1 ) ) ) e. RR )
49		nnexpcl 12873	. . . . . . . . 9 |- ( ( 2 e. NN /\ k e. NN0 ) -> ( 2 ^ k ) e. NN )
50	42, 49	mpan 706	. . . . . . . 8 |- ( k e. NN0 -> ( 2 ^ k ) e. NN )
51	50	nnrpd 11870	. . . . . . 7 |- ( k e. NN0 -> ( 2 ^ k ) e. RR+ )
52	51	adantl 482	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( 2 ^ k ) e. RR+ )
53		rerpdivcl 11861	. . . . . 6 |- ( ( 3 e. RR /\ ( 2 ^ k ) e. RR+ ) -> ( 3 / ( 2 ^ k ) ) e. RR )
54	41, 52, 53	sylancr 695	. . . . 5 |- ( ( ph /\ k e. NN0 ) -> ( 3 / ( 2 ^ k ) ) e. RR )
55		oveq1 6657	. . . . . . . . . . . 12 |- ( z = ( S ` k ) -> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
56		oveq2 6658	. . . . . . . . . . . . . 14 |- ( m = k -> ( 2 ^ m ) = ( 2 ^ k ) )
57	56	oveq2d 6666	. . . . . . . . . . . . 13 |- ( m = k -> ( 1 / ( 2 ^ m ) ) = ( 1 / ( 2 ^ k ) ) )
58	57	oveq2d 6666	. . . . . . . . . . . 12 |- ( m = k -> ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) )
59		ovex 6678	. . . . . . . . . . . 12 |- ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) e. _V
60	55, 58, 19, 59	ovmpt2 6796	. . . . . . . . . . 11 |- ( ( ( S ` k ) e. X /\ k e. NN0 ) -> ( ( S ` k ) B k ) = ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) )
61	40, 60	sylancom 701	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) B k ) = ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) )
62		df-br 4654	. . . . . . . . . . . . . . . . 17 |- ( ( S ` k ) G k <-> <. ( S ` k ) , k >. e. G )
63		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = <. ( S ` k ) , k >. -> ( T ` x ) = ( T ` <. ( S ` k ) , k >. ) )
64		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( S ` k ) T k ) = ( T ` <. ( S ` k ) , k >. )
65	63, 64	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. ( S ` k ) , k >. -> ( T ` x ) = ( ( S ` k ) T k ) )
66	35, 36	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = <. ( S ` k ) , k >. -> ( 2nd ` x ) = k )
67	66	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. ( S ` k ) , k >. -> ( ( 2nd ` x ) + 1 ) = ( k + 1 ) )
68	65, 67	breq12d 4666	. . . . . . . . . . . . . . . . . . . 20 |- ( x = <. ( S ` k ) , k >. -> ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) <-> ( ( S ` k ) T k ) G ( k + 1 ) ) )
69		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = <. ( S ` k ) , k >. -> ( B ` x ) = ( B ` <. ( S ` k ) , k >. ) )
70		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( S ` k ) B k ) = ( B ` <. ( S ` k ) , k >. )
71	69, 70	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = <. ( S ` k ) , k >. -> ( B ` x ) = ( ( S ` k ) B k ) )
72	65, 67	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = <. ( S ` k ) , k >. -> ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) = ( ( ( S ` k ) T k ) B ( k + 1 ) ) )
73	71, 72	ineq12d 3815	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
74	73	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 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 ) )
75	68, 74	anbi12d 747	. . . . . . . . . . . . . . . . . . 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 ) ) )
76	75	rspccv 3306	. . . . . . . . . . . . . . . . . 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 ) ) )
77	21, 76	syl 17	. . . . . . . . . . . . . . . . 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 ) ) )
78	62, 77	syl5bi 232	. . . . . . . . . . . . . . . 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 ) ) )
79	78	adantr 481	. . . . . . . . . . . . . . 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 ) ) )
80	34, 79	mpd 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 ) )
81	80	simpld 475	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) T k ) G ( k + 1 ) )
82		ovex 6678	. . . . . . . . . . . . . . 15 |- ( ( S ` k ) T k ) e. _V
83	16, 17, 18, 82, 27	heiborlem2 33611	. . . . . . . . . . . . . 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 ) )
84	83	simp2bi 1077	. . . . . . . . . . . . 13 |- ( ( ( S ` k ) T k ) G ( k + 1 ) -> ( ( S ` k ) T k ) e. ( F ` ( k + 1 ) ) )
85	81, 84	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) T k ) e. ( F ` ( k + 1 ) ) )
86	15, 85	sseldd 3604	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) T k ) e. X )
87	12	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. NN0 )
88		oveq1 6657	. . . . . . . . . . . 12 |- ( z = ( ( S ` k ) T k ) -> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( ( S ` k ) T k ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
89		oveq2 6658	. . . . . . . . . . . . . 14 |- ( m = ( k + 1 ) -> ( 2 ^ m ) = ( 2 ^ ( k + 1 ) ) )
90	89	oveq2d 6666	. . . . . . . . . . . . 13 |- ( m = ( k + 1 ) -> ( 1 / ( 2 ^ m ) ) = ( 1 / ( 2 ^ ( k + 1 ) ) ) )
91	90	oveq2d 6666	. . . . . . . . . . . 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 6678	. . . . . . . . . . . 12 |- ( ( ( S ` k ) T k ) ( ball ` D ) ( 1 / ( 2 ^ ( k + 1 ) ) ) ) e. _V
93	88, 91, 19, 92	ovmpt2 6796	. . . . . . . . . . 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 ) ) ) ) )
94	86, 87, 93	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( ( ( S ` k ) T k ) B ( k + 1 ) ) = ( ( ( S ` k ) T k ) ( ball ` D ) ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
95	61, 94	ineq12d 3815	. . . . . . . . 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 ) ) ) ) ) )
96	80	simprd 479	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K )
97		0elpw 4834	. . . . . . . . . . . . 13 |- (/) e. ~P U
98		0fin 8188	. . . . . . . . . . . . 13 |- (/) e. Fin
99		elin 3796	. . . . . . . . . . . . 13 |- ( (/) e. ( ~P U i^i Fin ) <-> ( (/) e. ~P U /\ (/) e. Fin ) )
100	97, 98, 99	mpbir2an 955	. . . . . . . . . . . 12 |- (/) e. ( ~P U i^i Fin )
101		0ss 3972	. . . . . . . . . . . 12 |- (/) C_ U. (/)
102		unieq 4444	. . . . . . . . . . . . . 14 |- ( v = (/) -> U. v = U. (/) )
103	102	sseq2d 3633	. . . . . . . . . . . . 13 |- ( v = (/) -> ( (/) C_ U. v <-> (/) C_ U. (/) ) )
104	103	rspcev 3309	. . . . . . . . . . . 12 |- ( ( (/) e. ( ~P U i^i Fin ) /\ (/) C_ U. (/) ) -> E. v e. ( ~P U i^i Fin ) (/) C_ U. v )
105	100, 101, 104	mp2an 708	. . . . . . . . . . 11 |- E. v e. ( ~P U i^i Fin ) (/) C_ U. v
106		0ex 4790	. . . . . . . . . . . . 13 |- (/) e. _V
107		sseq1 3626	. . . . . . . . . . . . . . 15 |- ( u = (/) -> ( u C_ U. v <-> (/) C_ U. v ) )
108	107	rexbidv 3052	. . . . . . . . . . . . . 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 ) )
109	108	notbid 308	. . . . . . . . . . . . 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 ) )
110	106, 109, 17	elab2 3354	. . . . . . . . . . . 12 |- ( (/) e. K <-> -. E. v e. ( ~P U i^i Fin ) (/) C_ U. v )
111	110	con2bii 347	. . . . . . . . . . 11 |- ( E. v e. ( ~P U i^i Fin ) (/) C_ U. v <-> -. (/) e. K )
112	105, 111	mpbi 220	. . . . . . . . . 10 |- -. (/) e. K
113		nelne2 2891	. . . . . . . . . 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 ) ) ) =/= (/) )
114	96, 112, 113	sylancl 694	. . . . . . . . 9 |- ( ( ph /\ k e. NN0 ) -> ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) =/= (/) )
115	95, 114	eqnetrrd 2862	. . . . . . . 8 |- ( ( ph /\ k e. NN0 ) -> ( ( ( S ` k ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) i^i ( ( ( S ` k ) T k ) ( ball ` D ) ( 1 / ( 2 ^ ( k + 1 ) ) ) ) ) =/= (/) )
116	51	rpreccld 11882	. . . . . . . . . . . . . 14 |- ( k e. NN0 -> ( 1 / ( 2 ^ k ) ) e. RR+ )
117	116	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( 2 ^ k ) ) e. RR+ )
118	117	rpred 11872	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( 2 ^ k ) ) e. RR )
119	45	rpreccld 11882	. . . . . . . . . . . . . 14 |- ( k e. NN0 -> ( 1 / ( 2 ^ ( k + 1 ) ) ) e. RR+ )
120	119	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( 2 ^ ( k + 1 ) ) ) e. RR+ )
121	120	rpred 11872	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( 2 ^ ( k + 1 ) ) ) e. RR )
122		rexadd 12063	. . . . . . . . . . . 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 ) ) ) ) )
123	118, 121, 122	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( ( 1 / ( 2 ^ k ) ) +e ( 1 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
124	123	breq1d 4663	. . . . . . . . . 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 ) ) ) )
125	117	rpxrd 11873	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( 2 ^ k ) ) e. RR* )
126	120	rpxrd 11873	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( 1 / ( 2 ^ ( k + 1 ) ) ) e. RR* )
127		bldisj 22203	. . . . . . . . . . . . 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 ) ) ) ) ) = (/) )
128	127	3exp2 1285	. . . . . . . . . . . 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 ) ) ) ) ) = (/) ) ) ) )
129	128	imp32 449	. . . . . . . . . . 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 ) ) ) ) ) = (/) ) )
130	7, 40, 86, 125, 126, 129	syl32anc 1334	. . . . . . . . . 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 ) ) ) ) ) = (/) ) )
131	124, 130	sylbird 250	. . . . . . . . 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 ) ) ) ) ) = (/) ) )
132	131	necon3ad 2807	. . . . . . . 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 ) ) ) )
133	115, 132	mpd 15	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> -. ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) <_ ( ( S ` k ) D ( ( S ` k ) T k ) ) )
134	117, 120	rpaddcld 11887	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) e. RR+ )
135	134	rpred 11872	. . . . . . . . 9 |- ( ( ph /\ k e. NN0 ) -> ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) e. RR )
136	4	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ k e. NN0 ) -> D e. ( Met ` X ) )
137		metcl 22137	. . . . . . . . . 10 |- ( ( D e. ( Met ` X ) /\ ( S ` k ) e. X /\ ( ( S ` k ) T k ) e. X ) -> ( ( S ` k ) D ( ( S ` k ) T k ) ) e. RR )
138	136, 40, 86, 137	syl3anc 1326	. . . . . . . . 9 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) D ( ( S ` k ) T k ) ) e. RR )
139	135, 138	letrid 10189	. . . . . . . 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 ) ) ) ) ) )
140	139	ord 392	. . . . . . 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 ) ) ) ) ) )
141	133, 140	mpd 15	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) D ( ( S ` k ) T k ) ) <_ ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
142		seqp1 12816	. . . . . . . . . . . 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 11722	. . . . . . . . . . . 12 |- NN0 = ( ZZ>= ` 0 )
144	142, 143	eleq2s 2719	. . . . . . . . . . 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 ) ) ) )
145	23	fveq1i 6192	. . . . . . . . . . 11 |- ( S ` ( k + 1 ) ) = ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` ( k + 1 ) )
146	23	fveq1i 6192	. . . . . . . . . . . 12 |- ( S ` k ) = ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` k )
147	146	oveq1i 6660	. . . . . . . . . . 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 ) ) )
148	144, 145, 147	3eqtr4g 2681	. . . . . . . . . 10 |- ( k e. NN0 -> ( S ` ( k + 1 ) ) = ( ( S ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) )
149		nn0p1nn 11332	. . . . . . . . . . . . . . . 16 |- ( k e. NN0 -> ( k + 1 ) e. NN )
150		nnne0 11053	. . . . . . . . . . . . . . . . 17 |- ( ( k + 1 ) e. NN -> ( k + 1 ) =/= 0 )
151	150	neneqd 2799	. . . . . . . . . . . . . . . 16 |- ( ( k + 1 ) e. NN -> -. ( k + 1 ) = 0 )
152	149, 151	syl 17	. . . . . . . . . . . . . . 15 |- ( k e. NN0 -> -. ( k + 1 ) = 0 )
153	152	iffalsed 4097	. . . . . . . . . . . . . 14 |- ( k e. NN0 -> if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) = ( ( k + 1 ) - 1 ) )
154		ovex 6678	. . . . . . . . . . . . . 14 |- ( ( k + 1 ) - 1 ) e. _V
155	153, 154	syl6eqel 2709	. . . . . . . . . . . . 13 |- ( k e. NN0 -> if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) e. _V )
156		eqeq1 2626	. . . . . . . . . . . . . . 15 |- ( m = ( k + 1 ) -> ( m = 0 <-> ( k + 1 ) = 0 ) )
157		oveq1 6657	. . . . . . . . . . . . . . 15 |- ( m = ( k + 1 ) -> ( m - 1 ) = ( ( k + 1 ) - 1 ) )
158	156, 157	ifbieq2d 4111	. . . . . . . . . . . . . 14 |- ( m = ( k + 1 ) -> if ( m = 0 , C , ( m - 1 ) ) = if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) )
159		eqid 2622	. . . . . . . . . . . . . 14 |- ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) = ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) )
160	158, 159	fvmptg 6280	. . . . . . . . . . . . 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 ) ) )
161	12, 155, 160	syl2anc 693	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) = if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) )
162		nn0cn 11302	. . . . . . . . . . . . 13 |- ( k e. NN0 -> k e. CC )
163		ax-1cn 9994	. . . . . . . . . . . . 13 |- 1 e. CC
164		pncan 10287	. . . . . . . . . . . . 13 |- ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
165	162, 163, 164	sylancl 694	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( ( k + 1 ) - 1 ) = k )
166	161, 153, 165	3eqtrd 2660	. . . . . . . . . . 11 |- ( k e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) = k )
167	166	oveq2d 6666	. . . . . . . . . 10 |- ( k e. NN0 -> ( ( S ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) = ( ( S ` k ) T k ) )
168	148, 167	eqtrd 2656	. . . . . . . . 9 |- ( k e. NN0 -> ( S ` ( k + 1 ) ) = ( ( S ` k ) T k ) )
169	168	adantl 482	. . . . . . . 8 |- ( ( ph /\ k e. NN0 ) -> ( S ` ( k + 1 ) ) = ( ( S ` k ) T k ) )
170	169	oveq1d 6665	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` ( k + 1 ) ) D ( S ` k ) ) = ( ( ( S ` k ) T k ) D ( S ` k ) ) )
171		metsym 22155	. . . . . . . 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 ) ) )
172	136, 86, 40, 171	syl3anc 1326	. . . . . . 7 |- ( ( ph /\ k e. NN0 ) -> ( ( ( S ` k ) T k ) D ( S ` k ) ) = ( ( S ` k ) D ( ( S ` k ) T k ) ) )
173	170, 172	eqtrd 2656	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` ( k + 1 ) ) D ( S ` k ) ) = ( ( S ` k ) D ( ( S ` k ) T k ) ) )
174		3cn 11095	. . . . . . . . . . . . 13 |- 3 e. CC
175	174	2timesi 11147	. . . . . . . . . . . 12 |- ( 2 x. 3 ) = ( 3 + 3 )
176	175	oveq1i 6660	. . . . . . . . . . 11 |- ( ( 2 x. 3 ) - 3 ) = ( ( 3 + 3 ) - 3 )
177	174, 174	pncan3oi 10297	. . . . . . . . . . 11 |- ( ( 3 + 3 ) - 3 ) = 3
178		df-3 11080	. . . . . . . . . . 11 |- 3 = ( 2 + 1 )
179	176, 177, 178	3eqtri 2648	. . . . . . . . . 10 |- ( ( 2 x. 3 ) - 3 ) = ( 2 + 1 )
180	179	oveq1i 6660	. . . . . . . . 9 |- ( ( ( 2 x. 3 ) - 3 ) / ( 2 ^ ( k + 1 ) ) ) = ( ( 2 + 1 ) / ( 2 ^ ( k + 1 ) ) )
181		rpcn 11841	. . . . . . . . . . 11 |- ( ( 2 ^ ( k + 1 ) ) e. RR+ -> ( 2 ^ ( k + 1 ) ) e. CC )
182		rpne0 11848	. . . . . . . . . . 11 |- ( ( 2 ^ ( k + 1 ) ) e. RR+ -> ( 2 ^ ( k + 1 ) ) =/= 0 )
183		2cn 11091	. . . . . . . . . . . . 13 |- 2 e. CC
184	183, 174	mulcli 10045	. . . . . . . . . . . 12 |- ( 2 x. 3 ) e. CC
185		divsubdir 10721	. . . . . . . . . . . 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 ) ) ) ) )
186	184, 174, 185	mp3an12 1414	. . . . . . . . . . 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 ) ) ) ) )
187	181, 182, 186	syl2anc 693	. . . . . . . . . 10 |- ( ( 2 ^ ( k + 1 ) ) e. RR+ -> ( ( ( 2 x. 3 ) - 3 ) / ( 2 ^ ( k + 1 ) ) ) = ( ( ( 2 x. 3 ) / ( 2 ^ ( k + 1 ) ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) )
188	45, 187	syl 17	. . . . . . . . 9 |- ( k e. NN0 -> ( ( ( 2 x. 3 ) - 3 ) / ( 2 ^ ( k + 1 ) ) ) = ( ( ( 2 x. 3 ) / ( 2 ^ ( k + 1 ) ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) )
189		divdir 10710	. . . . . . . . . . . 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 ) ) ) ) )
190	183, 163, 189	mp3an12 1414	. . . . . . . . . . 11 |- ( ( ( 2 ^ ( k + 1 ) ) e. CC /\ ( 2 ^ ( k + 1 ) ) =/= 0 ) -> ( ( 2 + 1 ) / ( 2 ^ ( k + 1 ) ) ) = ( ( 2 / ( 2 ^ ( k + 1 ) ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
191	181, 182, 190	syl2anc 693	. . . . . . . . . 10 |- ( ( 2 ^ ( k + 1 ) ) e. RR+ -> ( ( 2 + 1 ) / ( 2 ^ ( k + 1 ) ) ) = ( ( 2 / ( 2 ^ ( k + 1 ) ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
192	45, 191	syl 17	. . . . . . . . 9 |- ( k e. NN0 -> ( ( 2 + 1 ) / ( 2 ^ ( k + 1 ) ) ) = ( ( 2 / ( 2 ^ ( k + 1 ) ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
193	180, 188, 192	3eqtr3a 2680	. . . . . . . 8 |- ( k e. NN0 -> ( ( ( 2 x. 3 ) / ( 2 ^ ( k + 1 ) ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( 2 / ( 2 ^ ( k + 1 ) ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
194		rpcn 11841	. . . . . . . . . . . 12 |- ( ( 2 ^ k ) e. RR+ -> ( 2 ^ k ) e. CC )
195		rpne0 11848	. . . . . . . . . . . 12 |- ( ( 2 ^ k ) e. RR+ -> ( 2 ^ k ) =/= 0 )
196		2cnne0 11242	. . . . . . . . . . . . 13 |- ( 2 e. CC /\ 2 =/= 0 )
197		divcan5 10727	. . . . . . . . . . . . 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 ) ) )
198	174, 196, 197	mp3an13 1415	. . . . . . . . . . . 12 |- ( ( ( 2 ^ k ) e. CC /\ ( 2 ^ k ) =/= 0 ) -> ( ( 2 x. 3 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 3 / ( 2 ^ k ) ) )
199	194, 195, 198	syl2anc 693	. . . . . . . . . . 11 |- ( ( 2 ^ k ) e. RR+ -> ( ( 2 x. 3 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 3 / ( 2 ^ k ) ) )
200	51, 199	syl 17	. . . . . . . . . 10 |- ( k e. NN0 -> ( ( 2 x. 3 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 3 / ( 2 ^ k ) ) )
201	51, 194	syl 17	. . . . . . . . . . . . 13 |- ( k e. NN0 -> ( 2 ^ k ) e. CC )
202		mulcom 10022	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ ( 2 ^ k ) e. CC ) -> ( 2 x. ( 2 ^ k ) ) = ( ( 2 ^ k ) x. 2 ) )
203	183, 201, 202	sylancr 695	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( 2 x. ( 2 ^ k ) ) = ( ( 2 ^ k ) x. 2 ) )
204		expp1 12867	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ k e. NN0 ) -> ( 2 ^ ( k + 1 ) ) = ( ( 2 ^ k ) x. 2 ) )
205	183, 204	mpan 706	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( 2 ^ ( k + 1 ) ) = ( ( 2 ^ k ) x. 2 ) )
206	203, 205	eqtr4d 2659	. . . . . . . . . . 11 |- ( k e. NN0 -> ( 2 x. ( 2 ^ k ) ) = ( 2 ^ ( k + 1 ) ) )
207	206	oveq2d 6666	. . . . . . . . . 10 |- ( k e. NN0 -> ( ( 2 x. 3 ) / ( 2 x. ( 2 ^ k ) ) ) = ( ( 2 x. 3 ) / ( 2 ^ ( k + 1 ) ) ) )
208	200, 207	eqtr3d 2658	. . . . . . . . 9 |- ( k e. NN0 -> ( 3 / ( 2 ^ k ) ) = ( ( 2 x. 3 ) / ( 2 ^ ( k + 1 ) ) ) )
209	208	oveq1d 6665	. . . . . . . 8 |- ( k e. NN0 -> ( ( 3 / ( 2 ^ k ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( ( 2 x. 3 ) / ( 2 ^ ( k + 1 ) ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) )
210		divcan5 10727	. . . . . . . . . . . . 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 ) ) )
211	163, 196, 210	mp3an13 1415	. . . . . . . . . . . 12 |- ( ( ( 2 ^ k ) e. CC /\ ( 2 ^ k ) =/= 0 ) -> ( ( 2 x. 1 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 1 / ( 2 ^ k ) ) )
212	194, 195, 211	syl2anc 693	. . . . . . . . . . 11 |- ( ( 2 ^ k ) e. RR+ -> ( ( 2 x. 1 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 1 / ( 2 ^ k ) ) )
213	51, 212	syl 17	. . . . . . . . . 10 |- ( k e. NN0 -> ( ( 2 x. 1 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 1 / ( 2 ^ k ) ) )
214		2t1e2 11176	. . . . . . . . . . . 12 |- ( 2 x. 1 ) = 2
215	214	a1i 11	. . . . . . . . . . 11 |- ( k e. NN0 -> ( 2 x. 1 ) = 2 )
216	215, 206	oveq12d 6668	. . . . . . . . . 10 |- ( k e. NN0 -> ( ( 2 x. 1 ) / ( 2 x. ( 2 ^ k ) ) ) = ( 2 / ( 2 ^ ( k + 1 ) ) ) )
217	213, 216	eqtr3d 2658	. . . . . . . . 9 |- ( k e. NN0 -> ( 1 / ( 2 ^ k ) ) = ( 2 / ( 2 ^ ( k + 1 ) ) ) )
218	217	oveq1d 6665	. . . . . . . 8 |- ( k e. NN0 -> ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( 2 / ( 2 ^ ( k + 1 ) ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
219	193, 209, 218	3eqtr4d 2666	. . . . . . 7 |- ( k e. NN0 -> ( ( 3 / ( 2 ^ k ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
220	219	adantl 482	. . . . . 6 |- ( ( ph /\ k e. NN0 ) -> ( ( 3 / ( 2 ^ k ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( 1 / ( 2 ^ k ) ) + ( 1 / ( 2 ^ ( k + 1 ) ) ) ) )
221	141, 173, 220	3brtr4d 4685	. . . . 5 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` ( k + 1 ) ) D ( S ` k ) ) <_ ( ( 3 / ( 2 ^ k ) ) - ( 3 / ( 2 ^ ( k + 1 ) ) ) ) )
222		blss2 22209	. . . . 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 ) ) ) )
223	7, 31, 40, 48, 54, 221, 222	syl33anc 1341	. . . 4 |- ( ( ph /\ k e. NN0 ) -> ( ( S ` ( k + 1 ) ) ( ball ` D ) ( 3 / ( 2 ^ ( k + 1 ) ) ) ) C_ ( ( S ` k ) ( ball ` D ) ( 3 / ( 2 ^ k ) ) ) )
224	1, 223	sylan2 491	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( S ` ( k + 1 ) ) ( ball ` D ) ( 3 / ( 2 ^ ( k + 1 ) ) ) ) C_ ( ( S ` k ) ( ball ` D ) ( 3 / ( 2 ^ k ) ) ) )
225		peano2nn 11032	. . . . . . 7 |- ( k e. NN -> ( k + 1 ) e. NN )
226		fveq2 6191	. . . . . . . . 9 |- ( n = ( k + 1 ) -> ( S ` n ) = ( S ` ( k + 1 ) ) )
227		oveq2 6658	. . . . . . . . . 10 |- ( n = ( k + 1 ) -> ( 2 ^ n ) = ( 2 ^ ( k + 1 ) ) )
228	227	oveq2d 6666	. . . . . . . . 9 |- ( n = ( k + 1 ) -> ( 3 / ( 2 ^ n ) ) = ( 3 / ( 2 ^ ( k + 1 ) ) ) )
229	226, 228	opeq12d 4410	. . . . . . . 8 |- ( n = ( k + 1 ) -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. = <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. )
230		heibor.12	. . . . . . . 8 |- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )
231		opex 4932	. . . . . . . 8 |- <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. e. _V
232	229, 230, 231	fvmpt 6282	. . . . . . 7 |- ( ( k + 1 ) e. NN -> ( M ` ( k + 1 ) ) = <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. )
233	225, 232	syl 17	. . . . . 6 |- ( k e. NN -> ( M ` ( k + 1 ) ) = <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. )
234	233	adantl 482	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( M ` ( k + 1 ) ) = <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. )
235	234	fveq2d 6195	. . . 4 |- ( ( ph /\ k e. NN ) -> ( ( ball ` D ) ` ( M ` ( k + 1 ) ) ) = ( ( ball ` D ) ` <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. ) )
236		df-ov 6653	. . . 4 |- ( ( S ` ( k + 1 ) ) ( ball ` D ) ( 3 / ( 2 ^ ( k + 1 ) ) ) ) = ( ( ball ` D ) ` <. ( S ` ( k + 1 ) ) , ( 3 / ( 2 ^ ( k + 1 ) ) ) >. )
237	235, 236	syl6eqr 2674	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( ball ` D ) ` ( M ` ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) ( ball ` D ) ( 3 / ( 2 ^ ( k + 1 ) ) ) ) )
238		fveq2 6191	. . . . . . . 8 |- ( n = k -> ( S ` n ) = ( S ` k ) )
239		oveq2 6658	. . . . . . . . 9 |- ( n = k -> ( 2 ^ n ) = ( 2 ^ k ) )
240	239	oveq2d 6666	. . . . . . . 8 |- ( n = k -> ( 3 / ( 2 ^ n ) ) = ( 3 / ( 2 ^ k ) ) )
241	238, 240	opeq12d 4410	. . . . . . 7 |- ( n = k -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. = <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. )
242		opex 4932	. . . . . . 7 |- <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. e. _V
243	241, 230, 242	fvmpt 6282	. . . . . 6 |- ( k e. NN -> ( M ` k ) = <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. )
244	243	fveq2d 6195	. . . . 5 |- ( k e. NN -> ( ( ball ` D ) ` ( M ` k ) ) = ( ( ball ` D ) ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) )
245		df-ov 6653	. . . . 5 |- ( ( S ` k ) ( ball ` D ) ( 3 / ( 2 ^ k ) ) ) = ( ( ball ` D ) ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. )
246	244, 245	syl6eqr 2674	. . . 4 |- ( k e. NN -> ( ( ball ` D ) ` ( M ` k ) ) = ( ( S ` k ) ( ball ` D ) ( 3 / ( 2 ^ k ) ) ) )
247	246	adantl 482	. . 3 |- ( ( ph /\ k e. NN ) -> ( ( ball ` D ) ` ( M ` k ) ) = ( ( S ` k ) ( ball ` D ) ( 3 / ( 2 ^ k ) ) ) )
248	224, 237, 247	3sstr4d 3648	. 2 |- ( ( ph /\ k e. NN ) -> ( ( ball ` D ) ` ( M ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( M ` k ) ) )
249	248	ralrimiva 2966	1 |- ( ph -> A. k e. NN ( ( ball ` D ) ` ( M ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( M ` k ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   ~Pcpw 4158   <.cop 4183   U.cuni 4436   U_ciun 4520   class class class wbr 4653   {copab 4712   |-> cmpt 4729   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   2ndc2nd 7167   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   RR*cxr 10073   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   2c2 11070   3c3 11071   NN0cn0 11292   ZZ>=cuz 11687   RR+crp 11832   +ecxad 11944   seqcseq 12801   ^cexp 12860   *Metcxmt 19731   Metcme 19732   ballcbl 19733   MetOpencmopn 19736   CMetcms 23052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-seq 12802  df-exp 12861  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-cmet 23055

This theorem is referenced by:  heiborlem8  33617  heiborlem9  33618