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

Theorem mulid2 9384
Description: Identity law for multiplication. Note: see mulid1 9383 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 9340 . . 3  |-  1  e.  CC
2 mulcom 9368 . . 3  |-  ( ( 1  e.  CC  /\  A  e.  CC )  ->  ( 1  x.  A
)  =  ( A  x.  1 ) )
31, 2mpan 670 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  ( A  x.  1 ) )
4 mulid1 9383 . 2  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
53, 4eqtrd 2475 1  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6091   CCcc 9280   1c1 9283    x. cmul 9287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-mulcl 9344  ax-mulcom 9346  ax-mulass 9348  ax-distr 9349  ax-1rid 9352  ax-cnre 9355
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094
This theorem is referenced by:  mulid2i  9389  mulid2d  9404  muladd11  9539  1p1times  9540  mul02lem1  9545  cnegex2  9551  mulm1  9786  div1  10023  recdiv  10037  divdiv2  10043  conjmul  10048  2times  10440  ser1const  11862  expp1  11872  recan  12824  arisum  13322  geo2sum  13333  sinhval  13438  coshval  13439  demoivreALT  13485  gcdadd  13714  gcdid  13715  cncrng  17837  cnfld1  17841  cnfldmulg  17848  blcvx  20375  icccvx  20522  coeidp  21730  dgrid  21731  quartlem1  22252  asinsinlem  22286  asinsin  22287  atantan  22318  musumsum  22532  brbtwn2  23151  axsegconlem1  23163  ax5seglem1  23174  ax5seglem2  23175  ax5seglem4  23178  ax5seglem5  23179  axeuclid  23209  axcontlem2  23211  axcontlem4  23213  cnrngo  23890  cncvc  23961  subdivcomb2  27385  prodrblem  27442  prodmolem2a  27447  risefac1  27536  fallfac1  27537  bpoly3  28201  bpoly4  28202
  Copyright terms: Public domain W3C validator