![]() |
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 11209 | . . . . . . . 8 โข ((๐ด โ โ โง ๐ต โ โ) โ 1 โ โ) | |
2 | 1, 1 | addcld 11233 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ (1 + 1) โ โ) |
3 | simpl 484 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ โ) | |
4 | simpr 486 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ โ) | |
5 | 2, 3, 4 | adddid 11238 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 + 1) ยท (๐ด + ๐ต)) = (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต))) |
6 | 3, 4 | addcld 11233 | . . . . . . 7 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
7 | 1p1times 11385 | . . . . . . 7 โข ((๐ด + ๐ต) โ โ โ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) | |
8 | 6, 7 | syl 17 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
9 | 1p1times 11385 | . . . . . . 7 โข (๐ด โ โ โ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด)) | |
10 | 1p1times 11385 | . . . . . . 7 โข (๐ต โ โ โ ((1 + 1) ยท ๐ต) = (๐ต + ๐ต)) | |
11 | 9, 10 | oveqan12d 7428 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)) = ((๐ด + ๐ด) + (๐ต + ๐ต))) |
12 | 5, 8, 11 | 3eqtr3rd 2782 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + (๐ต + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
13 | 3, 3 | addcld 11233 | . . . . . 6 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ด) โ โ) |
14 | 13, 4, 4 | addassd 11236 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ด) + ๐ต) + ๐ต) = ((๐ด + ๐ด) + (๐ต + ๐ต))) |
15 | 6, 3, 4 | addassd 11236 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + ๐ด) + ๐ต) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
16 | 12, 14, 15 | 3eqtr4d 2783 | . . . 4 โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต)) |
17 | 13, 4 | addcld 11233 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + ๐ต) โ โ) |
18 | 6, 3 | addcld 11233 | . . . . 5 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + ๐ด) โ โ) |
19 | addcan2 11399 | . . . . 5 โข ((((๐ด + ๐ด) + ๐ต) โ โ โง ((๐ด + ๐ต) + ๐ด) โ โ โง ๐ต โ โ) โ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))) | |
20 | 17, 18, 4, 19 | syl3anc 1372 | . . . 4 โข ((๐ด โ โ โง ๐ต โ โ) โ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))) |
21 | 16, 20 | mpbid 231 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)) |
22 | 3, 3, 4 | addassd 11236 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ด) + ๐ต) = (๐ด + (๐ด + ๐ต))) |
23 | 3, 4, 3 | addassd 11236 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + ๐ด) = (๐ด + (๐ต + ๐ด))) |
24 | 21, 22, 23 | 3eqtr3d 2781 | . 2 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด))) |
25 | 4, 3 | addcld 11233 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ต + ๐ด) โ โ) |
26 | addcan 11398 | . . 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 7409 โcc 11108 1c1 11111 + caddc 11113 ยท cmul 11115 |
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 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-ltxr 11253 |
This theorem is referenced by: addcomi 11405 ltaddnegr 11430 add12 11431 add32 11432 add42 11435 subsub23 11465 pncan2 11467 addsub 11471 addsub12 11473 addsubeq4 11475 sub32 11494 pnpcan2 11500 ppncan 11502 sub4 11505 negsubdi2 11519 ltaddsub2 11689 leaddsub2 11691 leltadd 11698 ltaddpos2 11705 addge02 11725 conjmul 11931 recp1lt1 12112 recreclt 12113 avgle1 12452 avgle2 12453 avgle 12454 nn0nnaddcl 12503 xaddcom 13219 fzen 13518 fzshftral 13589 fzo0addelr 13687 elfzoext 13689 flzadd 13791 addmodidr 13885 modadd2mod 13886 nn0ennn 13944 seradd 14010 bernneq2 14193 ccatrn 14539 ccatalpha 14543 revccat 14716 2cshwcom 14766 shftval2 15022 shftval4 15024 crim 15062 absmax 15276 climshft2 15526 summolem3 15660 binom1dif 15779 isumshft 15785 arisum 15806 mertenslem1 15830 bpolydiflem 15998 addcos 16117 demoivreALT 16144 dvdsaddr 16246 sumodd 16331 divalglem4 16339 divalgb 16347 gcdaddm 16466 hashdvds 16708 phiprmpw 16709 pythagtriplem2 16750 prmgaplem7 16990 mulgnndir 18983 cnaddablx 19736 cnaddabl 19737 zaddablx 19740 cncrng 20966 ioo2bl 24309 icopnfcnv 24458 uniioombllem3 25102 fta1glem1 25683 plyremlem 25817 fta1lem 25820 vieta1lem1 25823 vieta1lem2 25824 aaliou3lem2 25856 dvradcnv 25933 pserdv2 25942 reeff1olem 25958 ptolemy 26006 logcnlem4 26153 cxpsqrt 26211 atandm2 26382 atandm4 26384 atanlogsublem 26420 2efiatan 26423 dvatan 26440 birthdaylem2 26457 emcllem2 26501 fsumharmonic 26516 wilthlem1 26572 wilthlem2 26573 basellem8 26592 1sgmprm 26702 perfectlem2 26733 pntibndlem1 27092 pntibndlem2 27094 pntlemd 27097 pntlemc 27098 eucrctshift 29496 cnaddabloOLD 29834 cdj3lem3b 31693 isarchi3 32333 archiabllem2c 32341 cos2h 36479 tan2h 36480 lcmineqlem4 40897 2xp3dxp2ge1d 41022 eldioph2lem1 41498 addcomgi 43215 fz0addcom 46025 epoo 46371 perfectALTVlem2 46390 sbgoldbaltlem2 46448 |
Copyright terms: Public domain | W3C validator |