Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > subcn | Structured version Visualization version GIF version |
Description: Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
Ref | Expression |
---|---|
addcn.j | ⊢ 𝐽 = (TopOpen‘ℂfld) |
Ref | Expression |
---|---|
subcn | ⊢ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcn.j | . 2 ⊢ 𝐽 = (TopOpen‘ℂfld) | |
2 | subf 11110 | . 2 ⊢ − :(ℂ × ℂ)⟶ℂ | |
3 | subcn2 15189 | . 2 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝑏 − 𝑐))) < 𝑎)) | |
4 | 1, 2, 3 | addcnlem 23793 | 1 ⊢ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2112 ‘cfv 6401 (class class class)co 7235 − cmin 11092 TopOpenctopn 16959 ℂfldccnfld 20396 Cn ccn 22153 ×t ctx 22489 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5196 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-cnex 10815 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 ax-pre-sup 10837 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-se 5528 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-isom 6410 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-of 7491 df-om 7667 df-1st 7783 df-2nd 7784 df-supp 7928 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-1o 8226 df-2o 8227 df-er 8415 df-map 8534 df-ixp 8603 df-en 8651 df-dom 8652 df-sdom 8653 df-fin 8654 df-fsupp 9016 df-fi 9057 df-sup 9088 df-inf 9089 df-oi 9156 df-card 9585 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-div 11520 df-nn 11861 df-2 11923 df-3 11924 df-4 11925 df-5 11926 df-6 11927 df-7 11928 df-8 11929 df-9 11930 df-n0 12121 df-z 12207 df-dec 12324 df-uz 12469 df-q 12575 df-rp 12617 df-xneg 12734 df-xadd 12735 df-xmul 12736 df-icc 12972 df-fz 13126 df-fzo 13269 df-seq 13607 df-exp 13668 df-hash 13930 df-cj 14695 df-re 14696 df-im 14697 df-sqrt 14831 df-abs 14832 df-struct 16733 df-sets 16750 df-slot 16768 df-ndx 16778 df-base 16794 df-ress 16818 df-plusg 16848 df-mulr 16849 df-starv 16850 df-sca 16851 df-vsca 16852 df-ip 16853 df-tset 16854 df-ple 16855 df-ds 16857 df-unif 16858 df-hom 16859 df-cco 16860 df-rest 16960 df-topn 16961 df-0g 16979 df-gsum 16980 df-topgen 16981 df-pt 16982 df-prds 16985 df-xrs 17040 df-qtop 17045 df-imas 17046 df-xps 17048 df-mre 17122 df-mrc 17123 df-acs 17125 df-mgm 18147 df-sgrp 18196 df-mnd 18207 df-submnd 18252 df-mulg 18522 df-cntz 18744 df-cmn 19205 df-psmet 20388 df-xmet 20389 df-met 20390 df-bl 20391 df-mopn 20392 df-cnfld 20397 df-top 21823 df-topon 21840 df-topsp 21862 df-bases 21875 df-cn 22156 df-cnp 22157 df-tx 22491 df-hmeo 22684 df-xms 23250 df-tms 23252 |
This theorem is referenced by: cnfldtgp 23798 sub1cncf 23848 sub2cncf 23849 iirevcn 23859 iihalf2cn 23863 icchmeo 23870 evth 23888 evth2 23889 subcncf 24374 dvcnp2 24849 cmvth 24920 dvlipcn 24923 dvle 24936 lhop1lem 24942 dvfsumge 24951 dvfsumabs 24952 ftc2 24973 taylthlem2 25298 sincn 25368 lgamgulmlem2 25944 pntlem3 26522 ipasslem7 28949 cvxpconn 32948 cvxsconn 32949 sinccvglem 33374 broucube 35585 ftc1cnnclem 35622 ftc2nc 35633 areacirclem2 35640 areaquad 40798 |
Copyright terms: Public domain | W3C validator |