MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcom Structured version   Visualization version   GIF version

Theorem addcom 9904
Description: Addition commutes. 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
StepHypRef Expression
1 1cnd 9744 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
21, 1addcld 9747 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 + 1) ∈ ℂ)
3 simpl 466 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
4 simpr 470 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
52, 3, 4adddid 9752 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 9747 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 9889 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 9889 . . . . . . 7 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10 1p1times 9889 . . . . . . 7 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
119, 10oveqan12d 6382 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
125, 8, 113eqtr3rd 2548 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
133, 3addcld 9747 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐴) ∈ ℂ)
1413, 4, 4addassd 9750 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
156, 3, 4addassd 9750 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1612, 14, 153eqtr4d 2549 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1713, 4addcld 9747 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
186, 3addcld 9747 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
19 addcan2 9903 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2017, 18, 4, 19syl3anc 1308 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2116, 20mpbid 217 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
223, 3, 4addassd 9750 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
233, 4, 3addassd 9750 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2421, 22, 233eqtr3d 2547 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
254, 3addcld 9747 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 𝐴) ∈ ℂ)
26 addcan 9902 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
273, 6, 25, 26syl3anc 1308 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
2824, 27mpbid 217 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wa 378   = wceq 1468  wcel 1937  (class class class)co 6363  cc 9622  1c1 9625   + caddc 9627   · cmul 9629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-mulcom 9688  ax-addass 9689  ax-mulass 9690  ax-distr 9691  ax-i2m1 9692  ax-1ne0 9693  ax-1rid 9694  ax-rnegex 9695  ax-rrecex 9696  ax-cnre 9697  ax-pre-lttri 9698  ax-pre-lttrn 9699  ax-pre-ltadd 9700
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-nel 2678  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-mpt 4495  df-id 4795  df-po 4801  df-so 4802  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-ov 6366  df-er 7440  df-en 7653  df-dom 7654  df-sdom 7655  df-pnf 9762  df-mnf 9763  df-ltxr 9765
This theorem is referenced by:  addcomi  9909  ltaddnegr  9933  add12  9934  add32  9935  add42  9938  subsub23  9967  pncan2  9969  addsub  9973  addsub12  9975  addsubeq4  9977  sub32  9995  pnpcan2  10001  ppncan  10003  sub4  10006  negsubdi2  10020  ltaddsub2  10177  leaddsub2  10179  leltadd  10186  ltaddpos2  10193  addge02  10213  conjmul  10413  recp1lt1  10593  recreclt  10594  avgle1  10942  avgle2  10943  avgle  10944  nn0nnaddcl  10992  xaddcom  11625  fzen  11912  fzshftral  11980  fzo0addelr  12072  elfzoext  12074  flzadd  12167  addmodidr  12248  modadd2mod  12249  nn0ennn  12305  seradd  12369  bernneq2  12513  hashfz  12720  ccatalpha  12867  revccat  13004  2cshwcom  13051  shftval2  13298  shftval4  13300  crim  13338  absmax  13552  climshft2  13806  summolem3  13940  binom1dif  14051  isumshft  14057  arisum  14078  mertenslem1  14100  bpolydiflem  14267  addcos  14388  demoivreALT  14415  dvdsaddr  14504  divalglem4  14537  divalgb  14547  gcdaddm  14655  hashdvds  14885  phiprmpw  14886  pythagtriplem2  14929  prmgaplem7  15189  mulgnndir  16940  cnaddablx  17667  cnaddabl  17668  zaddablx  17669  cncrng  19147  ioo2bl  21969  icopnfcnv  22128  uniioombllem3  22703  fta1glem1  23277  plyremlem  23418  fta1lem  23421  vieta1lem1  23424  vieta1lem2  23425  aaliou3lem2  23460  dvradcnv  23537  pserdv2  23546  reeff1olem  23562  ptolemy  23612  logcnlem4  23751  cxpsqrt  23809  atandm2  23964  atandm4  23966  atanlogsublem  24002  2efiatan  24005  dvatan  24022  birthdaylem2  24039  emcllem2  24083  fsumharmonic  24098  wilthlem1  24154  wilthlem2  24155  basellem8  24175  1sgmprm  24288  perfectlem2  24319  pntibndlem1  24588  pntibndlem2  24590  pntlemd  24593  pntlemc  24594  cnaddablo  26241  addinv  26243  cdj3lem3b  28256  isarchi3  28659  archiabllem2c  28667  cos2h  32169  tan2h  32170  eldioph2lem1  35842  addcomgi  37166  epoo  39350  perfectALTVlem2  39364  sgoldbaltlem2  39401  fz0addcom  39579  eucrctshift  40811
  Copyright terms: Public domain W3C validator