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

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

Proof of Theorem mulid2
StepHypRef Expression
1 ax-1cn 10282 . . 3 1 ∈ ℂ
2 mulcom 10310 . . 3 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
31, 2mpan 673 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4 mulid1 10326 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
53, 4eqtrd 2847 1 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157  (class class class)co 6877  cc 10222  1c1 10225   · cmul 10229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-mulcl 10286  ax-mulcom 10288  ax-mulass 10290  ax-distr 10291  ax-1rid 10294  ax-cnre 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-iota 6067  df-fv 6112  df-ov 6880
This theorem is referenced by:  mulid2i  10333  mulid2d  10346  muladd11  10494  1p1times  10495  mul02lem1  10500  cnegex2  10506  mulm1  10759  div1  11004  recdiv  11019  divdiv2  11025  conjmul  11030  ser1const  13083  expp1  13093  recan  14302  arisum  14817  geo2sum  14829  prodrblem  14883  prodmolem2a  14888  risefac1  14987  fallfac1  14988  bpoly3  15012  bpoly4  15013  sinhval  15107  coshval  15108  demoivreALT  15154  gcdadd  15469  gcdid  15470  cncrng  19978  cnfld1  19982  cnfldmulg  19989  blcvx  22818  icccvx  22966  cnlmod  23156  coeidp  24239  dgrid  24240  quartlem1  24804  asinsinlem  24838  asinsin  24839  atantan  24870  musumsum  25138  brbtwn2  26005  axsegconlem1  26017  ax5seglem1  26028  ax5seglem2  26029  ax5seglem4  26032  ax5seglem5  26033  axeuclid  26063  axcontlem2  26065  axcontlem4  26067  cncvcOLD  27772  subdivcomb2  31939  dvcosax  40622
  Copyright terms: Public domain W3C validator