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

Theorem addcomd 10276
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 (𝜑𝐴 ∈ ℂ)
addcomd.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
addcomd (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcomd
StepHypRef Expression
1 1cnd 10094 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
21, 1addcld 10097 . . . . . . 7 (𝜑 → (1 + 1) ∈ ℂ)
3 muld.1 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
4 addcomd.2 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
52, 3, 4adddid 10102 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 10097 . . . . . . 7 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 10245 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 10245 . . . . . . . 8 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
103, 9syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11 1p1times 10245 . . . . . . . 8 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
124, 11syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
1310, 12oveq12d 6708 . . . . . 6 (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
145, 8, 133eqtr3rd 2694 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
153, 3addcld 10097 . . . . . 6 (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
1615, 4, 4addassd 10100 . . . . 5 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
176, 3, 4addassd 10100 . . . . 5 (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1814, 16, 173eqtr4d 2695 . . . 4 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1915, 4addcld 10097 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
206, 3addcld 10097 . . . . 5 (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21 addcan2 10259 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2219, 20, 4, 21syl3anc 1366 . . . 4 (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2318, 22mpbid 222 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
243, 3, 4addassd 10100 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
253, 4, 3addassd 10100 . . 3 (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2623, 24, 253eqtr3d 2693 . 2 (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
274, 3addcld 10097 . . 3 (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28 addcan 10258 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
293, 6, 27, 28syl3anc 1366 . 2 (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
3026, 29mpbid 222 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972  1c1 9975   + caddc 9977   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-ltxr 10117
This theorem is referenced by:  muladd11r  10287  comraddd  10288  subadd2  10323  pncan  10325  npcan  10328  subcan  10374  subaddeqd  10484  addrsub  10486  ltadd1  10533  leadd2  10535  ltsubadd2  10537  lesubadd2  10539  lesub3d  10683  supadd  11029  ltaddrp2d  11944  lincmb01cmp  12353  iccf1o  12354  modaddabs  12748  muladdmodid  12750  negmod  12755  modadd2mod  12760  modadd12d  12766  modaddmulmod  12777  addmodlteq  12785  expaddz  12944  bcn2m1  13151  bcn2p1  13152  ccatrn  13407  addlenswrd  13484  spllen  13551  splfv2a  13553  relexpaddnn  13835  relexpaddg  13837  rtrclreclem3  13844  remullem  13912  sqreulem  14143  climaddc2  14410  clim2ser2  14430  iseraltlem2  14457  telfsumo  14578  fsumparts  14582  bcxmas  14611  bpoly4  14834  cosneg  14921  coshval  14929  sinadd  14938  sincossq  14950  cos2t  14952  absefi  14970  absefib  14972  dvdsaddre2b  15076  pwp1fsum  15161  sadadd2lem2  15219  bitsres  15242  bezoutlem2  15304  bezoutlem4  15306  pythagtrip  15586  pcadd2  15641  vdwapun  15725  vdwlem5  15736  vdwlem6  15737  vdwlem8  15739  gsumccat  17425  mulgnndir  17616  mulgnndirOLD  17617  mulgdirlem  17619  mulgdir  17620  sylow1lem1  18059  efgcpbllemb  18214  cygabl  18338  ablfacrp  18511  icccvx  22796  cnlmod  22986  cphipval  23088  pjthlem1  23254  ovolicc2lem4  23334  cmmbl  23348  voliunlem1  23364  itgmulc2  23645  dvle  23815  dvcvx  23828  dvfsumlem2  23835  dvfsumlem4  23837  dvfsum2  23842  ply1divex  23941  plymullem1  24015  coeeulem  24025  aaliou3lem6  24148  dvtaylp  24169  ulmcn  24198  abelthlem7  24237  pilem3  24252  rzgrp  24345  lawcos  24591  affineequiv  24598  heron  24610  quad2  24611  dcubic1lem  24615  dcubic2  24616  dcubic  24618  mcubic  24619  quart1lem  24627  quart1  24628  asinlem2  24641  asinsin  24664  cosasin  24676  atanlogaddlem  24685  atanlogadd  24686  cvxcl  24756  scvxcvx  24757  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamcvg2  24826  lgam1  24835  bposlem9  25062  lgseisenlem1  25145  2sqlem3  25190  2sqblem  25201  dchrisumlem2  25224  selberg  25282  selberg2  25285  chpdifbndlem1  25287  selberg4  25295  pntrlog2bndlem1  25311  pntrlog2bndlem6  25317  pntibndlem2  25325  pntlemb  25331  pntlemf  25339  padicabv  25364  colinearalglem2  25832  axsegconlem9  25850  axeuclidlem  25887  eupth2lem3lem3  27208  numclwlk3lem3  27322  2clwwlk2clwwlklem2lem2  27329  smcnlem  27680  ipval2  27690  hhph  28163  pjhthlem1  28378  golem1  29258  stcltrlem1  29263  bhmafibid2  29773  2sqmod  29776  omndmul2  29840  archirngz  29871  archiabllem1a  29873  archiabllem1  29875  archiabllem2c  29877  ballotlemsdom  30701  signshf  30793  fsum2dsub  30813  resconn  31354  iprodgam  31754  faclimlem1  31755  faclimlem3  31757  faclim  31758  iprodfac  31759  fwddifnp1  32397  dnibndlem7  32599  dnibndlem8  32600  knoppndvlem14  32641  bj-bary1  33292  dvtan  33590  itg2addnclem3  33593  itgaddnclem2  33599  itgmulc2nc  33608  ftc1anclem8  33622  dvasin  33626  areacirclem1  33630  pellexlem2  37711  pell14qrgt0  37740  rmxyadd  37803  rmxluc  37818  fzmaxdif  37865  acongeq  37867  jm2.19lem2  37874  jm2.26lem3  37885  areaquad  38119  int-addcomd  38793  int-leftdistd  38799  subadd4b  39808  sub31  39817  fsumsplit1  40122  coseq0  40393  coskpi2  40395  cosknegpi  40398  fperdvper  40451  dvbdfbdioolem2  40462  dvnmul  40476  dvmptfprodlem  40477  itgsincmulx  40508  itgsbtaddcnst  40516  stoweidlem11  40546  stirlinglem5  40613  stirlinglem7  40615  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem4  40646  fourierdlem26  40668  fourierdlem40  40682  fourierdlem42  40684  fourierdlem47  40688  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem79  40720  fourierdlem84  40725  fourierdlem93  40734  fourierdlem103  40744  fourierdlem111  40752  fourierswlem  40765  fouriersw  40766  etransclem32  40801  etransclem46  40815  sge0gtfsumgt  40978  hoidmv1lelem2  41127  hoidmvlelem2  41131  hspmbllem1  41161  smfmullem1  41319  sigarperm  41370  2elfz2melfz  41653  fargshiftfo  41703  fmtnorec3  41785  2zrngacmnd  42267  2zrngagrp  42268  ply1mulgsumlem1  42499  m1modmmod  42641  onetansqsecsq  42830  mvlladdd  42841
  Copyright terms: Public domain W3C validator