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

Theorem lmclimf 24743
Description: Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
Hypotheses
Ref Expression
lmclim.2 𝐽 = (TopOpen‘ℂfld)
lmclim.3 𝑍 = (ℤ𝑀)
Assertion
Ref Expression
lmclimf ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → (𝐹(⇝𝑡𝐽)𝑃𝐹𝑃))

Proof of Theorem lmclimf
StepHypRef Expression
1 simpr 485 . . 3 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → 𝐹:𝑍⟶ℂ)
2 lmclim.3 . . . 4 𝑍 = (ℤ𝑀)
3 uzssz 12820 . . . . 5 (ℤ𝑀) ⊆ ℤ
4 zsscn 12543 . . . . 5 ℤ ⊆ ℂ
53, 4sstri 3982 . . . 4 (ℤ𝑀) ⊆ ℂ
62, 5eqsstri 4007 . . 3 𝑍 ⊆ ℂ
7 cnex 11168 . . . 4 ℂ ∈ V
8 elpm2r 8817 . . . 4 (((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝑍⟶ℂ ∧ 𝑍 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm ℂ))
97, 7, 8mpanl12 700 . . 3 ((𝐹:𝑍⟶ℂ ∧ 𝑍 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm ℂ))
101, 6, 9sylancl 586 . 2 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → 𝐹 ∈ (ℂ ↑pm ℂ))
11 fdm 6708 . . . 4 (𝐹:𝑍⟶ℂ → dom 𝐹 = 𝑍)
12 eqimss2 4032 . . . 4 (dom 𝐹 = 𝑍𝑍 ⊆ dom 𝐹)
131, 11, 123syl 18 . . 3 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → 𝑍 ⊆ dom 𝐹)
14 lmclim.2 . . . 4 𝐽 = (TopOpen‘ℂfld)
1514, 2lmclim 24742 . . 3 ((𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹) → (𝐹(⇝𝑡𝐽)𝑃 ↔ (𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝐹𝑃)))
1613, 15syldan 591 . 2 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → (𝐹(⇝𝑡𝐽)𝑃 ↔ (𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝐹𝑃)))
1710, 16mpbirand 705 1 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → (𝐹(⇝𝑡𝐽)𝑃𝐹𝑃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  Vcvv 3469  wss 3939   class class class wbr 5136  dom cdm 5664  wf 6523  cfv 6527  (class class class)co 7388  pm cpm 8799  cc 11085  cz 12535  cuz 12799  cli 15405  TopOpenctopn 17344  fldccnfld 20871  𝑡clm 22652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5273  ax-sep 5287  ax-nul 5294  ax-pow 5351  ax-pr 5415  ax-un 7703  ax-cnex 11143  ax-resscn 11144  ax-1cn 11145  ax-icn 11146  ax-addcl 11147  ax-addrcl 11148  ax-mulcl 11149  ax-mulrcl 11150  ax-mulcom 11151  ax-addass 11152  ax-mulass 11153  ax-distr 11154  ax-i2m1 11155  ax-1ne0 11156  ax-1rid 11157  ax-rnegex 11158  ax-rrecex 11159  ax-cnre 11160  ax-pre-lttri 11161  ax-pre-lttrn 11162  ax-pre-ltadd 11163  ax-pre-mulgt0 11164  ax-pre-sup 11165
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3374  df-reu 3375  df-rab 3429  df-v 3471  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3958  df-nul 4314  df-if 4518  df-pw 4593  df-sn 4618  df-pr 4620  df-tp 4622  df-op 4624  df-uni 4897  df-iun 4987  df-br 5137  df-opab 5199  df-mpt 5220  df-tr 5254  df-id 5562  df-eprel 5568  df-po 5576  df-so 5577  df-fr 5619  df-we 5621  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6284  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7344  df-ov 7391  df-oprab 7392  df-mpo 7393  df-om 7834  df-1st 7952  df-2nd 7953  df-frecs 8243  df-wrecs 8274  df-recs 8348  df-rdg 8387  df-1o 8443  df-er 8681  df-map 8800  df-pm 8801  df-en 8918  df-dom 8919  df-sdom 8920  df-fin 8921  df-sup 9414  df-inf 9415  df-pnf 11227  df-mnf 11228  df-xr 11229  df-ltxr 11230  df-le 11231  df-sub 11423  df-neg 11424  df-div 11849  df-nn 12190  df-2 12252  df-3 12253  df-4 12254  df-5 12255  df-6 12256  df-7 12257  df-8 12258  df-9 12259  df-n0 12450  df-z 12536  df-dec 12655  df-uz 12800  df-q 12910  df-rp 12952  df-xneg 13069  df-xadd 13070  df-xmul 13071  df-fz 13462  df-seq 13944  df-exp 14005  df-cj 15023  df-re 15024  df-im 15025  df-sqrt 15159  df-abs 15160  df-clim 15409  df-struct 17057  df-slot 17092  df-ndx 17104  df-base 17122  df-plusg 17187  df-mulr 17188  df-starv 17189  df-tset 17193  df-ple 17194  df-ds 17196  df-unif 17197  df-rest 17345  df-topn 17346  df-topgen 17366  df-psmet 20863  df-xmet 20864  df-met 20865  df-bl 20866  df-mopn 20867  df-cnfld 20872  df-top 22318  df-topon 22335  df-bases 22371  df-lm 22655
This theorem is referenced by:  lmlim  32693  climreeq  44039
  Copyright terms: Public domain W3C validator