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

Theorem addcom 11348
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 11157 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ 1 โˆˆ โ„‚)
21, 1addcld 11181 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (1 + 1) โˆˆ โ„‚)
3 simpl 484 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ๐ด โˆˆ โ„‚)
4 simpr 486 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ๐ต โˆˆ โ„‚)
52, 3, 4adddid 11186 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((1 + 1) ยท (๐ด + ๐ต)) = (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)))
63, 4addcld 11181 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด + ๐ต) โˆˆ โ„‚)
7 1p1times 11333 . . . . . . 7 ((๐ด + ๐ต) โˆˆ โ„‚ โ†’ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
86, 7syl 17 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
9 1p1times 11333 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด))
10 1p1times 11333 . . . . . . 7 (๐ต โˆˆ โ„‚ โ†’ ((1 + 1) ยท ๐ต) = (๐ต + ๐ต))
119, 10oveqan12d 7381 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)) = ((๐ด + ๐ด) + (๐ต + ๐ต)))
125, 8, 113eqtr3rd 2786 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + ๐ด) + (๐ต + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
133, 3addcld 11181 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด + ๐ด) โˆˆ โ„‚)
1413, 4, 4addassd 11184 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (((๐ด + ๐ด) + ๐ต) + ๐ต) = ((๐ด + ๐ด) + (๐ต + ๐ต)))
156, 3, 4addassd 11184 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (((๐ด + ๐ต) + ๐ด) + ๐ต) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
1612, 14, 153eqtr4d 2787 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต))
1713, 4addcld 11181 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + ๐ด) + ๐ต) โˆˆ โ„‚)
186, 3addcld 11181 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + ๐ต) + ๐ด) โˆˆ โ„‚)
19 addcan2 11347 . . . . 5 ((((๐ด + ๐ด) + ๐ต) โˆˆ โ„‚ โˆง ((๐ด + ๐ต) + ๐ด) โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ†” ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)))
2017, 18, 4, 19syl3anc 1372 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ†” ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)))
2116, 20mpbid 231 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))
223, 3, 4addassd 11184 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + ๐ด) + ๐ต) = (๐ด + (๐ด + ๐ต)))
233, 4, 3addassd 11184 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + ๐ต) + ๐ด) = (๐ด + (๐ต + ๐ด)))
2421, 22, 233eqtr3d 2785 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)))
254, 3addcld 11181 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ต + ๐ด) โˆˆ โ„‚)
26 addcan 11346 . . 3 ((๐ด โˆˆ โ„‚ โˆง (๐ด + ๐ต) โˆˆ โ„‚ โˆง (๐ต + ๐ด) โˆˆ โ„‚) โ†’ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ†” (๐ด + ๐ต) = (๐ต + ๐ด)))
273, 6, 25, 26syl3anc 1372 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ†” (๐ด + ๐ต) = (๐ต + ๐ด)))
2824, 27mpbid 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