Theorem bcthlem20 8018

Description: Lemma for bcth 8032. A weaker version of bcthlem19 8017.

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
bcthlem20	|- (((n e. NN /\ m <_ n) /\ ((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))) < (2nd` (g` m)))

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 bcthlem20

Step	Hyp	Ref	Expression
1		bcthlem18.1	. . . . . . 7 |- D e. CMet
2		cmsmet 7961	. . . . . . 7 |- (D e. CMet -> D e. Met)
3	1, 2	ax-mp 7	. . . . . 6 |- D e. Met
4		bcthlem18.3	. . . . . . 7 |- X = dom dom D
5	4	metcl 7811	. . . . . 6 |- ((D e. Met /\ (1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
6	3, 5	mp3an1 903	. . . . 5 |- (((1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
7		bcthlem18.7	. . . . . . . 8 |- A = (X X. {x e. RR | 0 < x})
8	7	bcthlem4 8002	. . . . . . 7 |- ((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	. . . . . 6 |- ((g:NN-->A /\ m e. NN) -> (1st` (g` m)) e. X)
10	9	adantl 388	. . . . 5 |- ((n e. NN /\ (g:NN-->A /\ m e. NN)) -> (1st` (g` m)) e. X)
11	7	bcthlem4 8002	. . . . . . . 8 |- ((g:NN-->A /\ n e. NN) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
12	11	pm3.26d 321	. . . . . . 7 |- ((g:NN-->A /\ n e. NN) -> (1st` (g` n)) e. X)
13	12	ancoms 436	. . . . . 6 |- ((n e. NN /\ g:NN-->A) -> (1st` (g` n)) e. X)
14	13	adantrr 395	. . . . 5 |- ((n e. NN /\ (g:NN-->A /\ m e. NN)) -> (1st` (g` n)) e. X)
15	6, 10, 14	sylanc 471	. . . 4 |- ((n e. NN /\ (g:NN-->A /\ m e. NN)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
16	15	adantlr 393	. . 3 |- (((n e. NN /\ m <_ n) /\ (g:NN-->A /\ m e. NN)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
17	16	adantrlr 401	. 2 |- (((n e. NN /\ m <_ n) /\ ((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))) e. RR)
18	8	pm3.27d 325	. . . . . 6 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
19	18	pm3.26d 321	. . . . 5 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. RR)
20		rehalfclt 6034	. . . . 5 |- ((2nd` (g` m)) e. RR -> ((2nd` (g` m)) / 2) e. RR)
21	19, 20	syl 10	. . . 4 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) / 2) e. RR)
22	21	adantlr 393	. . 3 |- (((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN) -> ((2nd` (g` m)) / 2) e. RR)
23	22	adantl 388	. 2 |- (((n e. NN /\ m <_ n) /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> ((2nd` (g` m)) / 2) e. RR)
24	19	adantlr 393	. . 3 |- (((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN) -> (2nd` (g` m)) e. RR)
25	24	adantl 388	. 2 |- (((n e. NN /\ m <_ n) /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> (2nd` (g` m)) e. RR)
26		leloet 5518	. . . . . . 7 |- ((m e. RR /\ n e. RR) -> (m <_ n <-> (m < n \/ m = n)))
27		nnret 5929	. . . . . . 7 |- (m e. NN -> m e. RR)
28		nnret 5929	. . . . . . 7 |- (n e. NN -> n e. RR)
29	26, 27, 28	syl2an 454	. . . . . 6 |- ((m e. NN /\ n e. NN) -> (m <_ n <-> (m < n \/ m = n)))
30		bcthlem18.6	. . . . . . . . . . . . . . . 16 |- 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))})}
31		bcthlem18.8	. . . . . . . . . . . . . . . 16 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
32	1, 4, 30, 7, 31	bcthlem19 8017	. . . . . . . . . . . . . . 15 |- (((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))
33	32	ex 373	. . . . . . . . . . . . . 14 |- ((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)))
34	33	ex 373	. . . . . . . . . . . . 13 |- (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))))
35	34	exp3a 375	. . . . . . . . . . . 12 |- (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)))))
36	35	com34 36	. . . . . . . . . . 11 |- (n e. NN -> ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) -> (m < n -> (m e. NN -> ((1st` (g` m))D(1st` (g` n))) < ((2nd` (g` m)) / 2)))))
37	36	com24 37	. . . . . . . . . 10 |- (n e. NN -> (m e. NN -> (m < n -> ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) -> ((1st` (g` m))D(1st` (g` n))) < ((2nd` (g` m)) / 2)))))
38	37	com12 11	. . . . . . . . 9 |- (m e. NN -> (n e. NN -> (m < n -> ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) -> ((1st` (g` m))D(1st` (g` n))) < ((2nd` (g` m)) / 2)))))
39	38	imp31 362	. . . . . . . 8 |- (((m e. NN /\ n e. NN) /\ m < n) -> ((g:NN-->A /\ A.k e. NN (g