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

Theorem addcomd 10644
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 10436 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
21, 1addcld 10461 . . . . . . 7 (𝜑 → (1 + 1) ∈ ℂ)
3 muld.1 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
4 addcomd.2 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
52, 3, 4adddid 10466 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 10461 . . . . . . 7 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 10613 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 10613 . . . . . . . 8 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
103, 9syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11 1p1times 10613 . . . . . . . 8 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
124, 11syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
1310, 12oveq12d 6996 . . . . . 6 (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
145, 8, 133eqtr3rd 2823 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
153, 3addcld 10461 . . . . . 6 (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
1615, 4, 4addassd 10464 . . . . 5 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
176, 3, 4addassd 10464 . . . . 5 (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1814, 16, 173eqtr4d 2824 . . . 4 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1915, 4addcld 10461 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
206, 3addcld 10461 . . . . 5 (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21 addcan2 10627 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2219, 20, 4, 21syl3anc 1351 . . . 4 (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2318, 22mpbid 224 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
243, 3, 4addassd 10464 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
253, 4, 3addassd 10464 . . 3 (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2623, 24, 253eqtr3d 2822 . 2 (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
274, 3addcld 10461 . . 3 (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28 addcan 10626 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
293, 6, 27, 28syl3anc 1351 . 2 (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
3026, 29mpbid 224 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1507  wcel 2050  (class class class)co 6978  cc 10335  1c1 10338   + caddc 10340   · cmul 10342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-po 5327  df-so 5328  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-ov 6981  df-er 8091  df-en 8309  df-dom 8310  df-sdom 8311  df-pnf 10478  df-mnf 10479  df-ltxr 10481
This theorem is referenced by:  muladd11r  10655  comraddd  10656  subadd2  10692  pncan  10694  npcan  10698  subcan  10744  mvlladdd  10854  subaddeqd  10858  addrsub  10860  mulsubaddmulsub  10907  ltadd1  10910  leadd2  10912  ltsubadd2  10914  lesubadd2  10916  lesub3d  11061  supadd  11412  ltaddrp2d  12285  lincmb01cmp  12700  iccf1o  12701  modaddabs  13095  muladdmodid  13097  negmod  13102  modadd2mod  13107  modadd12d  13113  modaddmulmod  13124  addmodlteq  13132  expaddz  13291  bcn2m1  13502  bcn2p1  13503  ccatrn  13755  addlenswrdOLD  13833  spllen  13972  spllenOLD  13973  splfv2a  13976  splfv2aOLD  13977  relexpaddnn  14274  relexpaddg  14276  rtrclreclem3  14283  remullem  14351  sqreulem  14583  bhmafibid2  14690  climaddc2  14856  iseraltlem2  14903  telfsumo  15020  fsumparts  15024  bcxmas  15053  bpoly4  15276  sinadd  15380  sincossq  15392  cos2t  15394  absefi  15412  dvdsaddre2b  15520  pwp1fsum  15605  sadadd2lem2  15662  bitsres  15685  bezoutlem2  15747  bezoutlem4  15749  pythagtrip  16030  pcadd2  16085  vdwapun  16169  vdwlem5  16180  vdwlem6  16181  vdwlem8  16183  gsumccat  17849  mulgnndir  18043  mulgdirlem  18045  efgcpbllemb  18644  cygabl  18768  ablfacrp  18941  rzgrp  20472  icccvx  23260  cnlmod  23450  cphipval  23552  pjthlem1  23746  cmmbl  23841  voliunlem1  23857  dvle  24310  dvcvx  24323  dvfsumlem2  24330  dvfsumlem4  24332  dvfsum2  24337  ply1divex  24436  plymullem1  24510  coeeulem  24520  aaliou3lem6  24643  dvtaylp  24664  ulmcn  24693  abelthlem7  24732  pilem3  24747  lawcos  25098  affineequiv  25105  affineequiv3  25107  heron  25120  dcubic1lem  25125  dcubic2  25126  dcubic  25128  mcubic  25129  quart1lem  25137  quart1  25138  asinlem2  25151  asinsin  25174  cosasin  25186  atanlogaddlem  25195  atanlogadd  25196  cvxcl  25267  lgamgulmlem2  25312  lgamcvg2  25337  lgam1  25346  bposlem9  25573  lgseisenlem1  25656  2sqlem3  25701  2sqblem  25712  2sqmod  25717  addsqn2reu  25722  2sqreulem1  25727  2sqreunnlem1  25730  dchrisumlem2  25771  selberg  25829  selberg2  25832  selberg4  25842  pntrlog2bndlem1  25858  pntlemb  25878  pntlemf  25886  padicabv  25911  colinearalglem2  26399  axsegconlem9  26417  axeuclidlem  26454  eupth2lem3lem3  27763  numclwwlk3lem1  27942  smcnlem  28254  ipval2  28264  hhph  28737  pjhthlem1  28952  golem1  29832  stcltrlem1  29837  omndmul2  30431  archirngz  30484  archiabllem1a  30486  archiabllem1  30488  archiabllem2c  30490  ballotlemsdom  31415  signshf  31506  fsum2dsub  31526  resconn  32078  iprodgam  32494  faclimlem1  32495  faclimlem3  32497  faclim  32498  iprodfac  32499  fwddifnp1  33147  dnibndlem7  33343  dnibndlem8  33344  knoppndvlem14  33384  bj-bary1  34041  dvtan  34383  itg2addnclem3  34386  itgaddnclem2  34392  itgmulc2nc  34401  ftc1anclem8  34415  dvasin  34419  areacirclem1  34423  dffltz  38678  fltnltalem  38681  pellexlem2  38823  pell14qrgt0  38852  rmxyadd  38914  rmxluc  38929  fzmaxdif  38974  acongeq  38976  jm2.19lem2  38983  jm2.26lem3  38994  areaquad  39219  int-addcomd  39891  int-leftdistd  39897  subadd4b  40978  sub31  40987  fsumsplit1  41285  coseq0  41576  coskpi2  41578  cosknegpi  41581  fperdvper  41634  dvbdfbdioolem2  41645  dvnmul  41659  dvmptfprodlem  41660  itgsincmulx  41690  itgsbtaddcnst  41698  stoweidlem11  41728  stirlinglem5  41795  stirlinglem7  41797  dirkertrigeqlem1  41815  dirkertrigeqlem2  41816  dirkertrigeqlem3  41817  dirkertrigeq  41818  dirkercncflem2  41821  fourierdlem4  41828  fourierdlem26  41850  fourierdlem40  41864  fourierdlem42  41866  fourierdlem47  41870  fourierdlem63  41886  fourierdlem64  41887  fourierdlem65  41888  fourierdlem74  41897  fourierdlem75  41898  fourierdlem78  41901  fourierdlem79  41902  fourierdlem84  41907  fourierdlem93  41916  fourierdlem103  41926  fourierdlem111  41934  fourierswlem  41947  fouriersw  41948  etransclem32  41983  etransclem46  41997  sge0gtfsumgt  42157  hoidmv1lelem2  42306  hoidmvlelem2  42310  hspmbllem1  42340  smfmullem1  42498  sigarperm  42549  2elfz2melfz  42925  fargshiftfo  42975  ichexmpl2  43001  fmtnorec3  43079  2zrngacmnd  43578  2zrngagrp  43579  ply1mulgsumlem1  43808  m1modmmod  43950  resum2sqorgt0  44065  eenglngeehlnmlem2  44094  rrx2linest2  44100  line2xlem  44109  itsclc0yqsollem1  44118  itsclc0yqsol  44120  itscnhlc0xyqsol  44121  itsclc0xyqsolr  44125  itsclinecirc0b  44130  itsclquadb  44132  2itscplem1  44134  2itscp  44137  onetansqsecsq  44228
  Copyright terms: Public domain W3C validator