Theorem addcom 11397

Description: Addition is commutative. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
addcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcom

Step	Hyp	Ref	Expression
1		1cnd 11203	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
2	1, 1	addcld 11229	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 + 1) ∈ ℂ)
3		simpl 487	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
4		simpr 489	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11234	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11229	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11382	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11382	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10		1p1times 11382	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
11	9, 10	oveqan12d 7431	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
12	5, 8, 11	3eqtr3rd 2807	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
13	3, 3	addcld 11229	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐴) ∈ ℂ)
14	13, 4, 4	addassd 11232	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
15	6, 3, 4	addassd 11232	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
16	12, 14, 15	3eqtr4d 2808	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
17	13, 4	addcld 11229	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
18	6, 3	addcld 11229	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
19		addcan2 11396	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
20	17, 18, 4, 19	syl3anc 1398	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
21	16, 20	mpbid 235	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
22	3, 3, 4	addassd 11232	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
23	3, 4, 3	addassd 11232	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
24	21, 22, 23	3eqtr3d 2806	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
25	4, 3	addcld 11229	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) ∈ ℂ)
26		addcan 11395	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
27	3, 6, 25, 26	syl3anc 1398	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
28	24, 27	mpbid 235	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   + caddc 11104   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  addcomi  11402  ltaddnegr  11428  add12  11429  add32  11430  add42  11433  subsub23  11463  pncan2  11465  addsub  11469  addsub12  11471  addsubeq4  11473  sub32  11493  pnpcan2  11499  ppncan  11501  sub4  11504  negsubdi2  11518  ltaddsub2  11690  leaddsub2  11692  leltadd  11699  ltaddpos2  11706  addge02  11726  conjmul  11933  recp1lt1  12114  recreclt  12115  avgle1  12485  avgle2  12486  avgle  12487  nn0nnaddcl  12536  xaddcom  13267  fzen  13570  fzshftral  13645  fzo0addelr  13750  flzadd  13861  addmodidr  13958  modadd2mod  13959  nn0ennn  14017  seradd  14082  bernneq2  14268  ccatrn  14629  ccatalpha  14633  revccat  14805  2cshwcom  14855  shftval2  15114  shftval4  15116  crim  15168  absmax  15383  climshft2  15635  summolem3  15767  binom1dif  15889  isumshft  15895  arisum  15916  mertenslem1  15940  bpolydiflem  16109  addcos  16231  demoivreALT  16258  dvdsaddr  16362  sumodd  16447  divalglem4  16455  divalgb  16463  gcdaddm  16584  hashdvds  16835  phiprmpw  16836  pythagtriplem2  16878  prmgaplem7  17118  mulgnndir  19170  cnaddablx  19939  cnaddabl  19940  zaddablx  19943  psdmvr  22313  ioo2bl  24931  icopnfcnv  25082  uniioombllem3  25725  fta1glem1  26306  plyremlem  26446  fta1lem  26449  vieta1lem1  26452  vieta1lem2  26453  aaliou3lem2  26485  dvradcnv  26562  pserdv2  26571  reeff1olem  26587  ptolemy  26639  logcnlem4  26788  cxpsqrt  26846  atandm2  27020  atandm4  27022  atanlogsublem  27058  2efiatan  27061  dvatan  27078  birthdaylem2  27095  emcllem2  27139  fsumharmonic  27154  wilthlem1  27210  wilthlem2  27211  basellem8  27230  1sgmprm  27341  perfectlem2  27372  pntibndlem1  27731  pntibndlem2  27733  pntlemd  27736  pntlemc  27737  eucrctshift  30572  cnaddabloOLD  30911  cdj3lem3b  32770  isarchi3  33485  archiabllem2c  33493  cos2h  38240  tan2h  38241  lcmineqlem4  42777  eldioph2lem1  43471  addcomgi  45144  fz0addcom  48031  epoo  48445  perfectALTVlem2  48464  sbgoldbaltlem2  48522