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 476 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) | |
2 | simpl 472 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ) | |
3 | 1, 2 | addcomd 10117 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) = (𝐴 + 𝐵)) |
4 | addcl 9897 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
5 | subadd 10163 | . . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵))) | |
6 | 4, 1, 2, 5 | syl3anc 1318 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) − 𝐵) = 𝐴 ↔ (𝐵 + 𝐴) = (𝐴 + 𝐵))) |
7 | 3, 6 | mpbird 246 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 (class class class)co 6549 ℂcc 9813 + caddc 9818 − cmin 10145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-po 4959 df-so 4960 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-ltxr 9958 df-sub 10147 |
This theorem is referenced by: pncan2 10167 addsubass 10170 pncan3oi 10176 subid1 10180 nppcan2 10191 pncand 10272 nn1m1nn 10917 nnsub 10936 elnn0nn 11212 elz2 11271 zrevaddcl 11299 nzadd 11302 qrevaddcl 11686 irradd 11688 fzrev3 12276 elfzp1b 12286 fzrevral3 12296 fzval3 12404 seqf1olem1 12702 seqf1olem2 12703 subsq2 12835 bcp1nk 12966 bcp1m1 12969 bcpasc 12970 hashbclem 13093 ccatalpha 13228 wrdind 13328 wrd2ind 13329 2cshwcshw 13422 shftlem 13656 shftval5 13666 isershft 14242 isercoll2 14247 fsump1 14329 mptfzshft 14352 telfsumo 14375 fsumparts 14379 bcxmas 14406 isum1p 14412 geolim 14440 mertenslem2 14456 mertens 14457 fsumkthpow 14626 eftlub 14678 effsumlt 14680 eirrlem 14771 dvdsadd 14862 prmind2 15236 iserodd 15378 fldivp1 15439 prmpwdvds 15446 pockthlem 15447 prmreclem4 15461 prmreclem6 15463 4sqlem11 15497 vdwapun 15516 ramub1lem1 15568 ramcl 15571 efgsval2 17969 efgsrel 17970 pcoass 22632 shft2rab 23083 uniioombllem3 23159 uniioombllem4 23160 dvexp 23522 dvfsumlem1 23593 degltp1le 23637 ply1divex 23700 plyaddlem1 23773 plymullem1 23774 dvply1 23843 dvply2g 23844 vieta1lem2 23870 aaliou3lem7 23908 dvradcnv 23979 pserdvlem2 23986 abssinper 24074 advlogexp 24201 atantayl3 24466 leibpilem1 24467 leibpilem2 24468 emcllem2 24523 harmonicbnd4 24537 wilthlem2 24595 basellem8 24614 ppiprm 24677 ppinprm 24678 chtprm 24679 chtnprm 24680 chpp1 24681 chtub 24737 perfectlem1 24754 perfectlem2 24755 perfect 24756 bcp1ctr 24804 lgsvalmod 24841 lgseisen 24904 lgsquadlem1 24905 lgsquad2lem1 24909 2sqlem10 24953 rplogsumlem1 24973 selberg2lem 25039 logdivbnd 25045 pntrsumo1 25054 pntpbnd2 25076 wlklenvm1 26060 wlkiswwlk1 26218 wwlknext 26252 clwwlkf1 26324 eupap1 26503 eupath2lem3 26506 extwwlkfablem2 26605 subfacp1lem5 30420 subfacp1lem6 30421 subfacval2 30423 subfaclim 30424 cvmliftlem7 30527 cvmliftlem10 30530 mblfinlem2 32617 itg2addnclem3 32633 fdc 32711 mettrifi 32723 heiborlem4 32783 heiborlem6 32785 lzenom 36351 2nn0ind 36528 jm2.17a 36545 jm2.17b 36546 jm2.17c 36547 evensumeven 40154 perfectALTVlem2 40165 perfectALTV 40166 wwlksnext 41099 clwwlksf1 41224 |
Copyright terms: Public domain | W3C validator |