![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > npcan | 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 |
---|---|
npcan | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subcl 11407 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | |
2 | simpr 486 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) | |
3 | 1, 2 | addcomd 11364 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵))) |
4 | pncan3 11416 | . . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴) | |
5 | 4 | ancoms 460 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴) |
6 | 3, 5 | eqtrd 2777 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 (class class class)co 7362 ℂcc 11056 + caddc 11061 − cmin 11392 |
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 2708 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-resscn 11115 ax-1cn 11116 ax-icn 11117 ax-addcl 11118 ax-addrcl 11119 ax-mulcl 11120 ax-mulrcl 11121 ax-mulcom 11122 ax-addass 11123 ax-mulass 11124 ax-distr 11125 ax-i2m1 11126 ax-1ne0 11127 ax-1rid 11128 ax-rnegex 11129 ax-rrecex 11130 ax-cnre 11131 ax-pre-lttri 11132 ax-pre-lttrn 11133 ax-pre-ltadd 11134 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3066 df-rex 3075 df-reu 3357 df-rab 3411 df-v 3450 df-sbc 3745 df-csb 3861 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-po 5550 df-so 5551 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11198 df-mnf 11199 df-ltxr 11201 df-sub 11394 |
This theorem is referenced by: addsubass 11418 npncan 11429 nppcan 11430 nnpcan 11431 subcan2 11433 nnncan 11443 npcand 11523 nn1suc 12182 zlem1lt 12562 zltlem1 12563 peano5uzi 12599 nummac 12670 uzp1 12811 peano2uzr 12835 qbtwnre 13125 fz01en 13476 fzsuc2 13506 fseq1m1p1 13523 predfz 13573 fzoss2 13607 fzoaddel2 13635 fzosplitsnm1 13654 fldiv 13772 modfzo0difsn 13855 seqm1 13932 monoord2 13946 sermono 13947 seqf1olem1 13954 seqf1olem2 13955 seqz 13963 expm1t 14003 expubnd 14089 bcm1k 14222 bcn2 14226 hashfzo 14336 hashbclem 14356 hashf1 14363 seqcoll 14370 swrdfv2 14556 swrdspsleq 14560 swrdlsw 14562 addlenrevpfx 14585 ccatpfx 14596 cshwlen 14694 cshwidxmodr 14699 cshwidxm 14703 swrd2lsw 14848 shftlem 14960 shftfval 14962 seqshft 14977 iserex 15548 serf0 15572 iseralt 15576 sumrblem 15603 fsumm1 15643 mptfzshft 15670 binomlem 15721 binom1dif 15725 isumsplit 15732 climcndslem1 15741 binomrisefac 15932 bpolycl 15942 bpolysum 15943 bpolydiflem 15944 bpoly2 15947 bpoly3 15948 fsumcube 15950 ruclem12 16130 dvdssub2 16190 4sqlem19 16842 vdwapun 16853 vdwapid1 16854 vdwlem5 16864 vdwlem8 16867 vdwnnlem2 16875 ramub1lem2 16906 1259lem4 17013 1259prm 17015 2503prm 17019 4001prm 17024 gsumsgrpccat 18657 sylow1lem1 19387 efgsres 19527 efgredleme 19532 gsummptshft 19720 ablsimpgfindlem1 19893 icccvx 24329 reparphti 24376 ovolunlem1 24877 advlog 26025 cxpaddlelem 26120 ang180lem1 26175 ang180lem3 26177 asinlem2 26235 tanatan 26285 ppiub 26568 perfect1 26592 lgsquad2lem1 26748 rplogsumlem1 26848 selberg2lem 26914 logdivbnd 26920 pntrsumo1 26929 pntrsumbnd2 26931 ax5seglem3 27922 ax5seglem5 27924 axbtwnid 27930 axlowdimlem16 27948 axeuclidlem 27953 axcontlem2 27956 crctcshwlkn0lem6 28802 clwwlknonex2lem2 29094 clwwlknonex2 29095 eucrctshift 29229 cvmliftlem7 33925 nndivsub 34958 ltflcei 36095 itg2addnclem3 36160 mettrifi 36245 irrapxlem1 41174 rmspecsqrtnq 41258 jm2.24nn 41312 jm2.18 41341 jm2.23 41349 jm2.27c 41360 monoord2xrv 43793 itgsinexp 44270 2elfz2melfz 45624 sbgoldbwt 46043 sgoldbeven3prm 46049 evengpop3 46064 evengpoap3 46065 zlmodzxzsub 46510 ackval42 46856 |
Copyright terms: Public domain | W3C validator |