![]() |
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 10625 | . . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ) | |
2 | 1, 1 | addcld 10649 | . . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 + 1) ∈ ℂ) |
3 | simpl 486 | . . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ) | |
4 | simpr 488 | . . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) | |
5 | 2, 3, 4 | adddid 10654 | . . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵))) |
6 | 3, 4 | addcld 10649 | . . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
7 | 1p1times 10800 | . . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) | |
8 | 6, 7 | syl 17 | . . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
9 | 1p1times 10800 | . . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴)) | |
10 | 1p1times 10800 | . . . . . . 7 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵)) | |
11 | 9, 10 | oveqan12d 7154 | . . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵))) |
12 | 5, 8, 11 | 3eqtr3rd 2842 | . . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
13 | 3, 3 | addcld 10649 | . . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐴) ∈ ℂ) |
14 | 13, 4, 4 | addassd 10652 | . . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵))) |
15 | 6, 3, 4 | addassd 10652 | . . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
16 | 12, 14, 15 | 3eqtr4d 2843 | . . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵)) |
17 | 13, 4 | addcld 10649 | . . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ) |
18 | 6, 3 | addcld 10649 | . . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ) |
19 | addcan2 10814 | . . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))) | |
20 | 17, 18, 4, 19 | syl3anc 1368 | . . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))) |
21 | 16, 20 | mpbid 235 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)) |
22 | 3, 3, 4 | addassd 10652 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵))) |
23 | 3, 4, 3 | addassd 10652 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴))) |
24 | 21, 22, 23 | 3eqtr3d 2841 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴))) |
25 | 4, 3 | addcld 10649 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) ∈ ℂ) |
26 | addcan 10813 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) | |
27 | 3, 6, 25, 26 | syl3anc 1368 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
28 | 24, 27 | mpbid 235 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 (class class class)co 7135 ℂcc 10524 1c1 10527 + caddc 10529 · cmul 10531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-ov 7138 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-ltxr 10669 |
This theorem is referenced by: addcomi 10820 ltaddnegr 10845 add12 10846 add32 10847 add42 10850 subsub23 10880 pncan2 10882 addsub 10886 addsub12 10888 addsubeq4 10890 sub32 10909 pnpcan2 10915 ppncan 10917 sub4 10920 negsubdi2 10934 ltaddsub2 11104 leaddsub2 11106 leltadd 11113 ltaddpos2 11120 addge02 11140 conjmul 11346 recp1lt1 11527 recreclt 11528 avgle1 11865 avgle2 11866 avgle 11867 nn0nnaddcl 11916 xaddcom 12621 fzen 12919 fzshftral 12990 fzo0addelr 13087 elfzoext 13089 flzadd 13191 addmodidr 13283 modadd2mod 13284 nn0ennn 13342 seradd 13408 bernneq2 13587 ccatrn 13934 ccatalpha 13938 revccat 14119 2cshwcom 14169 shftval2 14426 shftval4 14428 crim 14466 absmax 14681 climshft2 14931 summolem3 15063 binom1dif 15180 isumshft 15186 arisum 15207 mertenslem1 15232 bpolydiflem 15400 addcos 15519 demoivreALT 15546 dvdsaddr 15645 sumodd 15729 divalglem4 15737 divalgb 15745 gcdaddm 15863 hashdvds 16102 phiprmpw 16103 pythagtriplem2 16144 prmgaplem7 16383 mulgnndir 18248 cnaddablx 18981 cnaddabl 18982 zaddablx 18985 cncrng 20112 ioo2bl 23398 icopnfcnv 23547 uniioombllem3 24189 fta1glem1 24766 plyremlem 24900 fta1lem 24903 vieta1lem1 24906 vieta1lem2 24907 aaliou3lem2 24939 dvradcnv 25016 pserdv2 25025 reeff1olem 25041 ptolemy 25089 logcnlem4 25236 cxpsqrt 25294 atandm2 25463 atandm4 25465 atanlogsublem 25501 2efiatan 25504 dvatan 25521 birthdaylem2 25538 emcllem2 25582 fsumharmonic 25597 wilthlem1 25653 wilthlem2 25654 basellem8 25673 1sgmprm 25783 perfectlem2 25814 pntibndlem1 26173 pntibndlem2 26175 pntlemd 26178 pntlemc 26179 eucrctshift 28028 cnaddabloOLD 28364 cdj3lem3b 30223 isarchi3 30866 archiabllem2c 30874 cos2h 35048 tan2h 35049 lcmineqlem4 39320 2xp3dxp2ge1d 39387 eldioph2lem1 39701 addcomgi 41160 fz0addcom 43874 epoo 44221 perfectALTVlem2 44240 sbgoldbaltlem2 44298 |
Copyright terms: Public domain | W3C validator |