MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcomd Structured version   Unicode version
Theorem addcomd 9771
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 1cnd 9601 . . . . . . . 8 |- ( ph -> 1 e. CC )
21, 1addcld 9604 . . . . . . 7 |- ( ph -> ( 1 + 1 ) e. CC )
3 muld.1 . . . . . . 7 |- ( ph -> A e. CC )
4 addcomd.2 . . . . . . 7 |- ( ph -> B e. CC )
52, 3, 4adddid 9609 . . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
63, 4addcld 9604 . . . . . . 7 |- ( ph -> ( A + B ) e. CC )
7 1p1times 9740 . . . . . . 7 |- ( ( A + B ) e. CC -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
86, 7syl 16 . . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
9 1p1times 9740 . . . . . . . 8 |- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
103, 9syl 16 . . . . . . 7 |- ( ph -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
11 1p1times 9740 . . . . . . . 8 |- ( B e. CC -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
124, 11syl 16 . . . . . . 7 |- ( ph -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
1310, 12oveq12d 6288 . . . . . 6 |- ( ph -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
145, 8, 133eqtr3rd 2504 . . . . 5 |- ( ph -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
153, 3addcld 9604 . . . . . 6 |- ( ph -> ( A + A ) e. CC )
1615, 4, 4addassd 9607 . . . . 5 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
176, 3, 4addassd 9607 . . . . 5 |- ( ph -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
1814, 16, 173eqtr4d 2505 . . . 4 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
1915, 4addcld 9604 . . . . 5 |- ( ph -> ( ( A + A ) + B ) e. CC )
206, 3addcld 9604 . . . . 5 |- ( ph -> ( ( A + B ) + A ) e. CC )
21 addcan2 9754 . . . . 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 ) ) )
2219, 20, 4, 21syl3anc 1226 . . . 4 |- ( ph -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
2318, 22mpbid 210 . . 3 |- ( ph -> ( ( A + A ) + B ) = ( ( A + B ) + A ) )
243, 3, 4addassd 9607 . . 3 |- ( ph -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
253, 4, 3addassd 9607 . . 3 |- ( ph -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
2623, 24, 253eqtr3d 2503 . 2 |- ( ph -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
274, 3addcld 9604 . . 3 |- ( ph -> ( B + A ) e. CC )
28 addcan 9753 . . 3 |- ( ( A e. CC /\ ( A + B ) e. CC /\ ( B + A ) e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
293, 6, 27, 28syl3anc 1226 . 2 |- ( ph -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
3026, 29mpbid 210 1 |- ( ph -> ( A + B ) = ( B + A ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 184   = wceq 1398   e. wcel 1823  (class class class)co 6270   CCcc 9479   1c1 9482   + caddc 9484   x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-po 4789  df-so 4790  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-ltxr 9622
This theorem is referenced by:  subadd2  9815  pncan  9817  npcan  9820  subcan  9865  addrsub  9975  ltadd1  10015  leadd2  10017  ltsubadd2  10019  lesubadd2  10021  ltaddrp2d  11289  lincmb01cmp  11666  iccf1o  11667  modaddabs  12017  muladdmodid  12019  negmod  12020  modadd2mod  12022  modadd12d  12028  modaddmulmod  12038  expaddz  12195  bcn2m1  12387  bcn2p1  12388  ccatrn  12598  addlenswrd  12657  spllen  12724  splfv2a  12726  relexpaddnn  12969  relexpaddg  12971  rtrclreclem3  12978  remullem  13046  sqreulem  13277  climaddc2  13543  clim2ser2  13563  iseraltlem2  13590  telfsumo  13701  fsumparts  13705  bcxmas  13732  cosneg  13967  coshval  13975  sinadd  13984  sincossq  13996  cos2t  13998  absefi  14016  absefib  14018  sadadd2lem2  14187  bitsres  14210  bezoutlem2  14264  bezoutlem4  14266  pythagtrip  14445  pcadd2  14496  vdwapun  14579  vdwlem5  14590  vdwlem6  14591  vdwlem8  14593  gsumccat  16211  mulgnndir  16366  mulgdirlem  16368  mulgdir  16369  sylow1lem1  16820  efgcpbllemb  16975  cygabl  17095  ablfacrp  17315  icccvx  21619  pjthlem1  22021  ovolicc2lem4  22100  cmmbl  22114  voliunlem1  22129  itgmulc2  22409  dvle  22577  dvcvx  22590  dvfsumlem2  22597  dvfsumlem4  22599  dvfsum2  22604  ply1divex  22706  plymullem1  22780  coeeulem  22790  aaliou3lem6  22913  dvtaylp  22934  ulmcn  22963  abelthlem7  23002  pilem3  23017  rzgrp  23110  lawcos  23350  affineequiv  23357  heron  23369  quad2  23370  dcubic1lem  23374  dcubic2  23375  dcubic  23377  mcubic  23378  quart1lem  23386  quart1  23387  asinlem2  23400  asinsin  23423  cosasin  23435  atanlogaddlem  23444  atanlogadd  23445  cvxcl  23515  scvxcvx  23516  bposlem9  23768  lgseisenlem1  23825  2sqlem3  23842  2sqblem  23853  dchrisumlem2  23876  selberg  23934  selberg2  23937  chpdifbndlem1  23939  selberg4  23947  pntrlog2bndlem1  23963  pntrlog2bndlem6  23969  pntibndlem2  23977  pntlemb  23983  pntlemf  23991  padicabv  24016  colinearalglem2  24415  axsegconlem9  24433  axpasch  24449  axeuclidlem  24470  cusgrasizeinds  24681  fargshiftfo  24843  eupath2lem3  25184  numclwlk3lem3  25278  smcnlem  25808  ipval2  25818  hhph  26296  pjhthlem1  26510  golem1  27391  stcltrlem1  27396  addeqxfrd  27794  bhmafibid2  27870  2sqmod  27873  omndmul2  27939  archirngz  27970  archiabllem1a  27972  archiabllem1  27974  archiabllem2c  27976  ballotlemsdom  28717  signshf  28812  lgamgulmlem2  28839  lgamgulmlem3  28840  lgamcvg2  28864  lgam1  28873  rescon  28958  iprodgam  29369  faclimlem1  29412  faclimlem3  29414  faclim  29415  iprodfac  29416  bpoly4  30052  supadd  30285  dvtan  30308  itg2addnclem3  30311  itgaddnclem2  30317  itgmulc2nc  30326  ftc1anclem8  30340  dvasin  30346  areacirclem1  30350  pellexlem2  31008  pell14qrgt0  31037  rmxyadd  31099  rmxluc  31114  fzmaxdif  31161  acongeq  31163  jm2.19lem2  31174  jm2.26lem3  31185  areaquad  31428  subadd4b  31707  sub31  31722  fsumsplit1  31815  coseq0  31906  coskpi2  31908  cosknegpi  31911  fperdvper  31957  dvbdfbdioolem2  31968  dvnmul  31982  dvmptfprodlem  31983  itgsincmulx  32015  itgsbtaddcnst  32023  stoweidlem11  32035  stirlinglem5  32102  stirlinglem7  32104  dirkertrigeqlem1  32122  dirkertrigeqlem2  32123  dirkertrigeqlem3  32124  dirkertrigeq  32125  dirkercncflem2  32128  fourierdlem4  32135  fourierdlem26  32157  fourierdlem40  32171  fourierdlem42  32173  fourierdlem47  32178  fourierdlem63  32194  fourierdlem64  32195  fourierdlem65  32196  fourierdlem74  32205  fourierdlem75  32206  fourierdlem78  32209  fourierdlem79  32210  fourierdlem84  32215  fourierdlem93  32224  fourierdlem103  32234  fourierdlem111  32242  fourierswlem  32255  fouriersw  32256  etransclem32  32291  etransclem46  32305  sigarperm  32319  2elfz2melfz  32727  2zrngacmnd  33021  2zrngagrp  33022  ply1mulgsumlem1  33259  m1modmmod  33407  onetansqsecsq  33564  comraddd  33583  mvlladdd  33585  bj-bary1  35097  int-addcomd  38525  int-leftdistd  38531
  Copyright terms: Public domain W3C validator