![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pncan | Structured version Visualization version GIF version |
Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
pncan | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 488 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) | |
2 | simpl 486 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ) | |
3 | 1, 2 | addcomd 10831 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵)) |
4 | addcl 10608 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
5 | subadd 10878 | . . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵))) | |
6 | 4, 1, 2, 5 | syl3anc 1368 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵))) |
7 | 3, 6 | mpbird 260 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 (class class class)co 7135 ℂcc 10524 + caddc 10529 − cmin 10859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-ltxr 10669 df-sub 10861 |
This theorem is referenced by: pncan2 10882 addsubass 10885 pncan3oi 10891 subid1 10895 nppcan2 10906 pncand 10987 nn1m1nn 11646 nnsub 11669 elnn0nn 11927 elz2 11987 zrevaddcl 12015 nzadd 12018 qrevaddcl 12358 irradd 12360 fzrev3 12968 elfzp1b 12979 fzrevral3 12989 fzval3 13101 seqf1olem1 13405 seqf1olem2 13406 bcp1nk 13673 bcp1m1 13676 bcpasc 13677 hashbclem 13806 ccatalpha 13938 wrdind 14075 wrd2ind 14076 2cshwcshw 14178 shftlem 14419 shftval5 14429 isershft 15012 isercoll2 15017 fsump1 15103 mptfzshft 15125 telfsumo 15149 fsumparts 15153 bcxmas 15182 isum1p 15188 geolim 15218 mertenslem2 15233 mertens 15234 fsumkthpow 15402 eftlub 15454 effsumlt 15456 eirrlem 15549 dvdsadd 15644 prmind2 16019 iserodd 16162 fldivp1 16223 prmpwdvds 16230 pockthlem 16231 prmreclem4 16245 prmreclem6 16247 4sqlem11 16281 vdwapun 16300 ramub1lem1 16352 ramcl 16355 efgsval2 18851 efgsrel 18852 shft2rab 24112 uniioombllem3 24189 uniioombllem4 24190 dvexp 24556 dvfsumlem1 24629 degltp1le 24674 ply1divex 24737 plyaddlem1 24810 plymullem1 24811 dvply1 24880 dvply2g 24881 vieta1lem2 24907 aaliou3lem7 24945 dvradcnv 25016 pserdvlem2 25023 abssinper 25113 advlogexp 25246 atantayl3 25525 leibpilem2 25527 emcllem2 25582 harmonicbnd4 25596 basellem8 25673 ppiprm 25736 ppinprm 25737 chtprm 25738 chtnprm 25739 chpp1 25740 chtub 25796 perfectlem1 25813 perfectlem2 25814 perfect 25815 bcp1ctr 25863 lgsvalmod 25900 lgseisen 25963 lgsquadlem1 25964 lgsquad2lem1 25968 2sqlem10 26012 rplogsumlem1 26068 selberg2lem 26134 logdivbnd 26140 pntrsumo1 26149 pntpbnd2 26171 clwwlkf1 27834 subfacp1lem5 32544 subfacp1lem6 32545 subfacval2 32547 subfaclim 32548 cvmliftlem7 32651 cvmliftlem10 32654 mblfinlem2 35095 itg2addnclem3 35110 fdc 35183 mettrifi 35195 heiborlem4 35252 heiborlem6 35254 lzenom 39711 2nn0ind 39886 jm2.17a 39901 jm2.17b 39902 jm2.17c 39903 evensumeven 44225 perfectALTVlem2 44240 perfectALTV 44241 |
Copyright terms: Public domain | W3C validator |