Theorem bcthlem19 8014

Description: Lemma for bcth 8029. The distance between the center of a ball at m and any later ball in sequence g is less than half the radius of the ball at m.

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
bcthlem19	|- (((n e. NN /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) /\ m < n) -> ((1st` (g` m))D(1st` (g` n))) < ((2nd` (g` m)) / 2))

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

Proof of Theorem bcthlem19

Step	Hyp	Ref	Expression
1		bcthlem18.1	. . . . 5 |- D e. CMet
2		bcthlem18.3	. . . . 5 |- X = dom dom D
3		bcthlem18.6	. . . . 5 |- 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.7	. . . . 5 |- A = (X X. {x e. RR | 0 < x})
5		bcthlem18.8	. . . . 5 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
6	1, 2, 3, 4, 5	bcthlem18 8013	. . . 4 |- (n e. NN -> (((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN) -> (m < n -> ((1st` (g` n))( ball ` D)(2nd` (g` n))) (_ ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)))))
7	6	imp31 362	. . 3 |- (((n e. NN /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) /\ m < n) -> ((1st` (g` n))( ball ` D)(2nd` (g` n))) (_ ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)))
8	4	bcthlem4 7999	. . . . . . . 8 |- ((g:NN-->A /\ n e. NN) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
9	8	ancoms 438	. . . . . . 7 |- ((n e. NN /\ g:NN-->A) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
10	1	cmsmeti 7959	. . . . . . . 8 |- D e. Met
11	2	blcntr 7842	. . . . . . . 8 |- (((D e. Met /\ (1st` (g` n)) e. X) /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))) -> (1st` (g` n)) e. ((1st` (g` n))( ball ` D)(2nd` (g` n))))
12	10, 11	mpanl1 708	. . . . . . 7 |- (((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))) -> (1st` (g` n)) e. ((1st` (g` n))( ball ` D)(2nd` (g` n))))
13	9, 12	syl 10	. . . . . 6 |- ((n e. NN /\ g:NN-->A) -> (1st` (g` n)) e. ((1st` (g` n))( ball ` D)(2nd` (g` n))))
14	13	adantrr 397	. . . . 5 |- ((n e. NN /\ (g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (1st` (g` n)) e. ((1st` (g` n))( ball ` D)(2nd` (g` n))))
15	14	adantrr 397	. . . 4 |- ((n e. NN /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> (1st` (g` n)) e. ((1st` (g` n))( ball ` D)(2nd` (g` n))))
16	15	adantr 391	. . 3 |- (((n e. NN /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) /\ m < n) -> (1st` (g` n)) e. ((1st` (g` n))( ball ` D)(2nd` (g` n))))
17	7, 16	sseldd 2071	. 2 |- (((n e. NN /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) /\ m < n) -> (1st` (g` n)) e. ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)))
18	2	elbl2 7836	. . . . . . 7 |- (((D e. Met /\ (1st` (g` m)) e. X /\ (1st` (g` n)) e. X) /\ (((2nd` (g` m)) / 2) e. RR /\ 0 < ((2nd` (g` m)) / 2))) -> ((1st` (g` n)) e. ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)) <-> ((1st` (g` m))D(1st` (g` n))) < ((2nd` (g` m)) / 2)))
19	10, 18	mp3anl1 912	. . . . . 6 |- ((((1st` (g` m)) e. X /\ (1st` (g` n)) e. X) /\ (((2nd` (g` m)) / 2) e. RR /\ 0 < ((2nd` (g` m)) / 2))) -> ((1st` (g` n)) e. ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)) <-> ((1st` (g` m))D(1st` (g` n))) < ((2nd` (g` m)) / 2)))
20	4	bcthlem4 7999	. . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> ((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))))
21	20	pm3.26d 321	. . . . . . . 8 |- ((g:NN-->A /\ m e. NN) -> (1st` (g` m)) e. X)
22	21	adantr 391	. . . . . . 7 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> (1st` (g` m)) e. X)
23	8	pm3.26d 321	. . . . . . . 8 |- ((g:NN-->A /\ n e. NN) -> (1st` (g` n)) e. X)
24	23	adantlr 395	. . . . . . 7 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> (1st` (g` n)) e. X)
25	22, 24	jca 288	. . . . . 6 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> ((1st` (g` m)) e. X /\ (1st` (g` n)) e. X))
26	20	pm3.27d 325	. . . . . . . 8 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
27		rehalfclt 6036	. . . . . . . . . 10 |- ((2nd` (g` m)) e. RR -> ((2nd` (g` m)) / 2) e. RR)
28	27	adantr 391	. . . . . . . . 9 |- (((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))) -> ((2nd` (g` m)) / 2) e. RR)
29		halfpos2t 6039	. . . . . . . . . 10 |- ((2nd` (g` m)) e. RR -> (0 < (2nd` (g` m)) <-> 0 < ((2nd` (g` m)) / 2)))
30	29	biimpa 418	. . . . . . . . 9 |- (((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))) -> 0 < ((2nd` (g` m)) / 2))
31	28, 30	jca 288	. . . . . . . 8 |- (((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))) -> (((2nd` (g` m)) / 2) e. RR /\ 0 < ((2nd` (g` m)) / 2)))
32	26, 31	syl 10	. . . . . . 7 |- ((g:NN-->A /\ m e. NN) -> (((2nd` (g` m)) / 2) e. RR /\ 0 < ((2nd` (g` m)) / 2)