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 23426 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | |
2 | cncfrss2 23427 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | |
3 | elcncf 23424 | . . . 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 2105 ∀wral 3135 ∃wrex 3136 ⊆ wss 3933 class class class wbr 5057 ⟶wf 6344 ‘cfv 6348 (class class class)co 7145 ℂcc 10523 < clt 10663 − cmin 10858 ℝ+crp 12377 abscabs 14581 –cn→ccncf 23411 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 ax-cnex 10581 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-fv 6356 df-ov 7148 df-oprab 7149 df-mpo 7150 df-map 8397 df-cncf 23413 |
This theorem is referenced by: cncfss 23434 climcncf 23435 cncfco 23442 cncfmpt1f 23448 cncfmpt2ss 23450 negfcncf 23454 divcncf 23975 ivth2 23983 ivthicc 23986 evthicc2 23988 cniccbdd 23989 volivth 24135 cncombf 24186 cnmbf 24187 cniccibl 24368 cnmptlimc 24415 cpnord 24459 cpnres 24461 dvrec 24479 rollelem 24513 rolle 24514 cmvth 24515 mvth 24516 dvlip 24517 c1liplem1 24520 c1lip1 24521 c1lip2 24522 dveq0 24524 dvgt0lem1 24526 dvgt0lem2 24527 dvgt0 24528 dvlt0 24529 dvge0 24530 dvle 24531 dvivthlem1 24532 dvivth 24534 dvne0 24535 dvne0f1 24536 dvcnvrelem1 24541 dvcnvrelem2 24542 dvcnvre 24543 dvcvx 24544 dvfsumle 24545 dvfsumge 24546 dvfsumabs 24547 ftc1cn 24567 ftc2 24568 ftc2ditglem 24569 ftc2ditg 24570 itgparts 24571 itgsubstlem 24572 itgsubst 24573 ulmcn 24914 psercn 24941 pserdvlem2 24943 pserdv 24944 sincn 24959 coscn 24960 logtayl 25170 dvcncxp1 25251 leibpi 25447 lgamgulmlem2 25534 ftc2re 31768 fdvposlt 31769 fdvneggt 31770 fdvposle 31771 fdvnegge 31772 ivthALT 33580 knoppcld 33741 knoppndv 33770 cnicciblnc 34844 ftc1cnnclem 34846 ftc1cnnc 34847 ftc2nc 34857 cnioobibld 39698 evthiccabs 41647 cncfmptss 41744 mulc1cncfg 41746 expcnfg 41748 mulcncff 42027 cncfshift 42033 subcncff 42039 cncfcompt 42042 addcncff 42043 cncficcgt0 42047 divcncff 42050 cncfiooicclem1 42052 cncfiooiccre 42054 cncfioobd 42056 cncfcompt2 42058 dvsubcncf 42085 dvmulcncf 42086 dvdivcncf 42088 ioodvbdlimc1lem1 42092 cnbdibl 42123 itgsubsticclem 42136 itgsubsticc 42137 itgioocnicc 42138 iblcncfioo 42139 itgiccshift 42141 itgsbtaddcnst 42143 fourierdlem18 42287 fourierdlem32 42301 fourierdlem33 42302 fourierdlem39 42308 fourierdlem48 42316 fourierdlem49 42317 fourierdlem58 42326 fourierdlem59 42327 fourierdlem71 42339 fourierdlem73 42341 fourierdlem81 42349 fourierdlem84 42352 fourierdlem85 42353 fourierdlem88 42356 fourierdlem94 42362 fourierdlem97 42365 fourierdlem101 42369 fourierdlem103 42371 fourierdlem104 42372 fourierdlem111 42379 fourierdlem112 42380 fourierdlem113 42381 fouriercn 42394 |
Copyright terms: Public domain | W3C validator |