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

Theorem mulid2 9894
Description: Identity law for multiplication. Note: see mulid1 9893 for commuted version. (Contributed by NM, 8-Oct-1999.)
Assertion
Ref Expression
mulid2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2
StepHypRef Expression
1 ax-1cn 9850 . . 3 1 ∈ ℂ
2 mulcom 9878 . . 3 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
31, 2mpan 701 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4 mulid1 9893 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
53, 4eqtrd 2643 1 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9790  1c1 9793   · cmul 9797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-mulcl 9854  ax-mulcom 9856  ax-mulass 9858  ax-distr 9859  ax-1rid 9862  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  mulid2i  9899  mulid2d  9914  muladd11  10057  1p1times  10058  mul02lem1  10063  cnegex2  10069  mulm1  10322  div1  10565  recdiv  10580  divdiv2  10586  conjmul  10591  ser1const  12674  expp1  12684  recan  13870  arisum  14377  geo2sum  14389  prodrblem  14444  prodmolem2a  14449  risefac1  14549  fallfac1  14550  bpoly3  14574  bpoly4  14575  sinhval  14669  coshval  14670  demoivreALT  14716  gcdadd  15031  gcdid  15032  cncrng  19532  cnfld1  19536  cnfldmulg  19543  blcvx  22341  icccvx  22488  cnlmod  22677  coeidp  23740  dgrid  23741  quartlem1  24301  asinsinlem  24335  asinsin  24336  atantan  24367  musumsum  24635  brbtwn2  25503  axsegconlem1  25515  ax5seglem1  25526  ax5seglem2  25527  ax5seglem4  25530  ax5seglem5  25531  axeuclid  25561  axcontlem2  25563  axcontlem4  25565  cncvcOLD  26606  subdivcomb2  30671  dvcosax  38620
  Copyright terms: Public domain W3C validator