Theorem addcomd 11438

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 11231	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11255	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11260	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11255	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11407	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11407	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11407	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7432	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2776	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11255	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11258	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11258	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2777	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11255	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11255	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11421	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1369	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11258	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11258	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2775	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11255	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11420	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1369	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128  1c1 11131   + caddc 11133   · cmul 11135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275

This theorem is referenced by:  muladd11r  11449  comraddd  11450  subadd2  11486  pncan  11488  npcan  11491  subcan  11537  mvlladdd  11647  subaddeqd  11651  addrsub  11653  mulsubaddmulsub  11700  ltadd1  11703  leadd2  11705  ltsubadd2  11707  lesubadd2  11709  lesub3d  11854  supadd  12204  ltaddrp2d  13074  lincmb01cmp  13496  iccf1o  13497  modaddabs  13898  muladdmodid  13900  negmod  13905  modadd2mod  13910  modadd12d  13916  modaddmulmod  13927  addmodlteq  13935  expaddz  14095  bcn2m1  14307  bcn2p1  14308  spllen  14728  splfv2a  14730  relexpaddnn  15022  relexpaddg  15024  rtrclreclem3  15031  remullem  15099  sqreulem  15330  bhmafibid2  15437  climaddc2  15604  iseraltlem2  15653  fsumsplit1  15715  telfsumo  15772  fsumparts  15776  bcxmas  15805  bpoly4  16027  sinadd  16132  sincossq  16144  cos2t  16146  absefi  16164  dvdsaddre2b  16275  pwp1fsum  16359  sadadd2lem2  16416  bitsres  16439  bezoutlem2  16507  bezoutlem4  16509  pythagtrip  16794  pcadd2  16850  vdwapun  16934  vdwlem5  16945  vdwlem6  16946  vdwlem8  16948  gsumsgrpccat  18783  mulgnndir  19049  mulgdirlem  19051  cyccom  19149  efgcpbllemb  19701  ablfacrp  20014  cncrng  21303  rzgrp  21542  icccvx  24862  cnlmod  25054  cphipval  25158  pjthlem1  25352  cmmbl  25450  voliunlem1  25466  dvle  25927  dvcvx  25940  dvfsumlem2  25948  dvfsumlem2OLD  25949  dvfsumlem4  25951  dvfsum2  25956  ply1divex  26059  plymullem1  26135  coeeulem  26145  aaliou3lem6  26270  dvtaylp  26292  ulmcn  26322  abelthlem7  26362  pilem3  26377  lawcos  26735  affineequiv  26742  affineequiv3  26744  heron  26757  dcubic1lem  26762  dcubic2  26763  dcubic  26765  mcubic  26766  quart1lem  26774  quart1  26775  asinlem2  26788  asinsin  26811  cosasin  26823  atanlogaddlem  26832  atanlogadd  26833  cvxcl  26904  lgamgulmlem2  26949  lgamcvg2  26974  lgam1  26983  bposlem9  27212  lgseisenlem1  27295  2sqlem3  27340  2sqblem  27351  2sqmod  27356  addsqn2reu  27361  2sqreulem1  27366  2sqreunnlem1  27369  dchrisumlem2  27410  selberg  27468  selberg2  27471  selberg4  27481  pntrlog2bndlem1  27497  pntlemb  27517  pntlemf  27525  padicabv  27550  colinearalglem2  28705  axsegconlem9  28723  axeuclidlem  28760  eupth2lem3lem3  30027  numclwwlk3lem1  30179  smcnlem  30494  ipval2  30504  hhph  30975  pjhthlem1  31188  golem1  32068  stcltrlem1  32073  omndmul2  32770  cycpmco2lem3  32827  cycpmco2lem4  32828  cycpmco2lem5  32829  cycpmco2lem6  32830  cycpmco2  32832  archirngz  32875  archiabllem1a  32877  archiabllem1  32879  archiabllem2c  32881  ballotlemsdom  34067  fsum2dsub  34175  revwlk  34670  resconn  34792  iprodgam  35272  faclimlem1  35273  faclimlem3  35275  faclim  35276  iprodfac  35277  fwddifnp1  35697  dnibndlem7  35895  dnibndlem8  35896  knoppndvlem14  35936  bj-bary1  36727  dvtan  37078  itgaddnclem2  37087  itgmulc2nc  37096  ftc1anclem8  37108  dvasin  37112  areacirclem1  37116  lcmineqlem19  41455  aks4d1p1p2  41478  posbezout  41507  sticksstones7  41556  sticksstones12a  41561  sticksstones12  41562  metakunt15  41591  metakunt16  41592  dffltz  41980  fltbccoprm  41987  flt4lem3  41994  flt4lem5c  42000  flt4lem5d  42001  flt4lem5e  42002  flt4lem7  42005  nna4b4nsq  42006  fltnltalem  42008  3cubeslem2  42027  3cubeslem3l  42028  3cubeslem3r  42029  pellexlem2  42172  pell14qrgt0  42201  rmxyadd  42264  rmxluc  42279  fzmaxdif  42324  acongeq  42326  jm2.19lem2  42333  jm2.26lem3  42344  areaquad  42567  sqrtcval  42994  int-addcomd  43526  int-leftdistd  43532  subadd4b  44587  sub31  44595  coseq0  45175  coskpi2  45177  cosknegpi  45180  fperdvper  45230  dvbdfbdioolem2  45240  dvnmul  45254  dvmptfprodlem  45255  itgsincmulx  45285  itgsbtaddcnst  45293  stoweidlem11  45322  stirlinglem5  45389  stirlinglem7  45391  dirkertrigeqlem1  45409  dirkertrigeqlem2  45410  dirkertrigeqlem3  45411  dirkertrigeq  45412  dirkercncflem2  45415  fourierdlem4  45422  fourierdlem26  45444  fourierdlem40  45458  fourierdlem42  45460  fourierdlem47  45464  fourierdlem63  45480  fourierdlem64  45481  fourierdlem65  45482  fourierdlem74  45491  fourierdlem75  45492  fourierdlem78  45495  fourierdlem79  45496  fourierdlem84  45501  fourierdlem93  45510  fourierdlem103  45520  fourierdlem111  45528  fourierswlem  45541  fouriersw  45542  etransclem32  45577  etransclem46  45591  sge0gtfsumgt  45754  hoidmv1lelem2  45903  hoidmvlelem2  45907  hspmbllem1  45937  smfmullem1  46102  sigarperm  46171  2elfz2melfz  46621  fargshiftfo  46705  ichexmpl2  46733  fmtnorec3  46811  2zrngacmnd  47233  2zrngagrp  47234  ply1mulgsumlem1  47377  m1modmmod  47517  ackval1  47677  ackval2  47678  resum2sqorgt0  47705  eenglngeehlnmlem2  47734  rrx2linest2  47740  line2xlem  47749  itsclc0yqsollem1  47758  itsclc0yqsol  47760  itscnhlc0xyqsol  47761  itsclc0xyqsolr  47765  itsclinecirc0b  47770  itsclquadb  47772  2itscplem1  47774  2itscp  47777  onetansqsecsq  48115