Theorem bcthlem17 8012

Description: Lemma for bcth 8029. The radius of the balls in sequence g decreases exponentially.

Hypotheses

Ref	Expression
bcthlem18.1	|- D e. CMet
bcthlem18.3	|- X = dom dom D
bcthlem18.6	|- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
bcthlem18.7	|- A = (X X. {x e. RR | 0 < x})
bcthlem18.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem17	|- (n e. NN -> ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (2nd` (g` n)) < (1 / (2^n))))

Distinct variable groups:   j,n,y,z,A   j,p,r,D,n,y,z   k,n,F   j,J,p,r,y,z   j,M,p,r,y,z   z,O   j,X,n,p,r,y,z   j,k,x,g,p,r,y,z,n

Proof of Theorem bcthlem17

Step	Hyp	Ref	Expression
1		bcthlem18.1	. . . . . . . . 9 |- D e. CMet
2		bcthlem18.3	. . . . . . . . 9 |- X = dom dom D
3		bcthlem18.6	. . . . . . . . 9 |- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
4		bcthlem18.8	. . . . . . . . 9 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
5	1, 2, 3, 4	bcthlem15 8010	. . . . . . . 8 |- ((((m + 1) e. NN /\ (g` m) e. A) /\ (g` (m + 1)) e. ((m + 1)F(g` m))) -> (((1st` (g` (m + 1))) e. X /\ ((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1))))) /\ ((2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2) /\ ((1st` (g` (m + 1)))( ball ` D)(2nd` (g` (m + 1)))) (_ ((X \ ((cls` J)` (M` (m + 1)))) i^i ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2))))))
6		peano2nn 5937	. . . . . . . . . 10 |- (m e. NN -> (m + 1) e. NN)
7	6	adantr 391	. . . . . . . . 9 |- ((m e. NN /\ g:NN-->A) -> (m + 1) e. NN)
8		ffvelrn 3820	. . . . . . . . . 10 |- ((g:NN-->A /\ m e. NN) -> (g` m) e. A)
9	8	ancoms 438	. . . . . . . . 9 |- ((m e. NN /\ g:NN-->A) -> (g` m) e. A)
10	7, 9	jca 288	. . . . . . . 8 |- ((m e. NN /\ g:NN-->A) -> ((m + 1) e. NN /\ (g` m) e. A))
11	5, 10	sylan 450	. . . . . . 7 |- (((m e. NN /\ g:NN-->A) /\ (g` (m + 1)) e. ((m + 1)F(g` m))) -> (((1st` (g` (m + 1))) e. X /\ ((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1))))) /\ ((2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2) /\ ((1st` (g` (m + 1)))( ball ` D)(2nd` (g` (m + 1)))) (_ ((X \ ((cls` J)` (M` (m + 1)))) i^i ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2))))))
12	11	ex 373	. . . . . 6 |- ((m e. NN /\ g:NN-->A) -> ((g` (m + 1)) e. ((m + 1)F(g` m)) -> (((1st` (g` (m + 1))) e. X /\ ((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1))))) /\ ((2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2) /\ ((1st` (g` (m + 1)))( ball ` D)(2nd` (g` (m + 1)))) (_ ((X \ ((cls` J)` (M` (m + 1)))) i^i ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)))))))
13		bcthlem1 7996	. . . . . . . . . . 11 |- (((m e. NN /\ (2nd` (g` m)) e. RR) /\ ((2nd` (g` (m + 1))) e. RR /\ (2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2))) -> ((2nd` (g` m)) < (1 / (2^m)) -> (2nd` (g` (m + 1))) < (1 / (2^(m + 1)))))
14		pm3.26 319	. . . . . . . . . . . 12 |- ((m e. NN /\ g:NN-->A) -> m e. NN)
15		bcthlem18.7	. . . . . . . . . . . . . . . 16 |- A = (X X. {x e. RR | 0 < x})
16	15	bcthlem4 7999	. . . . . . . . . . . . . . 15 |- ((g:NN-->A /\ m e. NN) -> ((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))))
17	16	pm3.27d 325	. . . . . . . . . . . . . 14 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
18	17	pm3.26d 321	. . . . . . . . . . . . 13 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. RR)
19	18	ancoms 438	. . . . . . . . . . . 12 |- ((m e. NN /\ g:NN-->A) -> (2nd` (g` m)) e. RR)
20	14, 19	jca 288	. . . . . . . . . . 11 |- ((m e. NN /\ g:NN-->A) -> (m e. NN /\ (2nd` (g` m)) e. RR))
21	13, 20	sylan 450	. . . . . . . . . 10 |- (((m e. NN /\ g:NN-->A) /\ ((2nd` (g` (m + 1))) e. RR /\ (2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2))) -> ((2nd` (g` m)) < (1 / (2^m)) -> (2nd` (g` (m + 1))) < (1 / (2^(m + 1)))))
22	21	adantrlr 403	. . . . . . . . 9 |- (((m e. NN /\ g:NN-->A) /\ (((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1)))) /\ (2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2))) -> ((2nd` (g` m)) < (1 / (2^m)) -> (2nd` (g` (m + 1))) < (1 / (2^(m + 1)))))
23	22	adantrll 402	. . . . . . . 8 |- (((m e. NN /\ g:NN-->A) /\ (((1st` (g` (m + 1))) e. X /\ ((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1))))) /\ (2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2))) -> ((2nd` (g` m)) < (1 / (2^m)) -> (2nd` (g` (m + 1))) < (1 / (2^(m + 1)))))
24	23	adantrrr 405	. . . . . . 7 |- (((m e. NN /\ g:NN-->A) /\ (((1st` (g` (m + 1))) e. X /\ ((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1))))) /\ ((2nd` (g` (m + 1))) < ((2nd` (g` m)) / 2) /\ ((1st` (g` (m + 1)))( ball ` D)(2nd` (g` (m + 1)))) (_ ((X \ ((cls` J)` (M` (m + 1)))) i^i ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)))))) -> ((2nd` (g` m)) < (1 / (2^m)) -> (2nd` (g` (m + 1))) < (1 / (2^(m + 1)))))
25	24	ex 373	. . . . . 6 |- ((m e. NN /\ g:NN-->A) -> ((((1st` (g` (m + 1))) e. X /\ ((2nd` (g` (m + 1))) e. RR /\ 0 < (2nd` (g` (m + 1)))