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

Theorem 1t1e1 10118
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 9040 . 2  |-  1  e.  CC
21mulid1i 9084 1  |-  ( 1  x.  1 )  =  1
Colors of variables: wff set class
Syntax hints:    = wceq 1652  (class class class)co 6073   1c1 8983    x. cmul 8987
This theorem is referenced by:  addltmul  10195  1exp  11401  expge1  11409  mulexp  11411  mulexpz  11412  expaddz  11416  sqrecii  11456  i4  11475  facp1  11563  hashf1  11698  binom  12601  rpmul  13115  2503lem2  13449  4001lem4  13455  abvtrivd  15920  iimulcl  18954  dvexp  19831  dvef  19856  plydivlem1  20202  mulcxplem  20567  cxpmul2  20572  dvsqr  20620  abscxpbnd  20629  1cubr  20674  dchrmulcl  21025  dchr1cl  21027  dchrinvcl  21029  lgslem3  21074  lgsval2lem  21082  lgsneg  21095  lgsdilem  21098  lgsdir  21106  lgsdi  21108  lgsquad2lem1  21134  lgsquad2lem2  21135  dchrisum0flblem2  21195  rpvmasum2  21198  mudivsum  21216  pntibndlem2  21277  vcnegneg  22045  nvnncan  22136  ipdirilem  22322  hvnegdii  22556  hisubcomi  22598  honegneg  23301  lnophmlem2  23512  subfacval2  24865  m1expevenALT  24897  prodf1  25211  prodfrec  25215  fprodmul  25276  fallfac0  25336  binomfallfac  25349  faclim2  25359  axlowdimlem6  25878  pell1234qrmulcl  26909  pellqrex  26933  stoweidlem13  27729  stoweidlem16  27732  wallispi  27786  wallispi2lem2  27788
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-mulcl 9044  ax-mulcom 9046  ax-mulass 9048  ax-distr 9049  ax-1rid 9052  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076
  Copyright terms: Public domain W3C validator