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

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

Proof of Theorem mulid2
StepHypRef Expression
1 ax-1cn 10584 . . 3 1 ∈ ℂ
2 mulcom 10612 . . 3 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
31, 2mpan 689 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4 mulid1 10628 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
53, 4eqtrd 2833 1 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2111  (class class class)co 7135  cc 10524  1c1 10527   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138
This theorem is referenced by:  mulid2i  10635  mulid2d  10648  muladd11  10799  1p1times  10800  mul02lem1  10805  cnegex2  10811  mulm1  11070  div1  11318  subdivcomb2  11325  recdiv  11335  divdiv2  11341  conjmul  11346  ser1const  13422  expp1  13432  recan  14688  arisum  15207  geo2sum  15221  prodrblem  15275  prodmolem2a  15280  risefac1  15379  fallfac1  15380  bpoly3  15404  bpoly4  15405  sinhval  15499  coshval  15500  demoivreALT  15546  gcdadd  15864  gcdid  15865  cncrng  20112  cnfld1  20116  blcvx  23403  icccvx  23555  cnlmod  23745  coeidp  24860  dgrid  24861  quartlem1  25443  asinsinlem  25477  asinsin  25478  atantan  25509  musumsum  25777  brbtwn2  26699  axsegconlem1  26711  ax5seglem1  26722  ax5seglem2  26723  ax5seglem4  26726  ax5seglem5  26727  axeuclid  26757  axcontlem2  26759  axcontlem4  26761  cncvcOLD  28366  dvcosax  42566
  Copyright terms: Public domain W3C validator