![]() |
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 24407 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | |
2 | cncfrss2 24408 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | |
3 | elcncf 24405 | . . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) | |
4 | 1, 2, 3 | syl2anc 585 | . . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) |
5 | 4 | ibi 267 | . 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) |
6 | 5 | simpld 496 | 1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 ⊆ wss 3949 class class class wbr 5149 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ℂcc 11108 < clt 11248 − cmin 11444 ℝ+crp 12974 abscabs 15181 –cn→ccncf 24392 |
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 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 |
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 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-map 8822 df-cncf 24394 |
This theorem is referenced by: cncfss 24415 climcncf 24416 cncfco 24423 cncfcompt2 24424 cncfmpt1f 24430 cncfmpt2ss 24432 negfcncf 24439 divcncf 24964 ivth2 24972 ivthicc 24975 evthicc2 24977 cniccbdd 24978 volivth 25124 cncombf 25175 cnmbf 25176 cniccibl 25358 cnicciblnc 25360 cnmptlimc 25407 cpnord 25452 cpnres 25454 dvrec 25472 rollelem 25506 rolle 25507 cmvth 25508 mvth 25509 dvlip 25510 c1liplem1 25513 c1lip1 25514 c1lip2 25515 dveq0 25517 dvgt0lem1 25519 dvgt0lem2 25520 dvgt0 25521 dvlt0 25522 dvge0 25523 dvle 25524 dvivthlem1 25525 dvivth 25527 dvne0 25528 dvne0f1 25529 dvcnvrelem1 25534 dvcnvrelem2 25535 dvcnvre 25536 dvcvx 25537 dvfsumle 25538 dvfsumge 25539 dvfsumabs 25540 ftc1cn 25560 ftc2 25561 ftc2ditglem 25562 ftc2ditg 25563 itgparts 25564 itgsubstlem 25565 itgsubst 25566 ulmcn 25911 psercn 25938 pserdvlem2 25940 pserdv 25941 sincn 25956 coscn 25957 logtayl 26168 dvcncxp1 26251 leibpi 26447 lgamgulmlem2 26534 ftc2re 33610 fdvposlt 33611 fdvneggt 33612 fdvposle 33613 fdvnegge 33614 gg-cmvth 35181 gg-dvfsumle 35182 ivthALT 35220 knoppcld 35381 knoppndv 35410 ftc1cnnclem 36559 ftc1cnnc 36560 ftc2nc 36570 3factsumint 40890 intlewftc 40926 dvle2 40937 cnioobibld 41963 evthiccabs 44209 cncfmptss 44303 mulc1cncfg 44305 expcnfg 44307 mulcncff 44586 cncfshift 44590 subcncff 44596 cncfcompt 44599 addcncff 44600 cncficcgt0 44604 divcncff 44607 cncfiooicclem1 44609 cncfiooiccre 44611 cncfioobd 44613 dvsubcncf 44640 dvmulcncf 44641 dvdivcncf 44643 ioodvbdlimc1lem1 44647 cnbdibl 44678 itgsubsticclem 44691 itgsubsticc 44692 itgioocnicc 44693 iblcncfioo 44694 itgiccshift 44696 itgsbtaddcnst 44698 fourierdlem18 44841 fourierdlem32 44855 fourierdlem33 44856 fourierdlem39 44862 fourierdlem48 44870 fourierdlem49 44871 fourierdlem58 44880 fourierdlem59 44881 fourierdlem71 44893 fourierdlem73 44895 fourierdlem81 44903 fourierdlem84 44906 fourierdlem85 44907 fourierdlem88 44910 fourierdlem94 44916 fourierdlem97 44919 fourierdlem101 44923 fourierdlem103 44925 fourierdlem104 44926 fourierdlem111 44933 fourierdlem112 44934 fourierdlem113 44935 fouriercn 44948 |
Copyright terms: Public domain | W3C validator |