![]() |
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 479 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) | |
2 | simpl 476 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ) | |
3 | 1, 2 | addcomd 10564 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵)) |
4 | addcl 10341 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
5 | subadd 10611 | . . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵))) | |
6 | 4, 1, 2, 5 | syl3anc 1494 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵))) |
7 | 3, 6 | mpbird 249 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1656 ∈ wcel 2164 (class class class)co 6910 ℂcc 10257 + caddc 10262 − cmin 10592 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5007 ax-nul 5015 ax-pow 5067 ax-pr 5129 ax-un 7214 ax-resscn 10316 ax-1cn 10317 ax-icn 10318 ax-addcl 10319 ax-addrcl 10320 ax-mulcl 10321 ax-mulrcl 10322 ax-mulcom 10323 ax-addass 10324 ax-mulass 10325 ax-distr 10326 ax-i2m1 10327 ax-1ne0 10328 ax-1rid 10329 ax-rnegex 10330 ax-rrecex 10331 ax-cnre 10332 ax-pre-lttri 10333 ax-pre-lttrn 10334 ax-pre-ltadd 10335 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-pw 4382 df-sn 4400 df-pr 4402 df-op 4406 df-uni 4661 df-br 4876 df-opab 4938 df-mpt 4955 df-id 5252 df-po 5265 df-so 5266 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-rn 5357 df-res 5358 df-ima 5359 df-iota 6090 df-fun 6129 df-fn 6130 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 df-fv 6135 df-riota 6871 df-ov 6913 df-oprab 6914 df-mpt2 6915 df-er 8014 df-en 8229 df-dom 8230 df-sdom 8231 df-pnf 10400 df-mnf 10401 df-ltxr 10403 df-sub 10594 |
This theorem is referenced by: pncan2 10615 addsubass 10619 pncan3oi 10625 subid1 10629 nppcan2 10640 pncand 10721 nn1m1nn 11379 nnsub 11402 elnn0nn 11669 elz2 11728 zrevaddcl 11757 nzadd 11760 qrevaddcl 12100 irradd 12102 fzrev3 12707 elfzp1b 12718 fzrevral3 12728 fzval3 12839 seqf1olem1 13141 seqf1olem2 13142 subsq2 13274 bcp1nk 13404 bcp1m1 13407 bcpasc 13408 hashbclem 13532 ccatalpha 13660 wrdind 13819 wrdindOLD 13820 wrd2ind 13821 wrd2indOLD 13822 2cshwcshw 13953 shftlem 14192 shftval5 14202 isershft 14778 isercoll2 14783 fsump1 14869 mptfzshft 14891 telfsumo 14915 fsumparts 14919 bcxmas 14948 isum1p 14954 geolim 14982 mertenslem2 14997 mertens 14998 fsumkthpow 15166 eftlub 15218 effsumlt 15220 eirrlem 15313 dvdsadd 15408 prmind2 15777 iserodd 15918 fldivp1 15979 prmpwdvds 15986 pockthlem 15987 prmreclem4 16001 prmreclem6 16003 4sqlem11 16037 vdwapun 16056 ramub1lem1 16108 ramcl 16111 efgsval2 18504 efgsrel 18505 pcoass 23200 shft2rab 23681 uniioombllem3 23758 uniioombllem4 23759 dvexp 24122 dvfsumlem1 24195 degltp1le 24239 ply1divex 24302 plyaddlem1 24375 plymullem1 24376 dvply1 24445 dvply2g 24446 vieta1lem2 24472 aaliou3lem7 24510 dvradcnv 24581 pserdvlem2 24588 abssinper 24677 advlogexp 24807 atantayl3 25086 leibpilem1 25087 leibpilem2 25088 emcllem2 25143 harmonicbnd4 25157 wilthlem2 25215 basellem8 25234 ppiprm 25297 ppinprm 25298 chtprm 25299 chtnprm 25300 chpp1 25301 chtub 25357 perfectlem1 25374 perfectlem2 25375 perfect 25376 bcp1ctr 25424 lgsvalmod 25461 lgseisen 25524 lgsquadlem1 25525 lgsquad2lem1 25529 2sqlem10 25573 rplogsumlem1 25593 selberg2lem 25659 logdivbnd 25665 pntrsumo1 25674 pntpbnd2 25696 wwlksnext 27211 clwwlkf1OLD 27395 clwwlkf1 27400 subfacp1lem5 31708 subfacp1lem6 31709 subfacval2 31711 subfaclim 31712 cvmliftlem7 31815 cvmliftlem10 31818 mblfinlem2 33990 itg2addnclem3 34005 fdc 34082 mettrifi 34094 heiborlem4 34154 heiborlem6 34156 lzenom 38176 2nn0ind 38352 jm2.17a 38369 jm2.17b 38370 jm2.17c 38371 evensumeven 42464 perfectALTVlem2 42479 perfectALTV 42480 |
Copyright terms: Public domain | W3C validator |