Theorem bcthlem24 7972

Description: Lemma for bcth 7982. An upper limit for the distance between a ball center at m and the convergence point q, in terms of any later ball center at n.

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

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

Proof of Theorem bcthlem24

Step	Hyp	Ref	Expression
1		bcthlem18.1	. . . . . . . . 9 |- D e. CMet
2	1	cmsmeti 7913	. . . . . . . 8 |- D e. Met
3		bcthlem18.3	. . . . . . . . 9 |- X = dom dom D
4	3	metcl 7761	. . . . . . . 8 |- ((D e. Met /\ ((1st o. g)` m) e. X /\ q e. X) -> (((1st o. g)` m)Dq) e. RR)
5	2, 4	mp3an1 901	. . . . . . 7 |- ((((1st o. g)` m) e. X /\ q e. X) -> (((1st o. g)` m)Dq) e. RR)
6		bcthlem3 7951	. . . . . . . 8 |- ((g:NN-->A /\ m e. NN) -> ((1st o. g)` m) = (1st` (g` m)))
7		bcthlem18.7	. . . . . . . . . 10 |- A = (X X. {x e. RR | 0 < x})
8	7	bcthlem4 7952	. . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> ((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))))
9	8	pm3.26d 321	. . . . . . . 8 |- ((g:NN-->A /\ m e. NN) -> (1st` (g` m)) e. X)
10	6, 9	eqeltrd 1545	. . . . . . 7 |- ((g:NN-->A /\ m e. NN) -> ((1st o. g)` m) e. X)
11	5, 10	sylan 448	. . . . . 6 |- (((g:NN-->A /\ m e. NN) /\ q e. X) -> (((1st o. g)` m)Dq) e. RR)
12	11	adantrl 394	. . . . 5 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> (((1st o. g)` m)Dq) e. RR)
13	12	ancoms 436	. . . 4 |- (((n e. NN /\ q e. X) /\ (g:NN-->A /\ m e. NN)) -> (((1st o. g)` m)Dq) e. RR)
14	13	adantrlr 401	. . 3 |- (((n e. NN /\ q e. X) /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> (((1st o. g)` m)Dq) e. RR)
15	14	adantr 389	. 2 |- ((((n e. NN /\ q e. X) /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) /\ m < n) -> (((1st o. g)` m)Dq) e. RR)
16		axaddrcl 5252	. . . . . 6 |- ((((1st` (g` m))D(1st` (g` n))) e. RR /\ (((1st o. g)` n)Dq) e. RR) -> (((1st` (g` m))D(1st` (g` n))) + (((1st o. g)` n)Dq)) e. RR)
17	3	metcl 7761	. . . . . . . . 9 |- ((D e. Met /\ (1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
18	2, 17	mp3an1 901	. . . . . . . 8 |- (((1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
19	9	adantr 389	. . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> (1st` (g` m)) e. X)
20	7	bcthlem4 7952	. . . . . . . . . 10 |- ((g:NN-->A /\ n e. NN) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
21	20	pm3.26d 321	. . . . . . . . 9 |- ((g:NN-->A /\ n e. NN) -> (1st` (g` n)) e. X)
22	21	adantlr 393	. . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> (1st` (g` n)) e. X)
23	18, 19, 22	sylanc 471	. . . . . . 7 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
24	23	adantrr 395	. . . . . 6 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
25	3	metcl 7761	. . . . . . . . . 10 |- ((D e. Met /\ ((1st o. g)` n) e. X /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
26	2, 25	mp3an1 901	. . . . . . . . 9 |- ((((1st o. g)` n) e. X /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
27		bcthlem3 7951	. . . . . . . . . 10 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) = (1st` (g` n)))
28	27, 21	eqeltrd 1545	. . . . . . . . 9 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) e. X)
29	26, 28	sylan 448	. . . . . . . 8 |- (((g:NN-->A /\ n e. NN) /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
30	29	anasss 440	. . . . . . 7 |- ((g:NN-->A /\ (n e. NN /\ q e. X)) -> (((1st o. g)` n)Dq) e. RR)
31	30	adantlr 393	. . . . . 6 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> (((1st o. g)` n)Dq) e. RR)
32	16, 24, 31	sylanc 471	. . . . 5 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> (((1st` (g` m))D(1st` (g` n))) + (((1st o. g)` n)Dq)) e. RR)
33	32	ancoms 436	. . . 4 |- (((n e. NN /\ q e. X) /\ (g:NN-->A /\ m e. NN)) -> (((1st` (g` m))D(1st` (g` n))) + (((1st o. g)` n)Dq)) e. RR)
34	33	adantrlr 401	. . 3 |- (((n e. NN /\ q e. X) /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> (((1st` (g` m))D(1st` (g` n))) + (((1st o. g)` n)Dq)) e. RR)
35	34	adantr 389	. 2 |- ((((n e. NN /\ q e. X) /\ ((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))) + (((1st o. g)` n)Dq)) e. RR)
36		axaddrcl 5252	. . . . . 6 |- ((((2nd` (g` m)) / 2) e. RR /\ (((1st o. g)` n)Dq) e. RR) -> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) e. RR)
37	8	pm3.27d 325	. . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
38	37	pm3.26d 321	. . . . . . . 8 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. RR)
39		rehalfclt 5989	. . . . . . . 8 |- ((2nd` (g` m)) e. RR -> ((2nd` (g` m)) / 2) e. RR)
40	38, 39	syl 10	. . . . . . 7 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) / 2) e. RR)
41	40	adantr 389	. . . . . 6 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((2nd` (g` m)) / 2) e. RR)
42	36, 41, 31	sylanc 471	. . . . 5 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN