HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem bcthlem25 7957
Description: Lemma for bcth 7966. Helper lemma to remove the dependence on n of the upper limit in bcthlem24 7956.
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
StepHypRef Expression
1 ltadd2t 5598 . . . . . . . 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
32cmsmeti 7897 . . . . . . . . . . . 12 |- D e. Met
4 bcthlem18.3 . . . . . . . . . . . . 13 |- X = dom dom D
54metcl 7750 . . . . . . . . . . . 12 |- ((D e. Met /\ ((1st o. g)` n) e. X /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
63, 5mp3an1 900 . . . . . . . . . . 11 |- ((((1st o. g)` n) e. X /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
7 bcthlem3 7935 . . . . . . . . . . . 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})
98bcthlem4 7936 . . . . . . . . . . . . 13 |- ((g:NN-->A /\ n e. NN) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
109pm3.26d 321 . . . . . . . . . . . 12 |- ((g:NN-->A /\ n e. NN) -> (1st` (g` n)) e. X)
117, 10eqeltrd 1540 . . . . . . . . . . 11 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) e. X)
126, 11sylan 448 . . . . . . . . . 10 |- (((g:NN-->A /\ n e. NN) /\ q e. X) -> (((1st o. g)` n)Dq) e. RR)
1312anasss 440 . . . . . . . . 9 |- ((g:NN-->A /\ (n e. NN /\ q e. X)) -> (((1st o. g)` n)Dq) e. RR)
1413adantlr 393 . . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> (((1st o. g)` n)Dq) e. RR)
158bcthlem4 7936 . . . . . . . . . . . 12 |- ((g:NN-->A /\ m e. NN) -> ((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))))
1615pm3.27d 325 . . . . . . . . . . 11 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
1716pm3.26d 321 . . . . . . . . . 10 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. RR)
18 rehalfclt 5981 . . . . . . . . . 10 |- ((2nd` (g` m)) e. RR -> ((2nd` (g` m)) / 2) e. RR)
1917, 18syl 10 . . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) / 2) e. RR)
2019adantr 389 . . . . . . . 8 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ q e. X)) -> ((2nd` (g` m)) / 2) e. RR)
211, 14, 20, 20syl3anc 856 . . . . . . 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))))
2217recnd 5287 . . . . . . . . . 10 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. CC)
23 2halvest 5986 . . . . . . . . . 10 |- ((2nd` (g` m)) e. CC -> (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2)) = (2nd` (g` m)))
2422, 23syl 10 . . . . . . . . 9 |- ((g:NN-->A /\ m e. NN) -> (((2nd` (g` m)) / 2) + ((2nd` (g` m)) / 2)) = (2nd` (g` m)))
2524adantr 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)))
2625breq2d 2620 . . . . . . 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))))
2721, 26bitrd 526 . . . . . 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))))
2827ancoms 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))))
2928adantrlr 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))))
3029adantr 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)))
332, 4, 31, 8, 32bcthlem24 7956 . . . 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)