Theorem bcthlem25 7985

Description: Lemma for bcth 7994. Helper lemma to remove the dependence on n of the upper limit in bcthlem24 7984.

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
bcthlem25	|- (((((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)` n)Dq) < ((2nd` (g` m)) / 2)) -> (((1st o. g)` m)Dq) < (2nd` (g` m)))

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 bcthlem25

Step	Hyp	Ref	Expression
1		ltadd2t 5608	. . . . . . . 8 |- (((((1st o. g)` n)Dq) e. RR /\ ((2nd` (g` m)) / 2) e. RR /\ ((2nd` (g` m)) / 2) e. RR) -> ((((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2))))
2		bcthlem18.1	. . . . . . . . . . . . 13 |- D e. CMet
3	2	cmsmeti 7924	. . . . . . . . . . . 12 |- D e. Met
4		bcthlem18.3	. . . . . . . . . . . . 13 |- X = dom dom D
5	4	metcl 7771	. . . . . . . . . . . 12 |- ((D e. Met /\ ((1st o. g)` n) e. X /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
6	3, 5	mp3an1 902	. . . . . . . . . . 11 |- ((((1st o. g)` n) e. X /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
7		bcthlem3 7963	. . . . . . . . . . . 12 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) = (1st` (g` n)))
8		bcthlem18.7	. . . . . . . . . . . . . 14 |- A = (X X. {x e. RR | 0 < x})
9	8	bcthlem4 7964	. . . . . . . . . . . . 13 |- ((g:NN-->A /\ n e. NN) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
10	9	pm3.26d 321	. . . . . . . . . . . 12 |- ((g:NN-->A /\ n e. NN) -> (1st` (g` n)) e. X)
11	7, 10	eqeltrd 1546	. . . . . . . . . . 11 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) e. X)
12	6, 11	sylan 448	. . . . . . . . . 10 |- (((g:NN-->A /\ n e. NN) /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
13	12	anasss 440	. . . . . . . . 9 |- ((g:NN-->A /\ (n e. NN /\ q e. X)) -> (((1st o. g)` n)Dq) e. RR)
14	13	adantlr 393	. . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> (((1st o. g)` n)Dq) e. RR)
15	8	bcthlem4 7964	. . . . . . . . . . . 12 |- ((g:NN-->A /\ m e. NN) -> ((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))))
16	15	pm3.27d 325	. . . . . . . . . . 11 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
17	16	pm3.26d 321	. . . . . . . . . 10 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. RR)
18		rehalfclt 5991	. . . . . . . . . 10 |- ((2nd` (g` m)) e. RR -> ((2nd` (g` m)) / 2) e. RR)
19	17, 18	syl 10	. . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) / 2) e. RR)
20	19	adantr 389	. . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((2nd` (g` m)) / 2) e. RR)
21	1, 14, 20, 20	syl3anc 857	. . . . . . 7 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2))))
22	17	recnd 5298	. . . . . . . . . 10 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. CC)
23		2halvest 5996	. . . . . . . . . 10 |- ((2nd` (g` m)) e. CC -> (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2)) = (2nd` (g` m)))
24	22, 23	syl 10	. . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2)) = (2nd` (g` m)))
25	24	adantr 389	. . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2)) = (2nd` (g` m)))
26	25	breq2d 2626	. . . . . . 7 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2)) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (2nd` (g` m))))
27	21, 26	bitrd 527	. . . . . 6 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (2nd` (g` m))))
28	27	ancoms 436	. . . . 5 |- (((n e. NN /\ q e. X) /\ (g:NN-->A /\ m e. NN)) -> ((((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (2nd` (g` m))))
29	28	adantrlr 401	. . . 4 |- (((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)` n)Dq) < ((2nd` (g` m)) / 2) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (2nd` (g` m))))
30	29	adantr 389	. . 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)) /\ m < n) -> ((((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2) <-> (((2nd` (g` m)) / 2) + (((1st o. g)` n)Dq)) < (2nd` (g` m))))
31		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))})}
32		bcthlem18.8	. . . . 5 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
33	2, 4, 31, 8, 32	bcthlem24 7984	. . . 4 |- ((((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) <