![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addcom | Structured version Visualization version GIF version |
Description: Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
addcom | โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) = (๐ต + ๐ด)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1cnd 11157 | . . . . . . . 8 โข ((๐ด โ โ โง ๐ต โ โ) โ 1 โ โ) | |
2 | 1, 1 | addcld 11181 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ (1 + 1) โ โ) |
3 | simpl 484 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ โ) | |
4 | simpr 486 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ โ) | |
5 | 2, 3, 4 | adddid 11186 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 + 1) ยท (๐ด + ๐ต)) = (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต))) |
6 | 3, 4 | addcld 11181 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
7 | 1p1times 11333 | . . . . . . 7 โข ((๐ด + ๐ต) โ โ โ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) | |
8 | 6, 7 | syl 17 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
9 | 1p1times 11333 | . . . . . . 7 โข (๐ด โ โ โ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด)) | |
10 | 1p1times 11333 | . . . . . . 7 โข (๐ต โ โ โ ((1 + 1) ยท ๐ต) = (๐ต + ๐ต)) | |
11 | 9, 10 | oveqan12d 7381 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)) = ((๐ด + ๐ด) + (๐ต + ๐ต))) |
12 | 5, 8, 11 | 3eqtr3rd 2786 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + (๐ต + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
13 | 3, 3 | addcld 11181 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ด) โ โ) |
14 | 13, 4, 4 | addassd 11184 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ด) + ๐ต) + ๐ต) = ((๐ด + ๐ด) + (๐ต + ๐ต))) |
15 | 6, 3, 4 | addassd 11184 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + ๐ด) + ๐ต) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
16 | 12, 14, 15 | 3eqtr4d 2787 | . . . 4 โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต)) |
17 | 13, 4 | addcld 11181 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + ๐ต) โ โ) |
18 | 6, 3 | addcld 11181 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + ๐ด) โ โ) |
19 | addcan2 11347 | . . . . 5 โข ((((๐ด + ๐ด) + ๐ต) โ โ โง ((๐ด + ๐ต) + ๐ด) โ โ โง ๐ต โ โ) โ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))) | |
20 | 17, 18, 4, 19 | syl3anc 1372 | . . . 4 โข ((๐ด โ โ โง ๐ต โ โ) โ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))) |
21 | 16, 20 | mpbid 231 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)) |
22 | 3, 3, 4 | addassd 11184 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + ๐ต) = (๐ด + (๐ด + ๐ต))) |
23 | 3, 4, 3 | addassd 11184 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + ๐ด) = (๐ด + (๐ต + ๐ด))) |
24 | 21, 22, 23 | 3eqtr3d 2785 | . 2 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด))) |
25 | 4, 3 | addcld 11181 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ต + ๐ด) โ โ) |
26 | addcan 11346 | . . 3 โข ((๐ด โ โ โง (๐ด + ๐ต) โ โ โง (๐ต + ๐ด) โ โ) โ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ (๐ด + ๐ต) = (๐ต + ๐ด))) | |
27 | 3, 6, 25, 26 | syl3anc 1372 | . 2 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ (๐ด + ๐ต) = (๐ต + ๐ด))) |
28 | 24, 27 | mpbid 231 | 1 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) = (๐ต + ๐ด)) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โ wb 205 โง wa 397 = wceq 1542 โ wcel 2107 (class class class)co 7362 โcc 11056 1c1 11059 + caddc 11061 ยท cmul 11063 |
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-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-ov 7365 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11198 df-mnf 11199 df-ltxr 11201 |
This theorem is referenced by: addcomi 11353 ltaddnegr 11378 add12 11379 add32 11380 add42 11383 subsub23 11413 pncan2 11415 addsub 11419 addsub12 11421 addsubeq4 11423 sub32 11442 pnpcan2 11448 ppncan 11450 sub4 11453 negsubdi2 11467 ltaddsub2 11637 leaddsub2 11639 leltadd 11646 ltaddpos2 11653 addge02 11673 conjmul 11879 recp1lt1 12060 recreclt 12061 avgle1 12400 avgle2 12401 avgle 12402 nn0nnaddcl 12451 xaddcom 13166 fzen 13465 fzshftral 13536 fzo0addelr 13634 elfzoext 13636 flzadd 13738 addmodidr 13832 modadd2mod 13833 nn0ennn 13891 seradd 13957 bernneq2 14140 ccatrn 14484 ccatalpha 14488 revccat 14661 2cshwcom 14711 shftval2 14967 shftval4 14969 crim 15007 absmax 15221 climshft2 15471 summolem3 15606 binom1dif 15725 isumshft 15731 arisum 15752 mertenslem1 15776 bpolydiflem 15944 addcos 16063 demoivreALT 16090 dvdsaddr 16192 sumodd 16277 divalglem4 16285 divalgb 16293 gcdaddm 16412 hashdvds 16654 phiprmpw 16655 pythagtriplem2 16696 prmgaplem7 16936 mulgnndir 18912 cnaddablx 19653 cnaddabl 19654 zaddablx 19657 cncrng 20834 ioo2bl 24172 icopnfcnv 24321 uniioombllem3 24965 fta1glem1 25546 plyremlem 25680 fta1lem 25683 vieta1lem1 25686 vieta1lem2 25687 aaliou3lem2 25719 dvradcnv 25796 pserdv2 25805 reeff1olem 25821 ptolemy 25869 logcnlem4 26016 cxpsqrt 26074 atandm2 26243 atandm4 26245 atanlogsublem 26281 2efiatan 26284 dvatan 26301 birthdaylem2 26318 emcllem2 26362 fsumharmonic 26377 wilthlem1 26433 wilthlem2 26434 basellem8 26453 1sgmprm 26563 perfectlem2 26594 pntibndlem1 26953 pntibndlem2 26955 pntlemd 26958 pntlemc 26959 eucrctshift 29229 cnaddabloOLD 29565 cdj3lem3b 31424 isarchi3 32065 archiabllem2c 32073 cos2h 36098 tan2h 36099 lcmineqlem4 40518 2xp3dxp2ge1d 40643 eldioph2lem1 41112 addcomgi 42810 fz0addcom 45623 epoo 45969 perfectALTVlem2 45988 sbgoldbaltlem2 46046 |
Copyright terms: Public domain | W3C validator |