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

Theorem mulid2 11161
Description: Identity law for multiplication. See mulid1 11160 for commuted version. (Contributed by NM, 8-Oct-1999.)
Assertion
Ref Expression
mulid2 (๐ด โˆˆ โ„‚ โ†’ (1 ยท ๐ด) = ๐ด)

Proof of Theorem mulid2
StepHypRef Expression
1 ax-1cn 11116 . . 3 1 โˆˆ โ„‚
2 mulcom 11144 . . 3 ((1 โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (1 ยท ๐ด) = (๐ด ยท 1))
31, 2mpan 689 . 2 (๐ด โˆˆ โ„‚ โ†’ (1 ยท ๐ด) = (๐ด ยท 1))
4 mulid1 11160 . 2 (๐ด โˆˆ โ„‚ โ†’ (๐ด ยท 1) = ๐ด)
53, 4eqtrd 2777 1 (๐ด โˆˆ โ„‚ โ†’ (1 ยท ๐ด) = ๐ด)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7362  โ„‚cc 11056  1c1 11059   ยท cmul 11063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-mulcl 11120  ax-mulcom 11122  ax-mulass 11124  ax-distr 11125  ax-1rid 11128  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365
This theorem is referenced by:  mulid2i  11167  mulid2d  11180  muladd11  11332  1p1times  11333  mul02lem1  11338  cnegex2  11344  mulm1  11603  div1  11851  subdivcomb2  11858  recdiv  11868  divdiv2  11874  conjmul  11879  ser1const  13971  expp1  13981  recan  15228  arisum  15752  geo2sum  15765  prodrblem  15819  prodmolem2a  15824  risefac1  15923  fallfac1  15924  bpoly3  15948  bpoly4  15949  sinhval  16043  coshval  16044  demoivreALT  16090  gcdadd  16413  gcdid  16414  cncrng  20834  cnfld1  20838  blcvx  24177  icccvx  24329  cnlmod  24519  coeidp  25640  dgrid  25641  quartlem1  26223  asinsinlem  26257  asinsin  26258  atantan  26289  musumsum  26557  brbtwn2  27896  axsegconlem1  27908  ax5seglem1  27919  ax5seglem2  27920  ax5seglem4  27923  ax5seglem5  27924  axeuclid  27954  axcontlem2  27956  axcontlem4  27958  cncvcOLD  29567  dvcosax  44241
  Copyright terms: Public domain W3C validator