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

Theorem addcom 9547
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 ax-1cn 9332 . . . . . . . . 9  |-  1  e.  CC
21a1i 11 . . . . . . . 8  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  1  e.  CC )
32, 2addcld 9397 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( 1  +  1 )  e.  CC )
4 simpl 454 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  A  e.  CC )
5 simpr 458 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
63, 4, 5adddid 9402 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) ) )
74, 5addcld 9397 . . . . . . 7  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
8 1p1times 9532 . . . . . . 7  |-  ( ( A  +  B )  e.  CC  ->  (
( 1  +  1 )  x.  ( A  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B
) ) )
97, 8syl 16 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
10 1p1times 9532 . . . . . . 7  |-  ( A  e.  CC  ->  (
( 1  +  1 )  x.  A )  =  ( A  +  A ) )
11 1p1times 9532 . . . . . . 7  |-  ( B  e.  CC  ->  (
( 1  +  1 )  x.  B )  =  ( B  +  B ) )
1210, 11oveqan12d 6103 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) )  =  ( ( A  +  A )  +  ( B  +  B ) ) )
136, 9, 123eqtr3rd 2478 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  ( B  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B ) ) )
144, 4addcld 9397 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  A
)  e.  CC )
1514, 5, 5addassd 9400 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( A  +  A )  +  ( B  +  B ) ) )
167, 4, 5addassd 9400 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  B )  +  A )  +  B
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
1713, 15, 163eqtr4d 2479 . . . 4  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( ( A  +  B
)  +  A )  +  B ) )
1814, 5addcld 9397 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  B
)  e.  CC )
197, 4addcld 9397 . . . . 5  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  +  A
)  e.  CC )
20 addcan2 9546 . . . . 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 ) ) )
2118, 19, 5, 20syl3anc 1213 . . . 4  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( ( A  +  A )  +  B )  +  B )  =  ( ( ( A  +  B )  +  A
)  +  B )  <-> 
( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) ) )
2217, 21mpbid 210 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) )
234, 4, 5addassd 9400 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  A )  +  B
)  =  ( A  +  ( A  +  B ) ) )
244, 5, 4addassd 9400 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  +  A
)  =  ( A  +  ( B  +  A ) ) )
2522, 23, 243eqtr3d 2477 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) ) )
265, 4addcld 9397 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  A
)  e.  CC )
27 addcan 9545 . . 3  |-  ( ( A  e.  CC  /\  ( A  +  B
)  e.  CC  /\  ( B  +  A
)  e.  CC )  ->  ( ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) )  <->  ( A  +  B )  =  ( B  +  A ) ) )
284, 7, 26, 27syl3anc 1213 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  ( A  +  B
) )  =  ( A  +  ( B  +  A ) )  <-> 
( A  +  B
)  =  ( B  +  A ) ) )
2925, 28mpbid 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 369    = wceq 1364    e. wcel 1757  (class class class)co 6084   CCcc 9272   1c1 9275    + caddc 9277    x. cmul 9279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-op 3876  df-uni 4084  df-br 4285  df-opab 4343  df-mpt 4344  df-id 4627  df-po 4632  df-so 4633  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-ov 6087  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415
This theorem is referenced by:  addcomi  9552  add12  9574  add32  9575  add42  9578  subsub23  9607  pncan2  9609  addsub  9613  addsub12  9615  addsubeq4  9617  sub32  9635  pnpcan2  9641  ppncan  9643  sub4  9646  negsubdi2  9660  ltaddsub2  9806  leaddsub2  9808  leltadd  9815  ltaddpos2  9822  addge02  9842  conjmul  10040  recp1lt1  10222  recreclt  10223  avgle1  10556  avgle2  10557  avgle  10558  nn0nnaddcl  10603  xaddcom  11200  fzen  11458  fzshftral  11535  flzadd  11659  modadd2mod  11737  nn0ennn  11789  seradd  11836  bernneq2  11979  hashfz  12176  revccat  12394  2cshwcom  12438  shftval2  12552  shftval4  12554  crim  12592  absmax  12805  climshft2  13048  summolem3  13179  binom1dif  13283  isumshft  13289  arisum  13309  mertenslem1  13331  addcos  13445  demoivreALT  13472  dvdsaddr  13559  divalglem4  13587  divalgb  13595  gcdaddm  13700  hashdvds  13837  phiprmpw  13838  pythagtriplem2  13871  mulgnndir  15633  cnaddablx  16332  cnaddabl  16333  zaddablx  16334  cncrng  17685  ioo2bl  20216  icopnfcnv  20360  uniioombllem3  20911  fta1glem1  21526  plyremlem  21659  fta1lem  21662  vieta1lem1  21665  vieta1lem2  21666  aaliou3lem2  21698  dvradcnv  21775  pserdv2  21784  reeff1olem  21800  ptolemy  21847  logcnlem4  21979  cxpsqr  22037  atandm2  22161  atandm4  22163  atanlogsublem  22199  2efiatan  22202  dvatan  22219  birthdaylem2  22235  emcllem2  22279  fsumharmonic  22294  wilthlem1  22295  wilthlem2  22296  basellem8  22314  1sgmprm  22427  perfectlem2  22458  pntibndlem1  22727  pntibndlem2  22729  pntlemd  22732  pntlemc  22733  cnaddablo  23664  addinv  23666  cdj3lem3b  25671  isarchi3  26032  archiabllem1a  26036  archiabllem2c  26040  bpolydiflem  28048  cos2h  28271  tan2h  28272  eldioph2lem1  28947  addcomgi  29561  fz0addcom  30050
  Copyright terms: Public domain W3C validator