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

Theorem addcomd 9268
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 9048 . . . . . . . . 9  |-  1  e.  CC
21a1i 11 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
32, 2addcld 9107 . . . . . . 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 9112 . . . . . 6  |-  ( ph  ->  ( ( 1  +  1 )  x.  ( A  +  B )
)  =  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) ) )
74, 5addcld 9107 . . . . . . 7  |-  ( ph  ->  ( A  +  B
)  e.  CC )
8 1p1times 9237 . . . . . . 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 9237 . . . . . . . 8  |-  ( A  e.  CC  ->  (
( 1  +  1 )  x.  A )  =  ( A  +  A ) )
114, 10syl 16 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  1 )  x.  A
)  =  ( A  +  A ) )
12 1p1times 9237 . . . . . . . 8  |-  ( B  e.  CC  ->  (
( 1  +  1 )  x.  B )  =  ( B  +  B ) )
135, 12syl 16 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  1 )  x.  B
)  =  ( B  +  B ) )
1411, 13oveq12d 6099 . . . . . 6  |-  ( ph  ->  ( ( ( 1  +  1 )  x.  A )  +  ( ( 1  +  1 )  x.  B ) )  =  ( ( A  +  A )  +  ( B  +  B ) ) )
156, 9, 143eqtr3rd 2477 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  ( B  +  B ) )  =  ( ( A  +  B )  +  ( A  +  B ) ) )
164, 4addcld 9107 . . . . . 6  |-  ( ph  ->  ( A  +  A
)  e.  CC )
1716, 5, 5addassd 9110 . . . . 5  |-  ( ph  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( A  +  A )  +  ( B  +  B ) ) )
187, 4, 5addassd 9110 . . . . 5  |-  ( ph  ->  ( ( ( A  +  B )  +  A )  +  B
)  =  ( ( A  +  B )  +  ( A  +  B ) ) )
1915, 17, 183eqtr4d 2478 . . . 4  |-  ( ph  ->  ( ( ( A  +  A )  +  B )  +  B
)  =  ( ( ( A  +  B
)  +  A )  +  B ) )
2016, 5addcld 9107 . . . . 5  |-  ( ph  ->  ( ( A  +  A )  +  B
)  e.  CC )
217, 4addcld 9107 . . . . 5  |-  ( ph  ->  ( ( A  +  B )  +  A
)  e.  CC )
22 addcan2 9251 . . . . 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 1184 . . . 4  |-  ( ph  ->  ( ( ( ( A  +  A )  +  B )  +  B )  =  ( ( ( A  +  B )  +  A
)  +  B )  <-> 
( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) ) )
2419, 23mpbid 202 . . 3  |-  ( ph  ->  ( ( A  +  A )  +  B
)  =  ( ( A  +  B )  +  A ) )
254, 4, 5addassd 9110 . . 3  |-  ( ph  ->  ( ( A  +  A )  +  B
)  =  ( A  +  ( A  +  B ) ) )
264, 5, 4addassd 9110 . . 3  |-  ( ph  ->  ( ( A  +  B )  +  A
)  =  ( A  +  ( B  +  A ) ) )
2724, 25, 263eqtr3d 2476 . 2  |-  ( ph  ->  ( A  +  ( A  +  B ) )  =  ( A  +  ( B  +  A ) ) )
285, 4addcld 9107 . . 3  |-  ( ph  ->  ( B  +  A
)  e.  CC )
29 addcan 9250 . . 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 1184 . 2  |-  ( ph  ->  ( ( A  +  ( A  +  B
) )  =  ( A  +  ( B  +  A ) )  <-> 
( A  +  B
)  =  ( B  +  A ) ) )
3127, 30mpbid 202 1  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725  (class class class)co 6081   CCcc 8988   1c1 8991    + caddc 8993    x. cmul 8995
This theorem is referenced by:  subadd2  9309  pncan  9311  npcan  9314  subcan  9356  ltadd1  9495  leadd2  9497  ltsubadd2  9499  lesubadd2  9501  ltaddrp2d  10678  lincmb01cmp  11038  iccf1o  11039  modadd12d  11282  expaddz  11424  bcn2m1  11615  bcn2p1  11616  spllen  11783  splfv2a  11785  remullem  11933  sqreulem  12163  climaddc2  12429  clim2ser2  12449  iseraltlem2  12476  fsumtscopo  12581  fsumparts  12585  bcxmas  12615  cosneg  12748  coshval  12756  sinadd  12765  sincossq  12777  cos2t  12779  absefi  12797  absefib  12799  sadadd2lem2  12962  bitsres  12985  bezoutlem2  13039  bezoutlem4  13041  pythagtrip  13208  pcadd2  13259  vdwapun  13342  vdwlem5  13353  vdwlem6  13354  vdwlem8  13356  gsumccat  14787  mulgnndir  14912  mulgdirlem  14914  mulgdir  14915  sylow1lem1  15232  efgcpbllemb  15387  cygabl  15500  ablfacrp  15624  icccvx  18975  pjthlem1  19338  ovolicc2lem4  19416  cmmbl  19429  voliunlem1  19444  itgmulc2  19725  dvle  19891  dvcvx  19904  dvfsumlem2  19911  dvfsumlem4  19913  dvfsum2  19918  ply1divex  20059  plymullem1  20133  coeeulem  20143  aaliou3lem6  20265  dvtaylp  20286  ulmcn  20315  abelthlem7  20354  pilem3  20369  lawcos  20658  affineequiv  20667  quad2  20679  dcubic1lem  20683  dcubic2  20684  dcubic  20686  mcubic  20687  quart1lem  20695  quart1  20696  asinlem2  20709  asinsin  20732  cosasin  20744  atanlogaddlem  20753  atanlogadd  20754  cvxcl  20823  scvxcvx  20824  bposlem9  21076  lgseisenlem1  21133  2sqlem3  21150  2sqblem  21161  dchrisumlem2  21184  selberg  21242  selberg2  21245  chpdifbndlem1  21247  selberg4  21255  pntrlog2bndlem1  21271  pntrlog2bndlem6  21277  pntibndlem2  21285  pntlemb  21291  pntlemf  21299  padicabv  21324  cusgrasizeinds  21485  fargshiftfo  21625  eupath2lem3  21701  smcnlem  22193  ipval2  22203  hhph  22680  pjhthlem1  22893  golem1  23774  stcltrlem1  23779  ballotlemsdom  24769  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamcvg2  24839  lgam1  24848  rescon  24933  modaddabs  25115  rtrclreclem.trans  25146  iprodgam  25319  faclimlem1  25362  faclimlem3  25364  faclim  25365  iprodfac  25366  colinearalglem2  25846  axsegconlem9  25864  axpasch  25880  axeuclidlem  25901  bpoly4  26105  supadd  26238  itg2addnclem3  26258  itgaddnclem2  26264  itgmulc2nc  26273  ftc1anclem8  26287  dvreasin  26290  areacirclem1  26292  pellexlem2  26893  pell14qrgt0  26922  rmxyadd  26984  rmxluc  26999  fzmaxdif  27046  acongeq  27048  jm2.19lem2  27061  jm2.26lem3  27072  stoweidlem11  27736  stirlinglem5  27803  stirlinglem7  27805  sigarperm  27826  2elfz2melfz  28117  ubmelm1fzo  28127  modadd2mod  28154  modaddmulmod  28158  cshwidxn  28247  onetansqsecsq  28504
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-po 4503  df-so 4504  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-er 6905  df-en 7110  df-dom 7111  df-sdom 7112  df-pnf 9122  df-mnf 9123  df-ltxr 9125
  Copyright terms: Public domain W3C validator