![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cncff | Structured version Visualization version GIF version |
Description: A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
Ref | Expression |
---|---|
cncff | ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cncfrss 23187 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | |
2 | cncfrss2 23188 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | |
3 | elcncf 23185 | . . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) | |
4 | 1, 2, 3 | syl2anc 584 | . . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) |
5 | 4 | ibi 268 | . 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) |
6 | 5 | simpld 495 | 1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2081 ∀wral 3105 ∃wrex 3106 ⊆ wss 3863 class class class wbr 4966 ⟶wf 6226 ‘cfv 6230 (class class class)co 7021 ℂcc 10386 < clt 10526 − cmin 10722 ℝ+crp 12244 abscabs 14432 –cn→ccncf 23172 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-cnex 10444 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3710 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-fv 6238 df-ov 7024 df-oprab 7025 df-mpo 7026 df-map 8263 df-cncf 23174 |
This theorem is referenced by: cncfss 23195 climcncf 23196 cncfco 23203 cncfmpt1f 23209 cncfmpt2ss 23211 negfcncf 23215 divcncf 23736 ivth2 23744 ivthicc 23747 evthicc2 23749 cniccbdd 23750 volivth 23896 cncombf 23947 cnmbf 23948 cniccibl 24129 cnmptlimc 24176 cpnord 24220 cpnres 24222 dvrec 24240 rollelem 24274 rolle 24275 cmvth 24276 mvth 24277 dvlip 24278 c1liplem1 24281 c1lip1 24282 c1lip2 24283 dveq0 24285 dvgt0lem1 24287 dvgt0lem2 24288 dvgt0 24289 dvlt0 24290 dvge0 24291 dvle 24292 dvivthlem1 24293 dvivth 24295 dvne0 24296 dvne0f1 24297 dvcnvrelem1 24302 dvcnvrelem2 24303 dvcnvre 24304 dvcvx 24305 dvfsumle 24306 dvfsumge 24307 dvfsumabs 24308 ftc1cn 24328 ftc2 24329 ftc2ditglem 24330 ftc2ditg 24331 itgparts 24332 itgsubstlem 24333 itgsubst 24334 ulmcn 24675 psercn 24702 pserdvlem2 24704 pserdv 24705 sincn 24720 coscn 24721 logtayl 24929 dvcncxp1 25010 leibpi 25207 lgamgulmlem2 25294 ftc2re 31491 fdvposlt 31492 fdvneggt 31493 fdvposle 31494 fdvnegge 31495 ivthALT 33298 knoppcld 33459 knoppndv 33488 cnicciblnc 34519 ftc1cnnclem 34521 ftc1cnnc 34522 ftc2nc 34532 cnioobibld 39330 evthiccabs 41338 cncfmptss 41435 mulc1cncfg 41437 expcnfg 41439 mulcncff 41718 cncfshift 41724 subcncff 41730 cncfcompt 41733 addcncff 41734 cncficcgt0 41738 divcncff 41741 cncfiooicclem1 41743 cncfiooiccre 41745 cncfioobd 41747 cncfcompt2 41749 dvsubcncf 41776 dvmulcncf 41777 dvdivcncf 41779 ioodvbdlimc1lem1 41783 cnbdibl 41814 itgsubsticclem 41827 itgsubsticc 41828 itgioocnicc 41829 iblcncfioo 41830 itgiccshift 41832 itgsbtaddcnst 41834 fourierdlem18 41978 fourierdlem32 41992 fourierdlem33 41993 fourierdlem39 41999 fourierdlem48 42007 fourierdlem49 42008 fourierdlem58 42017 fourierdlem59 42018 fourierdlem71 42030 fourierdlem73 42032 fourierdlem81 42040 fourierdlem84 42043 fourierdlem85 42044 fourierdlem88 42047 fourierdlem94 42053 fourierdlem97 42056 fourierdlem101 42060 fourierdlem103 42062 fourierdlem104 42063 fourierdlem111 42070 fourierdlem112 42071 fourierdlem113 42072 fouriercn 42085 |
Copyright terms: Public domain | W3C validator |