Theorem addcomd 9558

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 9327	. . . . . . . . 9 |- 1 e. CC
2	1	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. CC )
3	2, 2	addcld 9392	. . . . . . 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 9397	. . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
7	4, 5	addcld 9392	. . . . . . 7 |- ( ph -> ( A + B ) e. CC )
8		1p1times 9527	. . . . . . 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 9527	. . . . . . . 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 9527	. . . . . . . 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 6098	. . . . . 6 |- ( ph -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
15	6, 9, 14	3eqtr3rd 2474	. . . . 5 |- ( ph -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
16	4, 4	addcld 9392	. . . . . 6 |- ( ph -> ( A + A ) e. CC )
17	16, 5, 5	addassd 9395	. . . . 5 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
18	7, 4, 5	addassd 9395	. . . . 5 |- ( ph -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
19	15, 17, 18	3eqtr4d 2475	. . . 4 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
20	16, 5	addcld 9392	. . . . 5 |- ( ph -> ( ( A + A ) + B ) e. CC )
21	7, 4	addcld 9392	. . . . 5 |- ( ph -> ( ( A + B ) + A ) e. CC )
22		addcan2 9541	. . . . 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 1211	. . . 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 9395	. . 3 |- ( ph -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
26	4, 5, 4	addassd 9395	. . 3 |- ( ph -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
27	24, 25, 26	3eqtr3d 2473	. 2 |- ( ph -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
28	5, 4	addcld 9392	. . 3 |- ( ph -> ( B + A ) e. CC )
29		addcan 9540	. . 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 1211	. 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 1362   e. wcel 1755  (class class class)co 6080   CCcc 9267   1c1 9270   + caddc 9272   x. cmul 9274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-po 4628  df-so 4629  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9407  df-mnf 9408  df-ltxr 9410

This theorem is referenced by:  subadd2  9601  pncan  9603  npcan  9606  subcan  9651  ltadd1  9793  leadd2  9795  ltsubadd2  9797  lesubadd2  9799  ltaddrp2d  11044  lincmb01cmp  11414  iccf1o  11415  modaddabs  11729  modadd2mod  11732  modadd12d  11738  modaddmulmod  11748  expaddz  11891  bcn2m1  12083  bcn2p1  12084  addlenswrd  12314  spllen  12379  splfv2a  12381  remullem  12600  sqreulem  12830  climaddc2  13096  clim2ser2  13116  iseraltlem2  13143  fsumtscopo  13247  fsumparts  13251  bcxmas  13280  cosneg  13413  coshval  13421  sinadd  13430  sincossq  13442  cos2t  13444  absefi  13462  absefib  13464  sadadd2lem2  13628  bitsres  13651  bezoutlem2  13705  bezoutlem4  13707  pythagtrip  13883  pcadd2  13934  vdwapun  14017  vdwlem5  14028  vdwlem6  14029  vdwlem8  14031  gsumccat  15498  mulgnndir  15628  mulgdirlem  15630  mulgdir  15631  sylow1lem1  16076  efgcpbllemb  16231  cygabl  16346  ablfacrp  16540  icccvx  20363  pjthlem1  20765  ovolicc2lem4  20844  cmmbl  20857  voliunlem1  20872  itgmulc2  21152  dvle  21320  dvcvx  21333  dvfsumlem2  21340  dvfsumlem4  21342  dvfsum2  21347  ply1divex  21492  plymullem1  21566  coeeulem  21576  aaliou3lem6  21698  dvtaylp  21719  ulmcn  21748  abelthlem7  21787  pilem3  21802  lawcos  22096  affineequiv  22105  heron  22117  quad2  22118  dcubic1lem  22122  dcubic2  22123  dcubic  22125  mcubic  22126  quart1lem  22134  quart1  22135  asinlem2  22148  asinsin  22171  cosasin  22183  atanlogaddlem  22192  atanlogadd  22193  cvxcl  22262  scvxcvx  22263  bposlem9  22515  lgseisenlem1  22572  2sqlem3  22589  2sqblem  22600  dchrisumlem2  22623  selberg  22681  selberg2  22684  chpdifbndlem1  22686  selberg4  22694  pntrlog2bndlem1  22710  pntrlog2bndlem6  22716  pntibndlem2  22724  pntlemb  22730  pntlemf  22738  padicabv  22763  colinearalglem2  22975  axsegconlem9  22993  axpasch  23009  axeuclidlem  23030  cusgrasizeinds  23206  fargshiftfo  23346  eupath2lem3  23422  smcnlem  23914  ipval2  23924  hhph  24402  pjhthlem1  24616  golem1  25497  stcltrlem1  25502  omndmul2  25998  archirngz  26029  archiabllem1  26033  archiabllem2c  26035  ballotlemsdom  26741  signshf  26836  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamcvg2  26888  lgam1  26897  rescon  26982  rtrclreclem.trans  27194  iprodgam  27352  faclimlem1  27395  faclimlem3  27397  faclim  27398  iprodfac  27399  bpoly4  28048  supadd  28259  dvtan  28283  itg2addnclem3  28286  itgaddnclem2  28292  itgmulc2nc  28301  ftc1anclem8  28315  dvasin  28321  areacirclem1  28325  pellexlem2  29013  pell14qrgt0  29042  rmxyadd  29104  rmxluc  29119  fzmaxdif  29166  acongeq  29168  jm2.19lem2  29181  jm2.26lem3  29192  areaquad  29434  stoweidlem11  29649  stirlinglem5  29716  stirlinglem7  29718  sigarperm  29739  2elfz2melfz  30045  numclwlk3lem3  30509  onetansqsecsq  30802  comraddd  30819  mvlladdd  30821  mvrladdd  30824  bj-rsub  32164  bj-bary1  32173