![]() |
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 24277 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | |
2 | cncfrss2 24278 | . . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | |
3 | elcncf 24275 | . . . 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 3061 ∃wrex 3070 ⊆ wss 3914 class class class wbr 5109 ⟶wf 6496 ‘cfv 6500 (class class class)co 7361 ℂcc 11057 < clt 11197 − cmin 11393 ℝ+crp 12923 abscabs 15128 –cn→ccncf 24262 |
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 5260 ax-nul 5267 ax-pow 5324 ax-pr 5388 ax-un 7676 ax-cnex 11115 |
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 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-sbc 3744 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-pw 4566 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-id 5535 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-iota 6452 df-fun 6502 df-fn 6503 df-f 6504 df-fv 6508 df-ov 7364 df-oprab 7365 df-mpo 7366 df-map 8773 df-cncf 24264 |
This theorem is referenced by: cncfss 24285 climcncf 24286 cncfco 24293 cncfcompt2 24294 cncfmpt1f 24300 cncfmpt2ss 24302 negfcncf 24309 divcncf 24834 ivth2 24842 ivthicc 24845 evthicc2 24847 cniccbdd 24848 volivth 24994 cncombf 25045 cnmbf 25046 cniccibl 25228 cnicciblnc 25230 cnmptlimc 25277 cpnord 25322 cpnres 25324 dvrec 25342 rollelem 25376 rolle 25377 cmvth 25378 mvth 25379 dvlip 25380 c1liplem1 25383 c1lip1 25384 c1lip2 25385 dveq0 25387 dvgt0lem1 25389 dvgt0lem2 25390 dvgt0 25391 dvlt0 25392 dvge0 25393 dvle 25394 dvivthlem1 25395 dvivth 25397 dvne0 25398 dvne0f1 25399 dvcnvrelem1 25404 dvcnvrelem2 25405 dvcnvre 25406 dvcvx 25407 dvfsumle 25408 dvfsumge 25409 dvfsumabs 25410 ftc1cn 25430 ftc2 25431 ftc2ditglem 25432 ftc2ditg 25433 itgparts 25434 itgsubstlem 25435 itgsubst 25436 ulmcn 25781 psercn 25808 pserdvlem2 25810 pserdv 25811 sincn 25826 coscn 25827 logtayl 26038 dvcncxp1 26119 leibpi 26315 lgamgulmlem2 26402 ftc2re 33275 fdvposlt 33276 fdvneggt 33277 fdvposle 33278 fdvnegge 33279 ivthALT 34860 knoppcld 35021 knoppndv 35050 ftc1cnnclem 36199 ftc1cnnc 36200 ftc2nc 36210 3factsumint 40532 intlewftc 40568 dvle2 40579 cnioobibld 41595 evthiccabs 43824 cncfmptss 43918 mulc1cncfg 43920 expcnfg 43922 mulcncff 44201 cncfshift 44205 subcncff 44211 cncfcompt 44214 addcncff 44215 cncficcgt0 44219 divcncff 44222 cncfiooicclem1 44224 cncfiooiccre 44226 cncfioobd 44228 dvsubcncf 44255 dvmulcncf 44256 dvdivcncf 44258 ioodvbdlimc1lem1 44262 cnbdibl 44293 itgsubsticclem 44306 itgsubsticc 44307 itgioocnicc 44308 iblcncfioo 44309 itgiccshift 44311 itgsbtaddcnst 44313 fourierdlem18 44456 fourierdlem32 44470 fourierdlem33 44471 fourierdlem39 44477 fourierdlem48 44485 fourierdlem49 44486 fourierdlem58 44495 fourierdlem59 44496 fourierdlem71 44508 fourierdlem73 44510 fourierdlem81 44518 fourierdlem84 44521 fourierdlem85 44522 fourierdlem88 44525 fourierdlem94 44531 fourierdlem97 44534 fourierdlem101 44538 fourierdlem103 44540 fourierdlem104 44541 fourierdlem111 44548 fourierdlem112 44549 fourierdlem113 44550 fouriercn 44563 |
Copyright terms: Public domain | W3C validator |