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

Theorem addcom 9677
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  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )

Proof of Theorem addcom
StepHypRef Expression
1 1cnd 9523 . . . . . . . 8  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  1  e.  CC )
21, 1addcld 9526 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( 1  +  1 )  e.  CC )
3 simpl 455 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  A  e.  CC )
4 simpr 459 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
52, 3, 4adddid 9531 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) ) )
63, 4addcld 9526 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
7 1p1times 9662 . . . . . . 7  |-  ( ( A  +  B )  e.  CC  ->  (
( 1  +  1 )  x.  ( A  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B
) ) )
86, 7syl 16 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
9 1p1times 9662 . . . . . . 7  |-  ( A  e.  CC  ->  (
( 1  +  1 )  x.  A )  =  ( A  +  A ) )
10 1p1times 9662 . . . . . . 7  |-  ( B  e.  CC  ->  (
( 1  +  1 )  x.  B )  =  ( B  +  B ) )
119, 10oveqan12d 6215 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) )  =  ( ( A  +  A )  +  ( B  +  B ) ) )
125, 8, 113eqtr3rd 2432 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  ( B  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B ) ) )
133, 3addcld 9526 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  A
)  e.  CC )
1413, 4, 4addassd 9529 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( A  +  A )  +  ( B  +  B ) ) )
156, 3, 4addassd 9529 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  B )  +  A )  +  B
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
1612, 14, 153eqtr4d 2433 . . . 4  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( ( A  +  B
)  +  A )  +  B ) )
1713, 4addcld 9526 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  B
)  e.  CC )
186, 3addcld 9526 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  +  A
)  e.  CC )
19 addcan2 9676 . . . . 5  |-  ( ( ( ( A  +  A )  +  B
)  e.  CC  /\  ( ( A  +  B )  +  A
)  e.  CC  /\  B  e.  CC )  ->  ( ( ( ( A  +  A )  +  B )  +  B )  =  ( ( ( A  +  B )  +  A
)  +  B )  <-> 
( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) ) )
2017, 18, 4, 19syl3anc 1226 . . . 4  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( ( A  +  A )  +  B )  +  B )  =  ( ( ( A  +  B )  +  A
)  +  B )  <-> 
( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) ) )
2116, 20mpbid 210 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) )
223, 3, 4addassd 9529 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  B
)  =  ( A  +  ( A  +  B ) ) )
233, 4, 3addassd 9529 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  +  A
)  =  ( A  +  ( B  +  A ) ) )
2421, 22, 233eqtr3d 2431 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) ) )
254, 3addcld 9526 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  A
)  e.  CC )
26 addcan 9675 . . 3  |-  ( ( A  e.  CC  /\  ( A  +  B
)  e.  CC  /\  ( B  +  A
)  e.  CC )  ->  ( ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) )  <->  ( A  +  B )  =  ( B  +  A ) ) )
273, 6, 25, 26syl3anc 1226 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  ( A  +  B
) )  =  ( A  +  ( B  +  A ) )  <-> 
( A  +  B
)  =  ( B  +  A ) ) )
2824, 27mpbid 210 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826  (class class class)co 6196   CCcc 9401   1c1 9404    + caddc 9406    x. cmul 9408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-po 4714  df-so 4715  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-ltxr 9544
This theorem is referenced by:  addcomi  9682  add12  9704  add32  9705  add42  9708  subsub23  9738  pncan2  9740  addsub  9744  addsub12  9746  addsubeq4  9748  sub32  9766  pnpcan2  9772  ppncan  9774  sub4  9777  negsubdi2  9791  ltaddsub2  9945  leaddsub2  9947  leltadd  9954  ltaddpos2  9961  addge02  9981  conjmul  10178  recp1lt1  10359  recreclt  10360  avgle1  10695  avgle2  10696  avgle  10697  nn0nnaddcl  10744  xaddcom  11358  fzen  11624  fzshftral  11688  fzo0addelr  11770  elfzoext  11772  flzadd  11859  modadd2mod  11940  nn0ennn  11992  seradd  12052  bernneq2  12195  hashfz  12389  revccat  12651  2cshwcom  12695  shftval2  12910  shftval4  12912  crim  12950  absmax  13164  climshft2  13407  summolem3  13538  binom1dif  13647  isumshft  13653  arisum  13673  mertenslem1  13695  addcos  13911  demoivreALT  13938  dvdsaddr  14027  divalglem4  14056  divalgb  14064  gcdaddm  14169  hashdvds  14307  phiprmpw  14308  pythagtriplem2  14343  mulgnndir  16281  cnaddablx  16991  cnaddabl  16992  zaddablx  16993  cncrng  18552  ioo2bl  21383  icopnfcnv  21527  uniioombllem3  22079  fta1glem1  22651  plyremlem  22785  fta1lem  22788  vieta1lem1  22791  vieta1lem2  22792  aaliou3lem2  22824  dvradcnv  22901  pserdv2  22910  reeff1olem  22926  ptolemy  22974  logcnlem4  23113  cxpsqrt  23171  atandm2  23324  atandm4  23326  atanlogsublem  23362  2efiatan  23365  dvatan  23382  birthdaylem2  23399  emcllem2  23443  fsumharmonic  23458  wilthlem1  23459  wilthlem2  23460  basellem8  23478  1sgmprm  23591  perfectlem2  23622  pntibndlem1  23891  pntibndlem2  23893  pntlemd  23896  pntlemc  23897  cnaddablo  25469  addinv  25471  cdj3lem3b  27475  isarchi3  27884  archiabllem2c  27892  bpolydiflem  29969  cos2h  30211  tan2h  30212  eldioph2lem1  30858  addcomgi  31533  perfectALTVlem2  32544  fz0addcom  32654
  Copyright terms: Public domain W3C validator