Theorem addcomd 9224

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	|- ( ph -> A e. CC )
addcomd.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
addcomd	|- ( ph -> ( A + B ) = ( B + A ) )

Proof of Theorem addcomd

Step	Hyp	Ref	Expression
1		ax-1cn 9004	. . . . . . . . 9 |- 1 e. CC
2	1	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. CC )
3	2, 2	addcld 9063	. . . . . . 7 |- ( ph -> ( 1 + 1 ) e. CC )
4		muld.1	. . . . . . 7 |- ( ph -> A e. CC )
5		addcomd.2	. . . . . . 7 |- ( ph -> B e. CC )
6	3, 4, 5	adddid 9068	. . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
7	4, 5	addcld 9063	. . . . . . 7 |- ( ph -> ( A + B ) e. CC )
8		1p1times 9193	. . . . . . 7 |- ( ( A + B ) e. CC -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
9	7, 8	syl 16	. . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
10		1p1times 9193	. . . . . . . 8 |- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
11	4, 10	syl 16	. . . . . . 7 |- ( ph -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
12		1p1times 9193	. . . . . . . 8 |- ( B e. CC -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
13	5, 12	syl 16	. . . . . . 7 |- ( ph -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
14	11, 13	oveq12d 6058	. . . . . 6 |- ( ph -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
15	6, 9, 14	3eqtr3rd 2445	. . . . 5 |- ( ph -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
16	4, 4	addcld 9063	. . . . . 6 |- ( ph -> ( A + A ) e. CC )
17	16, 5, 5	addassd 9066	. . . . 5 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
18	7, 4, 5	addassd 9066	. . . . 5 |- ( ph -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
19	15, 17, 18	3eqtr4d 2446	. . . 4 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
20	16, 5	addcld 9063	. . . . 5 |- ( ph -> ( ( A + A ) + B ) e. CC )
21	7, 4	addcld 9063	. . . . 5 |- ( ph -> ( ( A + B ) + A ) e. CC )
22		addcan2 9207	. . . . 5 |- ( ( ( ( A + A ) + B ) e. CC /\ ( ( A + B ) + A ) e. CC /\ B e. CC ) -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
23	20, 21, 5, 22	syl3anc 1184	. . . 4 |- ( ph -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
24	19, 23	mpbid 202	. . 3 |- ( ph -> ( ( A + A ) + B ) = ( ( A + B ) + A ) )
25	4, 4, 5	addassd 9066	. . 3 |- ( ph -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
26	4, 5, 4	addassd 9066	. . 3 |- ( ph -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
27	24, 25, 26	3eqtr3d 2444	. 2 |- ( ph -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
28	5, 4	addcld 9063	. . 3 |- ( ph -> ( B + A ) e. CC )
29		addcan 9206	. . 3 |- ( ( A e. CC /\ ( A + B ) e. CC /\ ( B + A ) e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
30	4, 7, 28, 29	syl3anc 1184	. 2 |- ( ph -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
31	27, 30	mpbid 202	1 |- ( ph -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721  (class class class)co 6040   CCcc 8944   1c1 8947   + caddc 8949   x. cmul 8951

This theorem is referenced by:  subadd2  9265  pncan  9267  npcan  9270  subcan  9312  ltadd1  9451  leadd2  9453  ltsubadd2  9455  lesubadd2  9457  ltaddrp2d  10634  lincmb01cmp  10994  iccf1o  10995  modadd12d  11237  expaddz  11379  bcn2m1  11570  bcn2p1  11571  spllen  11738  splfv2a  11740  remullem  11888  sqreulem  12118  climaddc2  12384  clim2ser2  12404  iseraltlem2  12431  fsumtscopo  12536  fsumparts  12540  bcxmas  12570  cosneg  12703  coshval  12711  sinadd  12720  sincossq  12732  cos2t  12734  absefi  12752  absefib  12754  sadadd2lem2  12917  bitsres  12940  bezoutlem2  12994  bezoutlem4  12996  pythagtrip  13163  pcadd2  13214  vdwapun  13297  vdwlem5  13308  vdwlem6  13309  vdwlem8  13311  gsumccat  14742  mulgnndir  14867  mulgdirlem  14869  mulgdir  14870  sylow1lem1  15187  efgcpbllemb  15342  cygabl  15455  ablfacrp  15579  icccvx  18928  pjthlem1  19291  ovolicc2lem4  19369  cmmbl  19382  voliunlem1  19397  itgmulc2  19678  dvle  19844  dvcvx  19857  dvfsumlem2  19864  dvfsumlem4  19866  dvfsum2  19871  ply1divex  20012  plymullem1  20086  coeeulem  20096  aaliou3lem6  20218  dvtaylp  20239  ulmcn  20268  abelthlem7  20307  pilem3  20322  lawcos  20611  affineequiv  20620  quad2  20632  dcubic1lem  20636  dcubic2  20637  dcubic  20639  mcubic  20640  quart1lem  20648  quart1  20649  asinlem2  20662  asinsin  20685  cosasin  20697  atanlogaddlem  20706  atanlogadd  20707  cvxcl  20776  scvxcvx  20777  bposlem9  21029  lgseisenlem1  21086  2sqlem3  21103  2sqblem  21114  dchrisumlem2  21137  selberg  21195  selberg2  21198  chpdifbndlem1  21200  selberg4  21208  pntrlog2bndlem1  21224  pntrlog2bndlem6  21230  pntibndlem2  21238  pntlemb  21244  pntlemf  21252  padicabv  21277  cusgrasizeinds  21438  fargshiftfo  21578  eupath2lem3  21654  smcnlem  22146  ipval2  22156  hhph  22633  pjhthlem1  22846  golem1  23727  stcltrlem1  23732  ballotlemsdom  24722  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamcvg2  24792  lgam1  24801  rescon  24886  modaddabs  25068  rtrclreclem.trans  25099  iprodgam  25272  faclimlem1  25310  faclimlem3  25312  faclim  25313  iprodfac  25314  colinearalglem2  25750  axsegconlem9  25768  axpasch  25784  axeuclidlem  25805  bpoly4  26009  supadd  26138  itg2addnclem3  26157  itgaddnclem2  26163  itgmulc2nc  26172  dvreasin  26179  areacirclem2  26181  pellexlem2  26783  pell14qrgt0  26812  rmxyadd  26874  rmxluc  26889  fzmaxdif  26936  acongeq  26938  jm2.19lem2  26951  jm2.26lem3  26962  stoweidlem11  27627  stirlinglem5  27694  stirlinglem7  27696  sigarperm  27717  ubmelm1fzo  27987  onetansqsecsq  28218

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-po 4463  df-so 4464  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-ltxr 9081