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

Theorem mulid2 8926
Description: Identity law for multiplication. Note: see mulid1 8925 for commuted version. (Contributed by NM, 8-Oct-1999.)
Assertion
Ref Expression
mulid2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )

Proof of Theorem mulid2
StepHypRef Expression
1 ax-1cn 8885 . . 3  |-  1  e.  CC
2 mulcom 8913 . . 3  |-  ( ( 1  e.  CC  /\  A  e.  CC )  ->  ( 1  x.  A
)  =  ( A  x.  1 ) )
31, 2mpan 651 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  ( A  x.  1 ) )
4 mulid1 8925 . 2  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
53, 4eqtrd 2390 1  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710  (class class class)co 5945   CCcc 8825   1c1 8828    x. cmul 8832
This theorem is referenced by:  mulid2i  8930  mulid2d  8943  muladd11  9072  1p1times  9073  mul02lem1  9078  cnegex2  9084  mulm1  9311  div1  9543  recdiv  9556  divdiv2  9562  conjmul  9567  2times  9935  ser1const  11194  expp1  11203  recan  11916  arisum  12415  geo2sum  12426  sinhval  12531  coshval  12532  demoivreALT  12578  gcdadd  12806  gcdid  12807  cncrng  16501  cnfld1  16505  cnfldmulg  16512  blcvx  18406  icccvx  18552  coeidp  19748  dgrid  19749  quartlem1  20264  asinsinlem  20298  asinsin  20299  atantan  20330  musumsum  20544  cnrngo  21182  cncvc  21253  subdivcomb2  24497  prodrblem  24556  prodmolem2a  24561  risefac1  24636  fallfac1  24637  brbtwn2  25092  axsegconlem1  25104  ax5seglem1  25115  ax5seglem2  25116  ax5seglem4  25119  ax5seglem5  25120  axeuclid  25150  axcontlem2  25152  axcontlem4  25154  bpoly3  25352  bpoly4  25353  fmul01lt1lem2  27038  stoweidlem13  27085  stoweidlem14  27086  stoweidlem26  27098  wallispilem4  27140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-mulcl 8889  ax-mulcom 8891  ax-mulass 8893  ax-distr 8894  ax-1rid 8897  ax-cnre 8900
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345  df-ov 5948
  Copyright terms: Public domain W3C validator