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

Theorem addcomd 10835
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 10629 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
21, 1addcld 10653 . . . . . . 7 (𝜑 → (1 + 1) ∈ ℂ)
3 muld.1 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
4 addcomd.2 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
52, 3, 4adddid 10658 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 10653 . . . . . . 7 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 10804 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 10804 . . . . . . . 8 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
103, 9syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11 1p1times 10804 . . . . . . . 8 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
124, 11syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
1310, 12oveq12d 7157 . . . . . 6 (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
145, 8, 133eqtr3rd 2845 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
153, 3addcld 10653 . . . . . 6 (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
1615, 4, 4addassd 10656 . . . . 5 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
176, 3, 4addassd 10656 . . . . 5 (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1814, 16, 173eqtr4d 2846 . . . 4 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1915, 4addcld 10653 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
206, 3addcld 10653 . . . . 5 (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21 addcan2 10818 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2219, 20, 4, 21syl3anc 1368 . . . 4 (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2318, 22mpbid 235 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
243, 3, 4addassd 10656 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
253, 4, 3addassd 10656 . . 3 (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2623, 24, 253eqtr3d 2844 . 2 (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
274, 3addcld 10653 . . 3 (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28 addcan 10817 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
293, 6, 27, 28syl3anc 1368 . 2 (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
3026, 29mpbid 235 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2112  (class class class)co 7139  cc 10528  1c1 10531   + caddc 10533   · cmul 10535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-ltxr 10673
This theorem is referenced by:  muladd11r  10846  comraddd  10847  subadd2  10883  pncan  10885  npcan  10888  subcan  10934  mvlladdd  11044  subaddeqd  11048  addrsub  11050  mulsubaddmulsub  11097  ltadd1  11100  leadd2  11102  ltsubadd2  11104  lesubadd2  11106  lesub3d  11251  supadd  11600  ltaddrp2d  12457  lincmb01cmp  12877  iccf1o  12878  modaddabs  13276  muladdmodid  13278  negmod  13283  modadd2mod  13288  modadd12d  13294  modaddmulmod  13305  addmodlteq  13313  expaddz  13473  bcn2m1  13684  bcn2p1  13685  spllen  14111  splfv2a  14113  relexpaddnn  14405  relexpaddg  14407  rtrclreclem3  14414  remullem  14482  sqreulem  14714  bhmafibid2  14821  climaddc2  14987  iseraltlem2  15034  telfsumo  15152  fsumparts  15156  bcxmas  15185  bpoly4  15408  sinadd  15512  sincossq  15524  cos2t  15526  absefi  15544  dvdsaddre2b  15652  pwp1fsum  15735  sadadd2lem2  15792  bitsres  15815  bezoutlem2  15881  bezoutlem4  15883  pythagtrip  16164  pcadd2  16219  vdwapun  16303  vdwlem5  16314  vdwlem6  16315  vdwlem8  16317  gsumsgrpccat  17999  gsumccatOLD  18000  mulgnndir  18251  mulgdirlem  18253  cyccom  18341  efgcpbllemb  18876  cygablOLD  19007  ablfacrp  19184  rzgrp  20315  icccvx  23558  cnlmod  23748  cphipval  23850  pjthlem1  24044  cmmbl  24141  voliunlem1  24157  dvle  24613  dvcvx  24626  dvfsumlem2  24633  dvfsumlem4  24635  dvfsum2  24640  ply1divex  24740  plymullem1  24814  coeeulem  24824  aaliou3lem6  24947  dvtaylp  24968  ulmcn  24997  abelthlem7  25036  pilem3  25051  lawcos  25405  affineequiv  25412  affineequiv3  25414  heron  25427  dcubic1lem  25432  dcubic2  25433  dcubic  25435  mcubic  25436  quart1lem  25444  quart1  25445  asinlem2  25458  asinsin  25481  cosasin  25493  atanlogaddlem  25502  atanlogadd  25503  cvxcl  25573  lgamgulmlem2  25618  lgamcvg2  25643  lgam1  25652  bposlem9  25879  lgseisenlem1  25962  2sqlem3  26007  2sqblem  26018  2sqmod  26023  addsqn2reu  26028  2sqreulem1  26033  2sqreunnlem1  26036  dchrisumlem2  26077  selberg  26135  selberg2  26138  selberg4  26148  pntrlog2bndlem1  26164  pntlemb  26184  pntlemf  26192  padicabv  26217  colinearalglem2  26704  axsegconlem9  26722  axeuclidlem  26759  eupth2lem3lem3  28018  numclwwlk3lem1  28170  smcnlem  28483  ipval2  28493  hhph  28964  pjhthlem1  29177  golem1  30057  stcltrlem1  30062  omndmul2  30766  cycpmco2lem3  30823  cycpmco2lem4  30824  cycpmco2lem5  30825  cycpmco2lem6  30826  cycpmco2  30828  archirngz  30871  archiabllem1a  30873  archiabllem1  30875  archiabllem2c  30877  ballotlemsdom  31877  fsum2dsub  31986  revwlk  32479  resconn  32601  iprodgam  33082  faclimlem1  33083  faclimlem3  33085  faclim  33086  iprodfac  33087  fwddifnp1  33734  dnibndlem7  33931  dnibndlem8  33932  knoppndvlem14  33972  bj-bary1  34721  dvtan  35100  itgaddnclem2  35109  itgmulc2nc  35118  ftc1anclem8  35130  dvasin  35134  areacirclem1  35138  lcmineqlem19  39328  metakunt15  39355  metakunt16  39356  dffltz  39602  fltnltalem  39605  3cubeslem2  39613  3cubeslem3l  39614  3cubeslem3r  39615  pellexlem2  39758  pell14qrgt0  39787  rmxyadd  39849  rmxluc  39864  fzmaxdif  39909  acongeq  39911  jm2.19lem2  39918  jm2.26lem3  39929  areaquad  40153  sqrtcval  40328  int-addcomd  40866  int-leftdistd  40872  subadd4b  41900  sub31  41909  fsumsplit1  42201  coseq0  42493  coskpi2  42495  cosknegpi  42498  fperdvper  42548  dvbdfbdioolem2  42558  dvnmul  42572  dvmptfprodlem  42573  itgsincmulx  42603  itgsbtaddcnst  42611  stoweidlem11  42640  stirlinglem5  42707  stirlinglem7  42709  dirkertrigeqlem1  42727  dirkertrigeqlem2  42728  dirkertrigeqlem3  42729  dirkertrigeq  42730  dirkercncflem2  42733  fourierdlem4  42740  fourierdlem26  42762  fourierdlem40  42776  fourierdlem42  42778  fourierdlem47  42782  fourierdlem63  42798  fourierdlem64  42799  fourierdlem65  42800  fourierdlem74  42809  fourierdlem75  42810  fourierdlem78  42813  fourierdlem79  42814  fourierdlem84  42819  fourierdlem93  42828  fourierdlem103  42838  fourierdlem111  42846  fourierswlem  42859  fouriersw  42860  etransclem32  42895  etransclem46  42909  sge0gtfsumgt  43069  hoidmv1lelem2  43218  hoidmvlelem2  43222  hspmbllem1  43252  smfmullem1  43410  sigarperm  43461  2elfz2melfz  43862  fargshiftfo  43946  ichexmpl2  43974  fmtnorec3  44052  2zrngacmnd  44553  2zrngagrp  44554  ply1mulgsumlem1  44781  m1modmmod  44922  ackval1  45082  ackval2  45083  resum2sqorgt0  45110  eenglngeehlnmlem2  45139  rrx2linest2  45145  line2xlem  45154  itsclc0yqsollem1  45163  itsclc0yqsol  45165  itscnhlc0xyqsol  45166  itsclc0xyqsolr  45170  itsclinecirc0b  45175  itsclquadb  45177  2itscplem1  45179  2itscp  45182  onetansqsecsq  45274
  Copyright terms: Public domain W3C validator