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

Theorem 1t1e1 10082
Description: 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
1t1e1  |-  ( 1  x.  1 )  =  1

Proof of Theorem 1t1e1
StepHypRef Expression
1 ax-1cn 9004 . 2  |-  1  e.  CC
21mulid1i 9048 1  |-  ( 1  x.  1 )  =  1
Colors of variables: wff set class
Syntax hints:    = wceq 1649  (class class class)co 6040   1c1 8947    x. cmul 8951
This theorem is referenced by:  addltmul  10159  1exp  11364  expge1  11372  mulexp  11374  mulexpz  11375  expaddz  11379  sqrecii  11419  i4  11438  facp1  11526  hashf1  11661  binom  12564  rpmul  13078  2503lem2  13412  4001lem4  13418  abvtrivd  15883  iimulcl  18915  dvexp  19792  dvef  19817  plydivlem1  20163  mulcxplem  20528  cxpmul2  20533  dvsqr  20581  abscxpbnd  20590  1cubr  20635  dchrmulcl  20986  dchr1cl  20988  dchrinvcl  20990  lgslem3  21035  lgsval2lem  21043  lgsneg  21056  lgsdilem  21059  lgsdir  21067  lgsdi  21069  lgsquad2lem1  21095  lgsquad2lem2  21096  dchrisum0flblem2  21156  rpvmasum2  21159  mudivsum  21177  pntibndlem2  21238  vcnegneg  22006  nvnncan  22097  ipdirilem  22283  hvnegdii  22517  hisubcomi  22559  honegneg  23262  lnophmlem2  23473  subfacval2  24826  m1expevenALT  24858  prodf1  25172  prodfrec  25176  fprodmul  25237  fallfac0  25296  binomfallfac  25308  faclim2  25315  axlowdimlem6  25790  pell1234qrmulcl  26808  pellqrex  26832  stoweidlem13  27629  stoweidlem16  27632  wallispi  27686  wallispi2lem2  27688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-mulcom 9010  ax-mulass 9012  ax-distr 9013  ax-1rid 9016  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator