Theorem addcomd 11339

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

Step	Hyp	Ref	Expression
1		1cnd 11131	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11155	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11160	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11155	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11308	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11308	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11308	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7378	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2781	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11155	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11158	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11158	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11155	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11155	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11322	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11158	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11158	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11155	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11321	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028  1c1 11031   + caddc 11033   · cmul 11035

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  muladd11r  11350  comraddd  11351  subadd2  11388  pncan  11390  npcan  11393  subcan  11440  mvlladdd  11552  subaddeqd  11556  addrsub  11558  mulsubaddmulsub  11605  ltadd1  11608  leadd2  11610  ltsubadd2  11612  lesubadd2  11614  lesub3d  11759  supadd  12114  ltaddrp2d  12987  lincmb01cmp  13415  iccf1o  13416  elfzoext  13642  modaddabs  13835  muladdmodid  13837  negmod  13843  modadd2mod  13848  modadd12d  13854  modaddmulmod  13865  addmodlteq  13873  expaddz  14033  bcn2m1  14251  bcn2p1  14252  lenrevpfxcctswrd  14639  spllen  14681  splfv2a  14683  relexpaddnn  14978  relexpaddg  14980  rtrclreclem3  14987  remullem  15055  sqreulem  15287  bhmafibid2  15396  climaddc2  15563  iseraltlem2  15610  fsumsplit1  15672  telfsumo  15729  fsumparts  15733  bcxmas  15762  bpoly4  15986  sinadd  16093  sincossq  16105  cos2t  16107  absefi  16125  dvdsaddre2b  16238  pwp1fsum  16322  sadadd2lem2  16381  bitsres  16404  bezoutlem2  16471  bezoutlem4  16473  pythagtrip  16766  pcadd2  16822  vdwapun  16906  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  gsumsgrpccat  18769  mulgnndir  19037  mulgdirlem  19039  cyccom  19136  efgcpbllemb  19688  ablfacrp  20001  omndmul2  20066  cncrng  21347  rzgrp  21582  icccvx  24908  cnlmod  25100  cphipval  25203  pjthlem1  25397  cmmbl  25495  voliunlem1  25511  dvle  25972  dvcvx  25985  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem4  25996  dvfsum2  26001  ply1divex  26102  plymullem1  26179  coeeulem  26189  aaliou3lem6  26316  dvtaylp  26338  ulmcn  26368  abelthlem7  26408  pilem3  26423  lawcos  26786  affineequiv  26793  affineequiv3  26795  heron  26808  dcubic1lem  26813  dcubic2  26814  dcubic  26816  mcubic  26817  quart1lem  26825  quart1  26826  asinlem2  26839  asinsin  26862  cosasin  26874  atanlogaddlem  26883  atanlogadd  26884  cvxcl  26955  lgamgulmlem2  27000  lgamcvg2  27025  lgam1  27034  bposlem9  27263  lgseisenlem1  27346  2sqlem3  27391  2sqblem  27402  2sqmod  27407  addsqn2reu  27412  2sqreulem1  27417  2sqreunnlem1  27420  dchrisumlem2  27461  selberg  27519  selberg2  27522  selberg4  27532  pntrlog2bndlem1  27548  pntlemb  27568  pntlemf  27576  padicabv  27601  colinearalglem2  28963  axsegconlem9  28981  axeuclidlem  29018  eupth2lem3lem3  30288  numclwwlk3lem1  30440  smcnlem  30755  ipval2  30765  hhph  31236  pjhthlem1  31449  golem1  32329  stcltrlem1  32334  pythagreim  32806  quad3d  32810  cycpmco2lem3  33191  cycpmco2lem4  33192  cycpmco2lem5  33193  cycpmco2lem6  33194  cycpmco2  33196  archirngz  33252  archiabllem1a  33254  archiabllem1  33256  archiabllem2c  33258  constrrtcc  33873  cos9thpiminplylem1  33920  cos9thpiminplylem2  33921  cos9thpiminplylem3  33922  cos9thpinconstrlem1  33927  ballotlemsdom  34650  fsum2dsub  34745  revwlk  35300  resconn  35421  iprodgam  35917  faclimlem1  35918  faclimlem3  35920  faclim  35921  iprodfac  35922  fwddifnp1  36340  dnibndlem7  36659  dnibndlem8  36660  knoppndvlem14  36700  bj-bary1  37488  dvtan  37842  itgaddnclem2  37851  itgmulc2nc  37860  ftc1anclem8  37872  dvasin  37876  areacirclem1  37880  lcmineqlem19  42338  aks4d1p1p2  42361  posbezout  42391  sticksstones7  42443  sticksstones12a  42448  sticksstones12  42449  bcle2d  42470  aks6d1c7lem1  42471  dffltz  42913  fltbccoprm  42920  flt4lem3  42927  flt4lem5c  42933  flt4lem5d  42934  flt4lem5e  42935  flt4lem7  42938  nna4b4nsq  42939  fltnltalem  42941  3cubeslem2  42963  3cubeslem3l  42964  3cubeslem3r  42965  pellexlem2  43108  pell14qrgt0  43137  rmxyadd  43199  rmxluc  43214  fzmaxdif  43259  acongeq  43261  jm2.19lem2  43268  jm2.26lem3  43279  areaquad  43494  sqrtcval  43918  int-addcomd  44450  int-leftdistd  44456  subadd4b  45567  sub31  45574  coseq0  46144  coskpi2  46146  cosknegpi  46149  fperdvper  46199  dvbdfbdioolem2  46209  dvnmul  46223  dvmptfprodlem  46224  itgsincmulx  46254  itgsbtaddcnst  46262  stoweidlem11  46291  stirlinglem5  46358  stirlinglem7  46360  dirkertrigeqlem1  46378  dirkertrigeqlem2  46379  dirkertrigeqlem3  46380  dirkertrigeq  46381  dirkercncflem2  46384  fourierdlem4  46391  fourierdlem26  46413  fourierdlem40  46427  fourierdlem42  46429  fourierdlem47  46433  fourierdlem63  46449  fourierdlem64  46450  fourierdlem65  46451  fourierdlem74  46460  fourierdlem75  46461  fourierdlem78  46464  fourierdlem79  46465  fourierdlem84  46470  fourierdlem93  46479  fourierdlem103  46489  fourierdlem111  46497  fourierswlem  46510  fouriersw  46511  etransclem32  46546  etransclem46  46560  sge0gtfsumgt  46723  hoidmv1lelem2  46872  hoidmvlelem2  46876  hspmbllem1  46906  smfmullem1  47071  sigarperm  47140  cjnpoly  47171  2elfz2melfz  47600  m1modmmod  47640  mod2addne  47646  fargshiftfo  47724  ichexmpl2  47752  fmtnorec3  47830  2zrngacmnd  48530  2zrngagrp  48531  ply1mulgsumlem1  48668  ackval1  48963  ackval2  48964  resum2sqorgt0  48991  eenglngeehlnmlem2  49020  rrx2linest2  49026  line2xlem  49035  itsclc0yqsollem1  49044  itsclc0yqsol  49046  itscnhlc0xyqsol  49047  itsclc0xyqsolr  49051  itsclinecirc0b  49056  itsclquadb  49058  2itscplem1  49060  2itscp  49063  onetansqsecsq  50042