Theorem cncff 24786

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 24784	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24785	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24782	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 584	. . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
5	4	ibi 267	. 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
6	5	simpld 494	1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   ⊆ wss 3914   class class class wbr 5107  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  ℂcc 11066   < clt 11208   − cmin 11405  ℝ⁺crp 12951  abscabs 15200  –cn→ccncf 24769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-map 8801  df-cncf 24771

This theorem is referenced by:  cncfss  24792  climcncf  24793  cncfco  24800  cncfcompt2  24801  cncfmpt1f  24807  cncfmpt2ss  24809  negfcncf  24817  divcncf  25348  ivth2  25356  ivthicc  25359  evthicc2  25361  cniccbdd  25362  volivth  25508  cncombf  25559  cnmbf  25560  cniccibl  25742  cnicciblnc  25744  cnmptlimc  25791  cpnord  25837  cpnres  25839  dvrec  25859  rollelem  25893  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  c1liplem1  25901  c1lip1  25902  c1lip2  25903  dveq0  25905  dvgt0lem1  25907  dvgt0lem2  25908  dvgt0  25909  dvlt0  25910  dvge0  25911  dvle  25912  dvivthlem1  25913  dvivth  25915  dvne0  25916  dvne0f1  25917  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  ftc1cn  25950  ftc2  25951  ftc2ditglem  25952  ftc2ditg  25953  itgparts  25954  itgsubstlem  25955  itgsubst  25956  ulmcn  26308  psercn  26336  pserdvlem2  26338  pserdv  26339  sincn  26354  coscn  26355  logtayl  26569  dvcncxp1  26652  leibpi  26852  lgamgulmlem2  26940  ftc2re  34589  fdvposlt  34590  fdvneggt  34591  fdvposle  34592  fdvnegge  34593  ivthALT  36323  knoppcld  36493  knoppndv  36522  ftc1cnnclem  37685  ftc1cnnc  37686  ftc2nc  37696  3factsumint  42013  intlewftc  42049  dvle2  42060  cnioobibld  43203  evthiccabs  45494  cncfmptss  45585  mulc1cncfg  45587  expcnfg  45589  mulcncff  45868  cncfshift  45872  subcncff  45878  cncfcompt  45881  addcncff  45882  cncficcgt0  45886  divcncff  45889  cncfiooicclem1  45891  cncfiooiccre  45893  cncfioobd  45895  dvsubcncf  45922  dvmulcncf  45923  dvdivcncf  45925  ioodvbdlimc1lem1  45929  cnbdibl  45960  itgsubsticclem  45973  itgsubsticc  45974  itgioocnicc  45975  iblcncfioo  45976  itgiccshift  45978  itgsbtaddcnst  45980  fourierdlem18  46123  fourierdlem32  46137  fourierdlem33  46138  fourierdlem39  46144  fourierdlem48  46152  fourierdlem49  46153  fourierdlem58  46162  fourierdlem59  46163  fourierdlem71  46175  fourierdlem73  46177  fourierdlem81  46185  fourierdlem84  46188  fourierdlem85  46189  fourierdlem88  46192  fourierdlem94  46198  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fouriercn  46230