![]() |
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 10738 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | |
2 | simpr 485 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) | |
3 | 1, 2 | addcomd 10695 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = (𝐵 + (𝐴 − 𝐵))) |
4 | pncan3 10747 | . . 3 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴) | |
5 | 4 | ancoms 459 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 − 𝐵)) = 𝐴) |
6 | 3, 5 | eqtrd 2833 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1525 ∈ wcel 2083 (class class class)co 7023 ℂcc 10388 + caddc 10393 − cmin 10723 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-po 5369 df-so 5370 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-er 8146 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-ltxr 10533 df-sub 10725 |
This theorem is referenced by: addsubass 10750 npncan 10761 nppcan 10762 nnpcan 10763 subcan2 10765 nnncan 10775 npcand 10855 nn1suc 11513 zlem1lt 11888 zltlem1 11889 peano5uzi 11925 nummac 11997 uzp1 12132 peano2uzr 12156 qbtwnre 12446 fz01en 12789 fzsuc2 12819 fseq1m1p1 12836 predfz 12886 fzoss2 12919 fzoaddel2 12947 fzosplitsnm1 12966 fldiv 13082 modfzo0difsn 13165 seqm1 13241 monoord2 13255 sermono 13256 seqf1olem1 13263 seqf1olem2 13264 seqz 13272 expm1t 13311 expubnd 13395 bcm1k 13529 bcn2 13533 hashfzo 13642 hashbclem 13662 hashf1 13667 seqcoll 13674 swrdfv2 13863 swrdspsleq 13867 swrdlsw 13869 addlenrevpfx 13892 cshwlen 14001 cshwidxmod 14005 cshwidxmodr 14006 cshwidxm 14010 swrd2lsw 14154 shftlem 14265 shftfval 14267 seqshft 14282 iserex 14851 serf0 14875 iseralt 14879 sumrblem 14905 fsumm1 14943 mptfzshft 14970 binomlem 15021 binom1dif 15025 isumsplit 15032 climcndslem1 15041 binomrisefac 15233 bpolycl 15243 bpolysum 15244 bpolydiflem 15245 bpoly2 15248 bpoly3 15249 fsumcube 15251 ruclem12 15431 dvdssub2 15488 4sqlem19 16132 vdwapun 16143 vdwapid1 16144 vdwlem5 16154 vdwlem8 16157 vdwnnlem2 16165 ramub1lem2 16196 1259lem4 16300 1259prm 16302 2503prm 16306 4001prm 16311 gsumccat 17821 sylow1lem1 18457 efgsres 18595 efgredleme 18600 gsummptshft 18780 icccvx 23241 reparphti 23288 ovolunlem1 23785 advlog 24922 cxpaddlelem 25017 ang180lem1 25072 ang180lem3 25074 asinlem2 25132 tanatan 25182 ppiub 25466 perfect1 25490 lgsquad2lem1 25646 rplogsumlem1 25746 selberg2lem 25812 logdivbnd 25818 pntrsumo1 25827 pntrsumbnd2 25829 ax5seglem3 26404 ax5seglem5 26406 axbtwnid 26412 axlowdimlem16 26430 axeuclidlem 26435 axcontlem2 26438 crctcshwlkn0lem6 27279 clwwlknonex2lem2 27573 clwwlknonex2 27574 eucrctshift 27708 cvmliftlem7 32148 nndivsub 33416 ltflcei 34432 itg2addnclem3 34497 mettrifi 34585 irrapxlem1 38925 rmspecsqrtnq 39009 jm2.24nn 39062 jm2.18 39091 jm2.23 39099 jm2.27c 39110 ablsimpgfindlem1 40186 monoord2xrv 41323 itgsinexp 41803 2elfz2melfz 43056 sbgoldbwt 43446 sgoldbeven3prm 43452 evengpop3 43467 evengpoap3 43468 zlmodzxzsub 43908 |
Copyright terms: Public domain | W3C validator |