Theorem addcomd 9576

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 9345	. . . . . . . . 9 |- 1 e. CC
2	1	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. CC )
3	2, 2	addcld 9410	. . . . . . 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 9415	. . . . . 6 |- ( ph -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
7	4, 5	addcld 9410	. . . . . . 7 |- ( ph -> ( A + B ) e. CC )
8		1p1times 9545	. . . . . . 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 9545	. . . . . . . 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 9545	. . . . . . . 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 6114	. . . . . 6 |- ( ph -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
15	6, 9, 14	3eqtr3rd 2484	. . . . 5 |- ( ph -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
16	4, 4	addcld 9410	. . . . . 6 |- ( ph -> ( A + A ) e. CC )
17	16, 5, 5	addassd 9413	. . . . 5 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
18	7, 4, 5	addassd 9413	. . . . 5 |- ( ph -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
19	15, 17, 18	3eqtr4d 2485	. . . 4 |- ( ph -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
20	16, 5	addcld 9410	. . . . 5 |- ( ph -> ( ( A + A ) + B ) e. CC )
21	7, 4	addcld 9410	. . . . 5 |- ( ph -> ( ( A + B ) + A ) e. CC )
22		addcan2 9559	. . . . 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 1218	. . . 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 9413	. . 3 |- ( ph -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
26	4, 5, 4	addassd 9413	. . 3 |- ( ph -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
27	24, 25, 26	3eqtr3d 2483	. 2 |- ( ph -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
28	5, 4	addcld 9410	. . 3 |- ( ph -> ( B + A ) e. CC )
29		addcan 9558	. . 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 1218	. 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 1369   e. wcel 1756  (class class class)co 6096   CCcc 9285   1c1 9288   + caddc 9290   x. cmul 9292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-po 4646  df-so 4647  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-ov 6099  df-er 7106  df-en 7316  df-dom 7317  df-sdom 7318  df-pnf 9425  df-mnf 9426  df-ltxr 9428

This theorem is referenced by:  subadd2  9619  pncan  9621  npcan  9624  subcan  9669  ltadd1  9811  leadd2  9813  ltsubadd2  9815  lesubadd2  9817  ltaddrp2d  11062  lincmb01cmp  11433  iccf1o  11434  modaddabs  11751  modadd2mod  11754  modadd12d  11760  modaddmulmod  11770  expaddz  11913  bcn2m1  12105  bcn2p1  12106  addlenswrd  12336  spllen  12401  splfv2a  12403  remullem  12622  sqreulem  12852  climaddc2  13118  clim2ser2  13138  iseraltlem2  13165  fsumtscopo  13270  fsumparts  13274  bcxmas  13303  cosneg  13436  coshval  13444  sinadd  13453  sincossq  13465  cos2t  13467  absefi  13485  absefib  13487  sadadd2lem2  13651  bitsres  13674  bezoutlem2  13728  bezoutlem4  13730  pythagtrip  13906  pcadd2  13957  vdwapun  14040  vdwlem5  14051  vdwlem6  14052  vdwlem8  14054  gsumccat  15524  mulgnndir  15654  mulgdirlem  15656  mulgdir  15657  sylow1lem1  16102  efgcpbllemb  16257  cygabl  16372  ablfacrp  16572  icccvx  20527  pjthlem1  20929  ovolicc2lem4  21008  cmmbl  21021  voliunlem1  21036  itgmulc2  21316  dvle  21484  dvcvx  21497  dvfsumlem2  21504  dvfsumlem4  21506  dvfsum2  21511  ply1divex  21613  plymullem1  21687  coeeulem  21697  aaliou3lem6  21819  dvtaylp  21840  ulmcn  21869  abelthlem7  21908  pilem3  21923  lawcos  22217  affineequiv  22226  heron  22238  quad2  22239  dcubic1lem  22243  dcubic2  22244  dcubic  22246  mcubic  22247  quart1lem  22255  quart1  22256  asinlem2  22269  asinsin  22292  cosasin  22304  atanlogaddlem  22313  atanlogadd  22314  cvxcl  22383  scvxcvx  22384  bposlem9  22636  lgseisenlem1  22693  2sqlem3  22710  2sqblem  22721  dchrisumlem2  22744  selberg  22802  selberg2  22805  chpdifbndlem1  22807  selberg4  22815  pntrlog2bndlem1  22831  pntrlog2bndlem6  22837  pntibndlem2  22845  pntlemb  22851  pntlemf  22859  padicabv  22884  colinearalglem2  23158  axsegconlem9  23176  axpasch  23192  axeuclidlem  23213  cusgrasizeinds  23389  fargshiftfo  23529  eupath2lem3  23605  smcnlem  24097  ipval2  24107  hhph  24585  pjhthlem1  24799  golem1  25680  stcltrlem1  25685  omndmul2  26180  archirngz  26211  archiabllem1  26215  archiabllem2c  26217  ballotlemsdom  26899  signshf  26994  lgamgulmlem2  27021  lgamgulmlem3  27022  lgamcvg2  27046  lgam1  27055  rescon  27140  rtrclreclem.trans  27353  iprodgam  27511  faclimlem1  27554  faclimlem3  27556  faclim  27557  iprodfac  27558  bpoly4  28207  supadd  28423  dvtan  28447  itg2addnclem3  28450  itgaddnclem2  28456  itgmulc2nc  28465  ftc1anclem8  28479  dvasin  28485  areacirclem1  28489  pellexlem2  29176  pell14qrgt0  29205  rmxyadd  29267  rmxluc  29282  fzmaxdif  29329  acongeq  29331  jm2.19lem2  29344  jm2.26lem3  29355  areaquad  29597  stoweidlem11  29811  stirlinglem5  29878  stirlinglem7  29880  sigarperm  29901  2elfz2melfz  30207  numclwlk3lem3  30671  ply1mulgsumlem1  30849  onetansqsecsq  31101  comraddd  31118  mvlladdd  31120  mvrladdd  31123  bj-rsub  32597  bj-bary1  32606