Theorem cncff 24723

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.

Step	Hyp	Ref	Expression
1		cncfrss 24721	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24722	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24719	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 583	. . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
5	4	ibi 267	. 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
6	5	simpld 494	1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062   ⊆ wss 3940   class class class wbr 5138  ⟶wf 6529  ‘cfv 6533  (class class class)co 7401  ℂcc 11103   < clt 11244   − cmin 11440  ℝ⁺crp 12970  abscabs 15177  –cn→ccncf 24706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-map 8817  df-cncf 24708

This theorem is referenced by:  cncfss  24729  climcncf  24730  cncfco  24737  cncfcompt2  24738  cncfmpt1f  24744  cncfmpt2ss  24746  negfcncf  24754  divcncf  25286  ivth2  25294  ivthicc  25297  evthicc2  25299  cniccbdd  25300  volivth  25446  cncombf  25497  cnmbf  25498  cniccibl  25680  cnicciblnc  25682  cnmptlimc  25729  cpnord  25775  cpnres  25777  dvrec  25797  rollelem  25831  rolle  25832  cmvth  25833  cmvthOLD  25834  mvth  25835  dvlip  25836  c1liplem1  25839  c1lip1  25840  c1lip2  25841  dveq0  25843  dvgt0lem1  25845  dvgt0lem2  25846  dvgt0  25847  dvlt0  25848  dvge0  25849  dvle  25850  dvivthlem1  25851  dvivth  25853  dvne0  25854  dvne0f1  25855  dvcnvrelem1  25860  dvcnvrelem2  25861  dvcnvre  25862  dvcvx  25863  dvfsumle  25864  dvfsumleOLD  25865  dvfsumge  25866  dvfsumabs  25867  ftc1cn  25888  ftc2  25889  ftc2ditglem  25890  ftc2ditg  25891  itgparts  25892  itgsubstlem  25893  itgsubst  25894  ulmcn  26240  psercn  26268  pserdvlem2  26270  pserdv  26271  sincn  26286  coscn  26287  logtayl  26498  dvcncxp1  26581  leibpi  26778  lgamgulmlem2  26866  ftc2re  34065  fdvposlt  34066  fdvneggt  34067  fdvposle  34068  fdvnegge  34069  ivthALT  35676  knoppcld  35837  knoppndv  35866  ftc1cnnclem  37015  ftc1cnnc  37016  ftc2nc  37026  3factsumint  41349  intlewftc  41385  dvle2  41396  cnioobibld  42418  evthiccabs  44660  cncfmptss  44754  mulc1cncfg  44756  expcnfg  44758  mulcncff  45037  cncfshift  45041  subcncff  45047  cncfcompt  45050  addcncff  45051  cncficcgt0  45055  divcncff  45058  cncfiooicclem1  45060  cncfiooiccre  45062  cncfioobd  45064  dvsubcncf  45091  dvmulcncf  45092  dvdivcncf  45094  ioodvbdlimc1lem1  45098  cnbdibl  45129  itgsubsticclem  45142  itgsubsticc  45143  itgioocnicc  45144  iblcncfioo  45145  itgiccshift  45147  itgsbtaddcnst  45149  fourierdlem18  45292  fourierdlem32  45306  fourierdlem33  45307  fourierdlem39  45313  fourierdlem48  45321  fourierdlem49  45322  fourierdlem58  45331  fourierdlem59  45332  fourierdlem71  45344  fourierdlem73  45346  fourierdlem81  45354  fourierdlem84  45357  fourierdlem85  45358  fourierdlem88  45361  fourierdlem94  45367  fourierdlem97  45370  fourierdlem101  45374  fourierdlem103  45376  fourierdlem104  45377  fourierdlem111  45384  fourierdlem112  45385  fourierdlem113  45386  fouriercn  45399