MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcom Structured version   Visualization version   GIF version

Theorem addcom 10166
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.)
Assertion
Ref Expression
addcom ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcom
StepHypRef Expression
1 1cnd 10000 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
21, 1addcld 10003 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 + 1) ∈ ℂ)
3 simpl 473 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
4 simpr 477 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
52, 3, 4adddid 10008 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 10003 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 10151 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 10151 . . . . . . 7 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10 1p1times 10151 . . . . . . 7 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
119, 10oveqan12d 6623 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
125, 8, 113eqtr3rd 2664 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
133, 3addcld 10003 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐴) ∈ ℂ)
1413, 4, 4addassd 10006 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
156, 3, 4addassd 10006 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1612, 14, 153eqtr4d 2665 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1713, 4addcld 10003 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
186, 3addcld 10003 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
19 addcan2 10165 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2017, 18, 4, 19syl3anc 1323 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2116, 20mpbid 222 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
223, 3, 4addassd 10006 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
233, 4, 3addassd 10006 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2421, 22, 233eqtr3d 2663 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
254, 3addcld 10003 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) ∈ ℂ)
26 addcan 10164 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
273, 6, 25, 26syl3anc 1323 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
2824, 27mpbid 222 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  (class class class)co 6604  cc 9878  1c1 9881   + caddc 9883   · cmul 9885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-po 4995  df-so 4996  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-pnf 10020  df-mnf 10021  df-ltxr 10023
This theorem is referenced by:  addcomi  10171  ltaddnegr  10196  add12  10197  add32  10198  add42  10201  subsub23  10230  pncan2  10232  addsub  10236  addsub12  10238  addsubeq4  10240  sub32  10259  pnpcan2  10265  ppncan  10267  sub4  10270  negsubdi2  10284  ltaddsub2  10447  leaddsub2  10449  leltadd  10456  ltaddpos2  10463  addge02  10483  conjmul  10686  recp1lt1  10865  recreclt  10866  avgle1  11216  avgle2  11217  avgle  11218  nn0nnaddcl  11268  xaddcom  12014  fzen  12300  fzshftral  12369  fzo0addelr  12463  elfzoext  12465  flzadd  12567  addmodidr  12659  modadd2mod  12660  nn0ennn  12718  seradd  12783  bernneq2  12931  hashfz  13154  ccatalpha  13314  revccat  13452  2cshwcom  13499  shftval2  13749  shftval4  13751  crim  13789  absmax  14003  climshft2  14247  summolem3  14378  binom1dif  14490  isumshft  14496  arisum  14517  mertenslem1  14541  bpolydiflem  14710  addcos  14829  demoivreALT  14856  dvdsaddr  14949  sumodd  15035  divalglem4  15043  divalgb  15051  gcdaddm  15170  hashdvds  15404  phiprmpw  15405  pythagtriplem2  15446  prmgaplem7  15685  mulgnndir  17490  mulgnndirOLD  17491  cnaddablx  18192  cnaddabl  18193  zaddablx  18196  cncrng  19686  ioo2bl  22504  icopnfcnv  22649  uniioombllem3  23259  fta1glem1  23829  plyremlem  23963  fta1lem  23966  vieta1lem1  23969  vieta1lem2  23970  aaliou3lem2  24002  dvradcnv  24079  pserdv2  24088  reeff1olem  24104  ptolemy  24152  logcnlem4  24291  cxpsqrt  24349  atandm2  24504  atandm4  24506  atanlogsublem  24542  2efiatan  24545  dvatan  24562  birthdaylem2  24579  emcllem2  24623  fsumharmonic  24638  wilthlem1  24694  wilthlem2  24695  basellem8  24714  1sgmprm  24824  perfectlem2  24855  pntibndlem1  25178  pntibndlem2  25180  pntlemd  25183  pntlemc  25184  eucrctshift  26969  cnaddabloOLD  27282  cdj3lem3b  29145  isarchi3  29523  archiabllem2c  29531  cos2h  33029  tan2h  33030  eldioph2lem1  36800  addcomgi  38139  fz0addcom  40621  epoo  40908  perfectALTVlem2  40923  sgoldbaltlem2  40960
  Copyright terms: Public domain W3C validator