![]() |
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 22741 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | |
2 | cncfrss2 22742 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | |
3 | elcncf 22739 | . . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) | |
4 | 1, 2, 3 | syl2anc 694 | . . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) |
5 | 4 | ibi 256 | . 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) |
6 | 5 | simpld 474 | 1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∈ wcel 2030 ∀wral 2941 ∃wrex 2942 ⊆ wss 3607 class class class wbr 4685 ⟶wf 5922 ‘cfv 5926 (class class class)co 6690 ℂcc 9972 < clt 10112 − cmin 10304 ℝ+crp 11870 abscabs 14018 –cn→ccncf 22726 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-cnex 10030 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-fv 5934 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-map 7901 df-cncf 22728 |
This theorem is referenced by: cncfss 22749 climcncf 22750 cncfco 22757 cncfmpt1f 22763 cncfmpt2ss 22765 negfcncf 22769 divcncf 23262 ivth2 23270 ivthicc 23273 evthicc2 23275 cniccbdd 23276 volivth 23421 cncombf 23470 cnmbf 23471 cniccibl 23652 cnmptlimc 23699 cpnord 23743 cpnres 23745 dvrec 23763 rollelem 23797 rolle 23798 cmvth 23799 mvth 23800 dvlip 23801 c1liplem1 23804 c1lip1 23805 c1lip2 23806 dveq0 23808 dvgt0lem1 23810 dvgt0lem2 23811 dvgt0 23812 dvlt0 23813 dvge0 23814 dvle 23815 dvivthlem1 23816 dvivth 23818 dvne0 23819 dvne0f1 23820 dvcnvrelem1 23825 dvcnvrelem2 23826 dvcnvre 23827 dvcvx 23828 dvfsumle 23829 dvfsumge 23830 dvfsumabs 23831 ftc1cn 23851 ftc2 23852 ftc2ditglem 23853 ftc2ditg 23854 itgparts 23855 itgsubstlem 23856 itgsubst 23857 ulmcn 24198 psercn 24225 pserdvlem2 24227 pserdv 24228 sincn 24243 coscn 24244 logtayl 24451 dvcncxp1 24529 leibpi 24714 lgamgulmlem2 24801 ftc2re 30804 fdvposlt 30805 fdvneggt 30806 fdvposle 30807 fdvnegge 30808 ivthALT 32455 knoppcld 32620 knoppndv 32650 cnicciblnc 33611 ftc1cnnclem 33613 ftc1cnnc 33614 ftc2nc 33624 cnioobibld 38116 evthiccabs 40036 cncfmptss 40137 mulc1cncfg 40139 expcnfg 40141 mulcncff 40399 cncfshift 40405 subcncff 40411 cncfcompt 40414 addcncff 40415 cncficcgt0 40419 divcncff 40422 cncfiooicclem1 40424 cncfiooiccre 40426 cncfioobd 40428 cncfcompt2 40430 dvsubcncf 40457 dvmulcncf 40458 dvdivcncf 40460 ioodvbdlimc1lem1 40464 cnbdibl 40496 itgsubsticclem 40509 itgsubsticc 40510 itgioocnicc 40511 iblcncfioo 40512 itgiccshift 40514 itgsbtaddcnst 40516 fourierdlem18 40660 fourierdlem32 40674 fourierdlem33 40675 fourierdlem39 40681 fourierdlem48 40689 fourierdlem49 40690 fourierdlem58 40699 fourierdlem59 40700 fourierdlem71 40712 fourierdlem73 40714 fourierdlem81 40722 fourierdlem84 40725 fourierdlem85 40726 fourierdlem88 40729 fourierdlem94 40735 fourierdlem97 40738 fourierdlem101 40742 fourierdlem103 40744 fourierdlem104 40745 fourierdlem111 40752 fourierdlem112 40753 fourierdlem113 40754 fouriercn 40767 |
Copyright terms: Public domain | W3C validator |