Theorem addcomd 11411

Description: Addition is commutative. 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 11201	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11227	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11232	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11227	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11380	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11380	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11380	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7428	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2805	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11227	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11230	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11230	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2806	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11227	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11227	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11394	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1396	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11230	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11230	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2804	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11227	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11393	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1396	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097  1c1 11100   + caddc 11102   · cmul 11104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247

This theorem is referenced by:  muladd11r  11422  comraddd  11423  subadd2  11460  pncan  11462  npcan  11465  subcan  11512  mvlladdd  11624  subaddeqd  11628  addrsub  11630  mulsubaddmulsub  11677  ltadd1  11680  leadd2  11682  ltsubadd2  11684  lesubadd2  11686  lesub3d  11831  supadd  12182  ltaddrp2d  13093  lincmb01cmp  13521  iccf1o  13522  elfzoext  13750  modaddabs  13943  muladdmodid  13945  negmod  13951  modadd2mod  13956  modadd12d  13962  modaddmulmod  13973  addmodlteq  13981  expaddz  14141  bcn2m1  14359  bcn2p1  14360  lenrevpfxcctswrd  14748  spllen  14790  splfv2a  14792  relexpaddnn  15087  relexpaddg  15089  rtrclreclem3  15096  remullem  15178  sqreulem  15410  bhmafibid2  15519  climaddc2  15686  iseraltlem2  15733  fsumsplit1  15795  telfsumo  15853  fsumparts  15857  bcxmas  15888  bpoly4  16112  sinadd  16219  sincossq  16231  cos2t  16233  absefi  16251  dvdsaddre2b  16364  pwp1fsum  16448  sadadd2lem2  16507  bitsres  16530  bezoutlem2  16597  bezoutlem4  16599  pythagtrip  16893  pcadd2  16949  vdwapun  17033  vdwlem5  17044  vdwlem6  17045  vdwlem8  17047  gsumsgrpccat  18898  mulgnndir  19168  mulgdirlem  19170  cyccom  19273  efgcpbllemb  19824  ablfacrp  20137  omndmul2  20202  cncrng  21522  rzgrp  21752  icccvx  25088  cnlmod  25278  cphipval  25381  pjthlem1  25575  cmmbl  25672  voliunlem1  25688  dvle  26145  dvcvx  26158  dvfsumlem2  26165  dvfsumlem4  26167  dvfsum2  26172  ply1divex  26273  plymullem1  26350  coeeulem  26360  aaliou3lem6  26488  dvtaylp  26509  ulmcn  26538  abelthlem7  26577  pilem3  26592  lawcos  26957  affineequiv  26964  affineequiv3  26966  heron  26979  dcubic1lem  26984  dcubic2  26985  dcubic  26987  mcubic  26988  quart1lem  26996  quart1  26997  asinlem2  27010  asinsin  27033  cosasin  27045  atanlogaddlem  27054  atanlogadd  27055  cvxcl  27125  lgamgulmlem2  27170  lgamcvg2  27195  lgam1  27204  bposlem9  27432  lgseisenlem1  27515  2sqlem3  27560  2sqblem  27571  2sqmod  27576  addsqn2reu  27581  2sqreulem1  27586  2sqreunnlem1  27589  dchrisumlem2  27630  selberg  27688  selberg2  27691  selberg4  27701  pntrlog2bndlem1  27717  pntlemb  27737  pntlemf  27745  padicabv  27770  colinearalglem2  29223  axsegconlem9  29241  axeuclidlem  29278  eupth2lem3lem3  30547  numclwwlk3lem1  30699  smcnlem  31015  ipval2  31025  hhph  31496  pjhthlem1  31709  golem1  32589  stcltrlem1  32594  pythagreim  33056  quad3d  33060  cycpmco2lem3  33414  cycpmco2lem4  33415  cycpmco2lem5  33416  cycpmco2lem6  33417  cycpmco2  33419  archirngz  33475  archiabllem1a  33477  archiabllem1  33479  archiabllem2c  33481  constrrtcc  34091  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  cos9thpiminplylem3  34140  cos9thpinconstrlem1  34145  ballotlemsdom  34868  fsum2dsub  34960  revwlk  35571  resconn  35692  iprodgam  36188  faclimlem1  36189  faclimlem3  36191  faclim  36192  iprodfac  36193  fwddifnp1  36611  dnibndlem7  37017  dnibndlem8  37018  knoppndvlem14  37058  bj-bary1  37900  dvtan  38265  itgaddnclem2  38274  itgmulc2nc  38283  ftc1anclem8  38295  dvasin  38299  areacirclem1  38303  lcmineqlem19  42760  aks4d1p1p2  42783  posbezout  42813  sticksstones7  42865  sticksstones12a  42870  sticksstones12  42871  bcle2d  42892  aks6d1c7lem1  42893  quadfac  42918  dffltz  43314  fltbccoprm  43321  flt4lem3  43328  flt4lem5c  43334  flt4lem5d  43335  flt4lem5e  43336  flt4lem7  43339  nna4b4nsq  43340  fltnltalem  43342  3cubeslem2  43364  3cubeslem3l  43365  3cubeslem3r  43366  pellexlem2  43505  pell14qrgt0  43534  rmxyadd  43596  rmxluc  43611  fzmaxdif  43656  acongeq  43658  jm2.19lem2  43665  jm2.26lem3  43676  areaquad  43891  sqrtcval  44315  int-addcomd  44847  int-leftdistd  44853  subadd4b  45950  sub31  45957  coseq0  46526  coskpi2  46528  cosknegpi  46531  fperdvper  46581  dvbdfbdioolem2  46591  dvnmul  46605  dvmptfprodlem  46606  itgsincmulx  46636  itgsbtaddcnst  46644  stoweidlem11  46673  stirlinglem5  46740  stirlinglem7  46742  dirkertrigeqlem1  46760  dirkertrigeqlem2  46761  dirkertrigeqlem3  46762  dirkertrigeq  46763  dirkercncflem2  46766  fourierdlem4  46773  fourierdlem26  46795  fourierdlem40  46809  fourierdlem42  46811  fourierdlem47  46815  fourierdlem63  46831  fourierdlem64  46832  fourierdlem65  46833  fourierdlem74  46842  fourierdlem75  46843  fourierdlem78  46846  fourierdlem79  46847  fourierdlem84  46852  fourierdlem93  46861  fourierdlem103  46871  fourierdlem111  46879  fourierswlem  46892  fouriersw  46893  etransclem32  46928  etransclem46  46942  sge0gtfsumgt  47105  hoidmv1lelem2  47254  hoidmvlelem2  47258  hspmbllem1  47288  smfmullem1  47453  sigarperm  47522  sin5tlem1  47555  sin5tlem5  47559  cjnpoly  47571  2elfz2melfz  48000  m1modmmod  48046  mod2addne  48052  fargshiftfo  48136  ichexmpl2  48164  fmtnorec3  48245  2zrngacmnd  48958  2zrngagrp  48959  ply1mulgsumlem1  49111  ackval1  49406  ackval2  49407  resum2sqorgt0  49434  eenglngeehlnmlem2  49463  rrx2linest2  49469  line2xlem  49478  itsclc0yqsollem1  49487  itsclc0yqsol  49489  itscnhlc0xyqsol  49490  itsclc0xyqsolr  49494  itsclinecirc0b  49499  itsclquadb  49501  2itscplem1  49503  2itscp  49506  onetansqsecsq  50484