Theorem addcomd 11348

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 11139	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11164	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11169	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11164	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11317	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11317	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11317	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7385	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2781	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11164	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11167	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11167	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11164	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11164	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11331	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11167	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11167	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11164	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11330	. . 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 7367  ℂcc 11036  1c1 11039   + caddc 11041   · cmul 11043

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 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  muladd11r  11359  comraddd  11360  subadd2  11397  pncan  11399  npcan  11402  subcan  11449  mvlladdd  11561  subaddeqd  11565  addrsub  11567  mulsubaddmulsub  11614  ltadd1  11617  leadd2  11619  ltsubadd2  11621  lesubadd2  11623  lesub3d  11768  supadd  12124  ltaddrp2d  13020  lincmb01cmp  13448  iccf1o  13449  elfzoext  13677  modaddabs  13870  muladdmodid  13872  negmod  13878  modadd2mod  13883  modadd12d  13889  modaddmulmod  13900  addmodlteq  13908  expaddz  14068  bcn2m1  14286  bcn2p1  14287  lenrevpfxcctswrd  14674  spllen  14716  splfv2a  14718  relexpaddnn  15013  relexpaddg  15015  rtrclreclem3  15022  remullem  15090  sqreulem  15322  bhmafibid2  15431  climaddc2  15598  iseraltlem2  15645  fsumsplit1  15707  telfsumo  15765  fsumparts  15769  bcxmas  15800  bpoly4  16024  sinadd  16131  sincossq  16143  cos2t  16145  absefi  16163  dvdsaddre2b  16276  pwp1fsum  16360  sadadd2lem2  16419  bitsres  16442  bezoutlem2  16509  bezoutlem4  16511  pythagtrip  16805  pcadd2  16861  vdwapun  16945  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  gsumsgrpccat  18808  mulgnndir  19079  mulgdirlem  19081  cyccom  19178  efgcpbllemb  19730  ablfacrp  20043  omndmul2  20108  cncrng  21373  rzgrp  21603  icccvx  24917  cnlmod  25107  cphipval  25210  pjthlem1  25404  cmmbl  25501  voliunlem1  25517  dvle  25974  dvcvx  25987  dvfsumlem2  25994  dvfsumlem4  25996  dvfsum2  26001  ply1divex  26102  plymullem1  26179  coeeulem  26189  aaliou3lem6  26314  dvtaylp  26335  ulmcn  26364  abelthlem7  26403  pilem3  26418  lawcos  26780  affineequiv  26787  affineequiv3  26789  heron  26802  dcubic1lem  26807  dcubic2  26808  dcubic  26810  mcubic  26811  quart1lem  26819  quart1  26820  asinlem2  26833  asinsin  26856  cosasin  26868  atanlogaddlem  26877  atanlogadd  26878  cvxcl  26948  lgamgulmlem2  26993  lgamcvg2  27018  lgam1  27027  bposlem9  27255  lgseisenlem1  27338  2sqlem3  27383  2sqblem  27394  2sqmod  27399  addsqn2reu  27404  2sqreulem1  27409  2sqreunnlem1  27412  dchrisumlem2  27453  selberg  27511  selberg2  27514  selberg4  27524  pntrlog2bndlem1  27540  pntlemb  27560  pntlemf  27568  padicabv  27593  colinearalglem2  28976  axsegconlem9  28994  axeuclidlem  29031  eupth2lem3lem3  30300  numclwwlk3lem1  30452  smcnlem  30768  ipval2  30778  hhph  31249  pjhthlem1  31462  golem1  32342  stcltrlem1  32347  pythagreim  32818  quad3d  32822  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  archirngz  33250  archiabllem1a  33252  archiabllem1  33254  archiabllem2c  33256  constrrtcc  33879  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpinconstrlem1  33933  ballotlemsdom  34656  fsum2dsub  34751  revwlk  35307  resconn  35428  iprodgam  35924  faclimlem1  35925  faclimlem3  35927  faclim  35928  iprodfac  35929  fwddifnp1  36347  dnibndlem7  36744  dnibndlem8  36745  knoppndvlem14  36785  bj-bary1  37626  dvtan  37991  itgaddnclem2  38000  itgmulc2nc  38009  ftc1anclem8  38021  dvasin  38025  areacirclem1  38029  lcmineqlem19  42486  aks4d1p1p2  42509  posbezout  42539  sticksstones7  42591  sticksstones12a  42596  sticksstones12  42597  bcle2d  42618  aks6d1c7lem1  42619  dffltz  43067  fltbccoprm  43074  flt4lem3  43081  flt4lem5c  43087  flt4lem5d  43088  flt4lem5e  43089  flt4lem7  43092  nna4b4nsq  43093  fltnltalem  43095  3cubeslem2  43117  3cubeslem3l  43118  3cubeslem3r  43119  pellexlem2  43258  pell14qrgt0  43287  rmxyadd  43349  rmxluc  43364  fzmaxdif  43409  acongeq  43411  jm2.19lem2  43418  jm2.26lem3  43429  areaquad  43644  sqrtcval  44068  int-addcomd  44600  int-leftdistd  44606  subadd4b  45716  sub31  45723  coseq0  46292  coskpi2  46294  cosknegpi  46297  fperdvper  46347  dvbdfbdioolem2  46357  dvnmul  46371  dvmptfprodlem  46372  itgsincmulx  46402  itgsbtaddcnst  46410  stoweidlem11  46439  stirlinglem5  46506  stirlinglem7  46508  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem4  46539  fourierdlem26  46561  fourierdlem40  46575  fourierdlem42  46577  fourierdlem47  46581  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem84  46618  fourierdlem93  46627  fourierdlem103  46637  fourierdlem111  46645  fourierswlem  46658  fouriersw  46659  etransclem32  46694  etransclem46  46708  sge0gtfsumgt  46871  hoidmv1lelem2  47020  hoidmvlelem2  47024  hspmbllem1  47054  smfmullem1  47219  sigarperm  47288  sin5tlem1  47319  sin5tlem5  47323  cjnpoly  47331  2elfz2melfz  47760  m1modmmod  47806  mod2addne  47812  fargshiftfo  47896  ichexmpl2  47924  fmtnorec3  48005  2zrngacmnd  48718  2zrngagrp  48719  ply1mulgsumlem1  48856  ackval1  49151  ackval2  49152  resum2sqorgt0  49179  eenglngeehlnmlem2  49208  rrx2linest2  49214  line2xlem  49223  itsclc0yqsollem1  49232  itsclc0yqsol  49234  itscnhlc0xyqsol  49235  itsclc0xyqsolr  49239  itsclinecirc0b  49244  itsclquadb  49246  2itscplem1  49248  2itscp  49251  onetansqsecsq  50230