MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmmcvg Structured version   Visualization version   GIF version

Theorem lmmcvg 25473
Description: Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
Hypotheses
Ref Expression
lmmbr.2 𝐽 = (MetOpen‘𝐷)
lmmbr.3 (𝜑𝐷 ∈ (∞Met‘𝑋))
lmmbr3.5 𝑍 = (ℤ𝑀)
lmmbr3.6 (𝜑𝑀 ∈ ℤ)
lmmbrf.7 ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐴)
lmmcvg.8 (𝜑𝐹(⇝𝑡𝐽)𝑃)
lmmcvg.9 (𝜑𝑅 ∈ ℝ+)
Assertion
Ref Expression
lmmcvg (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅))
Distinct variable groups:   𝑗,𝑘,𝐷   𝑗,𝐹,𝑘   𝑃,𝑗,𝑘   𝑗,𝑋,𝑘   𝑗,𝑀   𝜑,𝑗,𝑘   𝑅,𝑗,𝑘   𝑗,𝑍,𝑘
Allowed substitution hints:   𝐴(𝑗, 𝑘)   𝐽(𝑗, 𝑘)   𝑀(𝑘)

Proof of Theorem lmmcvg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 breq2 5115 . . . . 5 (𝑥 = 𝑅 → (((𝐹𝑘)𝐷𝑃) < 𝑥 ↔ ((𝐹𝑘)𝐷𝑃) < 𝑅))
213anbi3d 1470 . . . 4 (𝑥 = 𝑅 → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑥) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅)))
32rexralbidv 3233 . . 3 (𝑥 = 𝑅 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑥) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅)))
4 lmmcvg.8 . . . . 5 (𝜑𝐹(⇝𝑡𝐽)𝑃)
5 lmmbr.2 . . . . . 6 𝐽 = (MetOpen‘𝐷)
6 lmmbr.3 . . . . . 6 (𝜑𝐷 ∈ (∞Met‘𝑋))
7 lmmbr3.5 . . . . . 6 𝑍 = (ℤ𝑀)
8 lmmbr3.6 . . . . . 6 (𝜑𝑀 ∈ ℤ)
95, 6, 7, 8lmmbr3 25472 . . . . 5 (𝜑 → (𝐹(⇝𝑡𝐽)𝑃 ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ 𝑃𝑋 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑥))))
104, 9mpbid 235 . . . 4 (𝜑 → (𝐹 ∈ (𝑋pm ℂ) ∧ 𝑃𝑋 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑥)))
1110simp3d 1162 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑥))
12 lmmcvg.9 . . 3 (𝜑𝑅 ∈ ℝ+)
133, 11, 12rspcdva 3584 . 2 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅))
147uztrn2 12899 . . . . . 6 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
15 3simpc 1168 . . . . . . 7 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) → ((𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅))
16 lmmbrf.7 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐴)
1716eleq1d 2850 . . . . . . . 8 ((𝜑𝑘𝑍) → ((𝐹𝑘) ∈ 𝑋𝐴𝑋))
1816oveq1d 7434 . . . . . . . . 9 ((𝜑𝑘𝑍) → ((𝐹𝑘)𝐷𝑃) = (𝐴𝐷𝑃))
1918breq1d 5121 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝐹𝑘)𝐷𝑃) < 𝑅 ↔ (𝐴𝐷𝑃) < 𝑅))
2017, 19anbi12d 644 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) ↔ (𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)))
2115, 20imbitrid 247 . . . . . 6 ((𝜑𝑘𝑍) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) → (𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)))
2214, 21sylan2 605 . . . . 5 ((𝜑 ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) → (𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)))
2322anassrs 473 . . . 4 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) → (𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)))
2423ralimdva 3179 . . 3 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) → ∀𝑘 ∈ (ℤ𝑗)(𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)))
2524reximdva 3180 . 2 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑃) < 𝑅) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)))
2613, 25mpd 16 1 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐴𝑋 ∧ (𝐴𝐷𝑃) < 𝑅))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wa 401  w3a 1103   = wceq 1570  wcel 2146  wral 3081  wrex 3091   class class class wbr 5111  dom cdm 5663  cfv 6540  (class class class)co 7419  pm cpm 8831  cc 11115   < clt 11260  cz 12608  cuz 12880  +crp 13034  ∞Metcxmet 21559  MetOpencmopn 21564  𝑡clm 23435
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194  ax-pre-sup 11195
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-map 8832  df-pm 8833  df-en 8950  df-dom 8951  df-sdom 8952  df-sup 9409  df-inf 9410  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-div 11889  df-nn 12251  df-2 12320  df-n0 12522  df-z 12609  df-uz 12881  df-q 12991  df-rp 13035  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-topgen 17520  df-psmet 21566  df-xmet 21567  df-bl 21569  df-mopn 21570  df-top 23103  df-topon 23120  df-bases 23155  df-lm 23438
This theorem is used by:  bfplem2  38534
  Copyright terms: Public domain W3C validator