HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem bcthlem26 8024
Description: Lemma for bcth 8032. The convergence point q belongs to every ball in sequence g.
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
bcthlem26 |- (((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` D)q) -> q e. ((1st` (g` m))( ball ` D)(2nd` (g` m))))
Distinct variable groups:   j,m,q,y,z,A   j,p,r,D,m,q,y,z   k,m,q,F   j,J,p,r,y,z   j,M,p,r,y,z   z,O   j,X,m,p,q,r,y,z   j,k,x,g,p,r,y,z,m,q
Proof of Theorem bcthlem26
StepHypRef Expression
1 bcthlem18.1 . . . . . 6 |- D e. CMet
2 bcthlem18.3 . . . . . 6 |- X = dom dom D
3 bcthlem18.7 . . . . . 6 |- A = (X X. {x e. RR | 0 < x})
41, 2, 3bcthlem13 8011 . . . . 5 |- (((g:NN-->A /\ m e. NN) /\ (1st o. g)(~~>m` D)q) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2)))
54adantllr 397 . . . 4 |- ((((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN) /\ (1st o. g)(~~>m` D)q) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2)))
65adantll 392 . . 3 |- (((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` D)q) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2)))
7 bcthlem3 8001 . . . . . . . . . . . . . 14 |- ((g:NN-->A /\ m e. NN) -> ((1st o. g)` m) = (1st` (g` m)))
87opreq1d 3975 . . . . . . . . . . . . 13 |- ((g:NN-->A /\ m e. NN) -> (((1st o. g)` m)Dq) = ((1st` (g` m))Dq))
98adantlr 393 . . . . . . . . . . . 12 |- (((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN) -> (((1st o. g)` m)Dq) = ((1st` (g` m))Dq))
109adantl 388 . . . . . . . . . . 11 |- (((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) = ((1st` (g` m))Dq))
1110ad2antrr 404 . . . . . . . . . 10 |- (((((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) = ((1st` (g` m))Dq))
12 bcthlem18.6 . . . . . . . . . . 11 |- 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))})}
13 bcthlem18.8 . . . . . . . . . . 11 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
141, 2, 12, 3, 13bcthlem25 8023 . . . . . . . . . 10 |- (((((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)))
1511, 14eqbrtrrd 2637 . . . . . . . . 9 |- (((((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` (g` m))Dq) < (2nd` (g` m)))
1615exp31 376 . . . . . . . 8 |- (((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` (g` m))Dq) < (2nd` (g` m)))))
1716imp3a 361 . . . . . . 7 |- (((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` (g` m))Dq) < (2nd` (g` m))))
1817anasss 440 . . . . . 6 |- ((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` (g` m))Dq) < (2nd` (g` m))))
1918expcom 374 . . . . 5 |- ((q e. X /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> (n e. NN -> ((m < n /\ (((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2)) -> ((1st` (g` m))Dq) < (2nd` (g` m)))))
2019r19.23adv 1746 . . . 4 |- ((q e. X /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> (E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2)) -> ((1st` (g` m))Dq) < (2nd` (g` m))))
2120adantr 389 . . 3 |- (((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` D)q) -> (E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < ((2nd` (g` m)) / 2)) -> ((1st` (g` m))Dq) < (2nd` (g` m))))
226, 21mpd 26 . 2 |- (((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` D)q) -> ((1st` (g` m))Dq) < (2nd` (g` m)))
231cmsmeti 7962 . . . . . 6 |- D e. Met
242elbl2 7839 . . . . . 6 |- (((D e. Met /\ (1st` (g` m)) e. X /\ q e. X) /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))) -> (q e. ((1st` (g` m))( ball ` D)(2nd` (g` m))) <-> ((1st` (g` m))Dq) < (2nd` (g`