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

Theorem addcomd 9269
Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
addcomd.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
addcomd  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )

Proof of Theorem addcomd
StepHypRef Expression
1 ax-1cn 9049 . . . . . . . . 9  |-  1  e.  CC
21a1i 11 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
32, 2addcld 9108 . . . . . . 7  |-  ( ph  ->  ( 1  +  1 )  e.  CC )
4 muld.1 . . . . . . 7  |-  ( ph  ->  A  e.  CC )
5 addcomd.2 . . . . . . 7  |-  ( ph  ->  B  e.  CC )
63, 4, 5adddid 9113 . . . . . 6  |-  ( ph  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) ) )
74, 5addcld 9108 . . . . . . 7  |-  ( ph  ->  ( A  +  B
)  e.  CC )
8 1p1times 9238 . . . . . . 7  |-  ( ( A  +  B )  e.  CC  ->  (
( 1  +  1 )  x.  ( A  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B
) ) )
97, 8syl 16 . . . . . 6  |-  ( ph  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
10 1p1times 9238 . . . . . . . 8  |-  ( A  e.  CC  ->  (
( 1  +  1 )  x.  A )  =  ( A  +  A ) )
114, 10syl 16 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  1 )  x.  A
)  =  ( A  +  A ) )
12 1p1times 9238 . . . . . . . 8  |-  ( B  e.  CC  ->  (
( 1  +  1 )  x.  B )  =  ( B  +  B ) )
135, 12syl 16 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  1 )  x.  B
)  =  ( B  +  B ) )
1411, 13oveq12d 6100 . . . . . 6  |-  ( ph  ->  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) )  =  ( ( A  +  A )  +  ( B  +  B ) ) )
156, 9, 143eqtr3rd 2478 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  ( B  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B ) ) )
164, 4addcld 9108 . . . . . 6  |-  ( ph  ->  ( A  +  A
)  e.  CC )
1716, 5, 5addassd 9111 . . . . 5  |-  ( ph  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( A  +  A )  +  ( B  +  B ) ) )
187, 4, 5addassd 9111 . . . . 5  |-  ( ph  ->  ( ( ( A  +  B )  +  A )  +  B
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
1915, 17, 183eqtr4d 2479 . . . 4  |-  ( ph  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( ( A  +  B
)  +  A )  +  B ) )
2016, 5addcld 9108 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  B
)  e.  CC )
217, 4addcld 9108 . . . . 5  |-  ( ph  ->  ( ( A  +  B )  +  A
)  e.  CC )
22 addcan2 9252 . . . . 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 ) ) )
2320, 21, 5, 22syl3anc 1185 . . . 4  |-  ( ph  ->  ( ( ( ( A  +  A )  +  B )  +  B )  =  ( ( ( A  +  B )  +  A
)  +  B )  <-> 
( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) ) )
2419, 23mpbid 203 . . 3  |-  ( ph  ->  ( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) )
254, 4, 5addassd 9111 . . 3  |-  ( ph  ->  ( ( A  +  A )  +  B
)  =  ( A  +  ( A  +  B ) ) )
264, 5, 4addassd 9111 . . 3  |-  ( ph  ->  ( ( A  +  B )  +  A
)  =  ( A  +  ( B  +  A ) ) )
2724, 25, 263eqtr3d 2477 . 2  |-  ( ph  ->  ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) ) )
285, 4addcld 9108 . . 3  |-  ( ph  ->  ( B  +  A
)  e.  CC )
29 addcan 9251 . . 3  |-  ( ( A  e.  CC  /\  ( A  +  B
)  e.  CC  /\  ( B  +  A
)  e.  CC )  ->  ( ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) )  <->  ( A  +  B )  =  ( B  +  A ) ) )
304, 7, 28, 29syl3anc 1185 . 2  |-  ( ph  ->  ( ( A  +  ( A  +  B
) )  =  ( A  +  ( B  +  A ) )  <-> 
( A  +  B
)  =  ( B  +  A ) ) )
3127, 30mpbid 203 1  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726  (class class class)co 6082   CCcc 8989   1c1 8992    + caddc 8994    x. cmul 8996
This theorem is referenced by:  subadd2  9310  pncan  9312  npcan  9315  subcan  9357  ltadd1  9496  leadd2  9498  ltsubadd2  9500  lesubadd2  9502  ltaddrp2d  10679  lincmb01cmp  11039  iccf1o  11040  modadd12d  11283  expaddz  11425  bcn2m1  11616  bcn2p1  11617  spllen  11784  splfv2a  11786  remullem  11934  sqreulem  12164  climaddc2  12430  clim2ser2  12450  iseraltlem2  12477  fsumtscopo  12582  fsumparts  12586  bcxmas  12616  cosneg  12749  coshval  12757  sinadd  12766  sincossq  12778  cos2t  12780  absefi  12798  absefib  12800  sadadd2lem2  12963  bitsres  12986  bezoutlem2  13040  bezoutlem4  13042  pythagtrip  13209  pcadd2  13260  vdwapun  13343  vdwlem5  13354  vdwlem6  13355  vdwlem8  13357  gsumccat  14788  mulgnndir  14913  mulgdirlem  14915  mulgdir  14916  sylow1lem1  15233  efgcpbllemb  15388  cygabl  15501  ablfacrp  15625  icccvx  18976  pjthlem1  19339  ovolicc2lem4  19417  cmmbl  19430  voliunlem1  19445  itgmulc2  19726  dvle  19892  dvcvx  19905  dvfsumlem2  19912  dvfsumlem4  19914  dvfsum2  19919  ply1divex  20060  plymullem1  20134  coeeulem  20144  aaliou3lem6  20266  dvtaylp  20287  ulmcn  20316  abelthlem7  20355  pilem3  20370  lawcos  20659  affineequiv  20668  quad2  20680  dcubic1lem  20684  dcubic2  20685  dcubic  20687  mcubic  20688  quart1lem  20696  quart1  20697  asinlem2  20710  asinsin  20733  cosasin  20745  atanlogaddlem  20754  atanlogadd  20755  cvxcl  20824  scvxcvx  20825  bposlem9  21077  lgseisenlem1  21134  2sqlem3  21151  2sqblem  21162  dchrisumlem2  21185  selberg  21243  selberg2  21246  chpdifbndlem1  21248  selberg4  21256  pntrlog2bndlem1  21272  pntrlog2bndlem6  21278  pntibndlem2  21286  pntlemb  21292  pntlemf  21300  padicabv  21325  cusgrasizeinds  21486  fargshiftfo  21626  eupath2lem3  21702  smcnlem  22194  ipval2  22204  hhph  22681  pjhthlem1  22894  golem1  23775  stcltrlem1  23780  ballotlemsdom  24770  lgamgulmlem2  24815  lgamgulmlem3  24816  lgamcvg2  24840  lgam1  24849  rescon  24934  modaddabs  25116  rtrclreclem.trans  25147  iprodgam  25320  faclimlem1  25363  faclimlem3  25365  faclim  25366  iprodfac  25367  colinearalglem2  25847  axsegconlem9  25865  axpasch  25881  axeuclidlem  25902  bpoly4  26106  supadd  26239  itg2addnclem3  26259  itgaddnclem2  26265  itgmulc2nc  26274  ftc1anclem8  26288  dvreasin  26291  areacirclem1  26293  pellexlem2  26894  pell14qrgt0  26923  rmxyadd  26985  rmxluc  27000  fzmaxdif  27047  acongeq  27049  jm2.19lem2  27062  jm2.26lem3  27073  stoweidlem11  27737  stirlinglem5  27804  stirlinglem7  27806  sigarperm  27827  2elfz2melfz  28118  ubmelm1fzo  28128  modadd2mod  28155  modaddmulmod  28159  cshwidxn  28248  onetansqsecsq  28505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-opab 4268  df-mpt 4269  df-id 4499  df-po 4504  df-so 4505  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-pnf 9123  df-mnf 9124  df-ltxr 9126
  Copyright terms: Public domain W3C validator