![]() |
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 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→𝐵) → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |