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

Theorem cncff 24279
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 24277 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
2 cncfrss2 24278 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐵 ⊆ ℂ)
3 elcncf 24275 . . . 4 ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
41, 2, 3syl2anc 585 . . 3 (𝐹 ∈ (𝐴cn𝐵) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
54ibi 267 . 2 (𝐹 ∈ (𝐴cn𝐵) → (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
65simpld 496 1 (𝐹 ∈ (𝐴cn𝐵) → 𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  wral 3061  wrex 3070  wss 3914   class class class wbr 5109  wf 6496  cfv 6500  (class class class)co 7361  cc 11057   < clt 11197  cmin 11393  +crp 12923  abscabs 15128  cnccncf 24262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-map 8773  df-cncf 24264
This theorem is referenced by:  cncfss  24285  climcncf  24286  cncfco  24293  cncfcompt2  24294  cncfmpt1f  24300  cncfmpt2ss  24302  negfcncf  24309  divcncf  24834  ivth2  24842  ivthicc  24845  evthicc2  24847  cniccbdd  24848  volivth  24994  cncombf  25045  cnmbf  25046  cniccibl  25228  cnicciblnc  25230  cnmptlimc  25277  cpnord  25322  cpnres  25324  dvrec  25342  rollelem  25376  rolle  25377  cmvth  25378  mvth  25379  dvlip  25380  c1liplem1  25383  c1lip1  25384  c1lip2  25385  dveq0  25387  dvgt0lem1  25389  dvgt0lem2  25390  dvgt0  25391  dvlt0  25392  dvge0  25393  dvle  25394  dvivthlem1  25395  dvivth  25397  dvne0  25398  dvne0f1  25399  dvcnvrelem1  25404  dvcnvrelem2  25405  dvcnvre  25406  dvcvx  25407  dvfsumle  25408  dvfsumge  25409  dvfsumabs  25410  ftc1cn  25430  ftc2  25431  ftc2ditglem  25432  ftc2ditg  25433  itgparts  25434  itgsubstlem  25435  itgsubst  25436  ulmcn  25781  psercn  25808  pserdvlem2  25810  pserdv  25811  sincn  25826  coscn  25827  logtayl  26038  dvcncxp1  26119  leibpi  26315  lgamgulmlem2  26402  ftc2re  33275  fdvposlt  33276  fdvneggt  33277  fdvposle  33278  fdvnegge  33279  ivthALT  34860  knoppcld  35021  knoppndv  35050  ftc1cnnclem  36199  ftc1cnnc  36200  ftc2nc  36210  3factsumint  40532  intlewftc  40568  dvle2  40579  cnioobibld  41595  evthiccabs  43824  cncfmptss  43918  mulc1cncfg  43920  expcnfg  43922  mulcncff  44201  cncfshift  44205  subcncff  44211  cncfcompt  44214  addcncff  44215  cncficcgt0  44219  divcncff  44222  cncfiooicclem1  44224  cncfiooiccre  44226  cncfioobd  44228  dvsubcncf  44255  dvmulcncf  44256  dvdivcncf  44258  ioodvbdlimc1lem1  44262  cnbdibl  44293  itgsubsticclem  44306  itgsubsticc  44307  itgioocnicc  44308  iblcncfioo  44309  itgiccshift  44311  itgsbtaddcnst  44313  fourierdlem18  44456  fourierdlem32  44470  fourierdlem33  44471  fourierdlem39  44477  fourierdlem48  44485  fourierdlem49  44486  fourierdlem58  44495  fourierdlem59  44496  fourierdlem71  44508  fourierdlem73  44510  fourierdlem81  44518  fourierdlem84  44521  fourierdlem85  44522  fourierdlem88  44525  fourierdlem94  44531  fourierdlem97  44534  fourierdlem101  44538  fourierdlem103  44540  fourierdlem104  44541  fourierdlem111  44548  fourierdlem112  44549  fourierdlem113  44550  fouriercn  44563
  Copyright terms: Public domain W3C validator