Theorem addcomd 9777

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 9546	. . . . . . . . 9 |- 1 e. CC
2	1	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. CC )
3	2, 2	addcld 9611	. . . . . . 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 9616	. . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
7	4, 5	addcld 9611	. . . . . . 7 |- ( ph -> ( A + B ) e. CC )
8		1p1times 9746	. . . . . . 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 9746	. . . . . . . 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 9746	. . . . . . . 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 6300	. . . . . 6 |- ( ph -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
15	6, 9, 14	3eqtr3rd 2517	. . . . 5 |- ( ph -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
16	4, 4	addcld 9611	. . . . . 6 |- ( ph -> ( A + A ) e. CC )
17	16, 5, 5	addassd 9614	. . . . 5 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
18	7, 4, 5	addassd 9614	. . . . 5 |- ( ph -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
19	15, 17, 18	3eqtr4d 2518	. . . 4 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
20	16, 5	addcld 9611	. . . . 5 |- ( ph -> ( ( A + A ) + B ) e. CC )
21	7, 4	addcld 9611	. . . . 5 |- ( ph -> ( ( A + B ) + A ) e. CC )
22		addcan2 9760	. . . . 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 1228	. . . 4 |- ( ph -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
24	19, 23	mpbid 210	. . 3 |- ( ph -> ( ( A + A ) + B ) = ( ( A + B ) + A ) )
25	4, 4, 5	addassd 9614	. . 3 |- ( ph -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
26	4, 5, 4	addassd 9614	. . 3 |- ( ph -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
27	24, 25, 26	3eqtr3d 2516	. 2 |- ( ph -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
28	5, 4	addcld 9611	. . 3 |- ( ph -> ( B + A ) e. CC )
29		addcan 9759	. . 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 1228	. 2 |- ( ph -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
31	27, 30	mpbid 210	1 |- ( ph -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767  (class class class)co 6282   CCcc 9486   1c1 9489   + caddc 9491   x. cmul 9493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-po 4800  df-so 4801  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-pnf 9626  df-mnf 9627  df-ltxr 9629

This theorem is referenced by:  subadd2  9820  pncan  9822  npcan  9825  subcan  9870  ltadd1  10015  leadd2  10017  ltsubadd2  10019  lesubadd2  10021  ltaddrp2d  11282  lincmb01cmp  11659  iccf1o  11660  modaddabs  11998  modadd2mod  12001  modadd12d  12007  modaddmulmod  12017  expaddz  12174  bcn2m1  12366  bcn2p1  12367  addlenswrd  12621  spllen  12689  splfv2a  12691  remullem  12920  sqreulem  13151  climaddc2  13417  clim2ser2  13437  iseraltlem2  13464  telfsumo  13575  fsumparts  13579  bcxmas  13606  cosneg  13739  coshval  13747  sinadd  13756  sincossq  13768  cos2t  13770  absefi  13788  absefib  13790  sadadd2lem2  13955  bitsres  13978  bezoutlem2  14032  bezoutlem4  14034  pythagtrip  14213  pcadd2  14264  vdwapun  14347  vdwlem5  14358  vdwlem6  14359  vdwlem8  14361  gsumccat  15832  mulgnndir  15964  mulgdirlem  15966  mulgdir  15967  sylow1lem1  16414  efgcpbllemb  16569  cygabl  16684  ablfacrp  16907  icccvx  21185  pjthlem1  21587  ovolicc2lem4  21666  cmmbl  21680  voliunlem1  21695  itgmulc2  21975  dvle  22143  dvcvx  22156  dvfsumlem2  22163  dvfsumlem4  22165  dvfsum2  22170  ply1divex  22272  plymullem1  22346  coeeulem  22356  aaliou3lem6  22478  dvtaylp  22499  ulmcn  22528  abelthlem7  22567  pilem3  22582  lawcos  22876  affineequiv  22885  heron  22897  quad2  22898  dcubic1lem  22902  dcubic2  22903  dcubic  22905  mcubic  22906  quart1lem  22914  quart1  22915  asinlem2  22928  asinsin  22951  cosasin  22963  atanlogaddlem  22972  atanlogadd  22973  cvxcl  23042  scvxcvx  23043  bposlem9  23295  lgseisenlem1  23352  2sqlem3  23369  2sqblem  23380  dchrisumlem2  23403  selberg  23461  selberg2  23464  chpdifbndlem1  23466  selberg4  23474  pntrlog2bndlem1  23490  pntrlog2bndlem6  23496  pntibndlem2  23504  pntlemb  23510  pntlemf  23518  padicabv  23543  colinearalglem2  23886  axsegconlem9  23904  axpasch  23920  axeuclidlem  23941  cusgrasizeinds  24152  fargshiftfo  24314  eupath2lem3  24655  numclwlk3lem3  24750  smcnlem  25283  ipval2  25293  hhph  25771  pjhthlem1  25985  golem1  26866  stcltrlem1  26871  omndmul2  27364  archirngz  27395  archiabllem1  27399  archiabllem2c  27401  ballotlemsdom  28090  signshf  28185  lgamgulmlem2  28212  lgamgulmlem3  28213  lgamcvg2  28237  lgam1  28246  rescon  28331  rtrclreclem.trans  28544  iprodgam  28702  faclimlem1  28745  faclimlem3  28747  faclim  28748  iprodfac  28749  bpoly4  29398  supadd  29619  dvtan  29642  itg2addnclem3  29645  itgaddnclem2  29651  itgmulc2nc  29660  ftc1anclem8  29674  dvasin  29680  areacirclem1  29684  pellexlem2  30370  pell14qrgt0  30399  rmxyadd  30461  rmxluc  30476  fzmaxdif  30523  acongeq  30525  jm2.19lem2  30536  jm2.26lem3  30547  areaquad  30789  subadd4b  31041  sub31  31056  coseq0  31199  coskpi2  31202  cosknegpi  31205  fperdvper  31248  dvbdfbdioolem2  31259  itgsincmulx  31292  itgsbtaddcnst  31300  stoweidlem11  31311  stirlinglem5  31378  stirlinglem7  31380  dirkertrigeqlem1  31398  dirkertrigeqlem2  31399  dirkertrigeqlem3  31400  dirkertrigeq  31401  dirkercncflem2  31404  fourierdlem4  31411  fourierdlem40  31447  fourierdlem42  31449  fourierdlem47  31454  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem74  31481  fourierdlem75  31482  fourierdlem78  31485  fourierdlem79  31486  fourierdlem84  31491  fourierdlem93  31500  fourierdlem103  31510  fourierdlem111  31518  fourierswlem  31531  fouriersw  31532  sigarperm  31544  2elfz2melfz  31803  ply1mulgsumlem1  32059  onetansqsecsq  32236  comraddd  32257  mvlladdd  32259  mvrladdd  32262  bj-rsub  33744  bj-bary1  33753