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

Theorem cncff 22918
Description: A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
Assertion
Ref Expression
cncff (𝐹 ∈ (𝐴cn𝐵) → 𝐹:𝐴𝐵)

Proof of Theorem cncff
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cncfrss 22916 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
2 cncfrss2 22917 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐵 ⊆ ℂ)
3 elcncf 22914 . . . 4 ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
41, 2, 3syl2anc 696 . . 3 (𝐹 ∈ (𝐴cn𝐵) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
54ibi 256 . 2 (𝐹 ∈ (𝐴cn𝐵) → (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
65simpld 477 1 (𝐹 ∈ (𝐴cn𝐵) → 𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2140  wral 3051  wrex 3052  wss 3716   class class class wbr 4805  wf 6046  cfv 6050  (class class class)co 6815  cc 10147   < clt 10287  cmin 10479  +crp 12046  abscabs 14194  cnccncf 22901
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-cnex 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-map 8028  df-cncf 22903
This theorem is referenced by:  cncfss  22924  climcncf  22925  cncfco  22932  cncfmpt1f  22938  cncfmpt2ss  22940  negfcncf  22944  divcncf  23437  ivth2  23445  ivthicc  23448  evthicc2  23450  cniccbdd  23451  volivth  23596  cncombf  23645  cnmbf  23646  cniccibl  23827  cnmptlimc  23874  cpnord  23918  cpnres  23920  dvrec  23938  rollelem  23972  rolle  23973  cmvth  23974  mvth  23975  dvlip  23976  c1liplem1  23979  c1lip1  23980  c1lip2  23981  dveq0  23983  dvgt0lem1  23985  dvgt0lem2  23986  dvgt0  23987  dvlt0  23988  dvge0  23989  dvle  23990  dvivthlem1  23991  dvivth  23993  dvne0  23994  dvne0f1  23995  dvcnvrelem1  24000  dvcnvrelem2  24001  dvcnvre  24002  dvcvx  24003  dvfsumle  24004  dvfsumge  24005  dvfsumabs  24006  ftc1cn  24026  ftc2  24027  ftc2ditglem  24028  ftc2ditg  24029  itgparts  24030  itgsubstlem  24031  itgsubst  24032  ulmcn  24373  psercn  24400  pserdvlem2  24402  pserdv  24403  sincn  24418  coscn  24419  logtayl  24627  dvcncxp1  24705  leibpi  24890  lgamgulmlem2  24977  ftc2re  31007  fdvposlt  31008  fdvneggt  31009  fdvposle  31010  fdvnegge  31011  ivthALT  32658  knoppcld  32823  knoppndv  32853  cnicciblnc  33813  ftc1cnnclem  33815  ftc1cnnc  33816  ftc2nc  33826  cnioobibld  38320  evthiccabs  40240  cncfmptss  40341  mulc1cncfg  40343  expcnfg  40345  mulcncff  40603  cncfshift  40609  subcncff  40615  cncfcompt  40618  addcncff  40619  cncficcgt0  40623  divcncff  40626  cncfiooicclem1  40628  cncfiooiccre  40630  cncfioobd  40632  cncfcompt2  40634  dvsubcncf  40661  dvmulcncf  40662  dvdivcncf  40664  ioodvbdlimc1lem1  40668  cnbdibl  40700  itgsubsticclem  40713  itgsubsticc  40714  itgioocnicc  40715  iblcncfioo  40716  itgiccshift  40718  itgsbtaddcnst  40720  fourierdlem18  40864  fourierdlem32  40878  fourierdlem33  40879  fourierdlem39  40885  fourierdlem48  40893  fourierdlem49  40894  fourierdlem58  40903  fourierdlem59  40904  fourierdlem71  40916  fourierdlem73  40918  fourierdlem81  40926  fourierdlem84  40929  fourierdlem85  40930  fourierdlem88  40933  fourierdlem94  40939  fourierdlem97  40942  fourierdlem101  40946  fourierdlem103  40948  fourierdlem104  40949  fourierdlem111  40956  fourierdlem112  40957  fourierdlem113  40958  fouriercn  40971
  Copyright terms: Public domain W3C validator