Metamath Proof Explorer

Theorem lmmcvg

Description: Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
lmmbr.3 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
lmmbr3.5 ${⊢}{Z}={ℤ}_{\ge {M}}$
lmmbr3.6 ${⊢}{\phi }\to {M}\in ℤ$
lmmbrf.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={A}$
lmmcvg.8
lmmcvg.9 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
Assertion lmmcvg ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({A}\in {X}\wedge {A}{D}{P}<{R}\right)$

Proof

Step Hyp Ref Expression
1 lmmbr.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 lmmbr.3 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
3 lmmbr3.5 ${⊢}{Z}={ℤ}_{\ge {M}}$
4 lmmbr3.6 ${⊢}{\phi }\to {M}\in ℤ$
5 lmmbrf.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={A}$
6 lmmcvg.8
7 lmmcvg.9 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
8 breq2 ${⊢}{x}={R}\to \left({F}\left({k}\right){D}{P}<{x}↔{F}\left({k}\right){D}{P}<{R}\right)$
9 8 3anbi3d ${⊢}{x}={R}\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\right)$
10 9 rexralbidv ${⊢}{x}={R}\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\right)$
11 1 2 3 4 lmmbr3
12 6 11 mpbid ${⊢}{\phi }\to \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
13 12 simp3d ${⊢}{\phi }\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)$
14 10 13 7 rspcdva ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)$
15 3 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
16 3simpc ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\to \left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)$
17 5 eleq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right)\in {X}↔{A}\in {X}\right)$
18 5 oveq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right){D}{P}={A}{D}{P}$
19 18 breq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right){D}{P}<{R}↔{A}{D}{P}<{R}\right)$
20 17 19 anbi12d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)↔\left({A}\in {X}\wedge {A}{D}{P}<{R}\right)\right)$
21 16 20 syl5ib ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\to \left({A}\in {X}\wedge {A}{D}{P}<{R}\right)\right)$
22 15 21 sylan2 ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\to \left({A}\in {X}\wedge {A}{D}{P}<{R}\right)\right)$
23 22 anassrs ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\to \left({A}\in {X}\wedge {A}{D}{P}<{R}\right)\right)$
24 23 ralimdva ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({A}\in {X}\wedge {A}{D}{P}<{R}\right)\right)$
25 24 reximdva ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{R}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({A}\in {X}\wedge {A}{D}{P}<{R}\right)\right)$
26 14 25 mpd ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({A}\in {X}\wedge {A}{D}{P}<{R}\right)$