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

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

Proof of Theorem 1t1e1
StepHypRef Expression
1 ax-1cn 9941 . 2 1 ∈ ℂ
21mulid1i 9989 1 (1 · 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6607  1c1 9884   · cmul 9888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-mulcl 9945  ax-mulcom 9947  ax-mulass 9949  ax-distr 9950  ax-1rid 9953  ax-cnre 9956
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-iota 5812  df-fv 5857  df-ov 6610
This theorem is referenced by:  neg1mulneg1e1  11192  addltmul  11215  1exp  12832  expge1  12840  mulexp  12842  mulexpz  12843  expaddz  12847  m1expeven  12850  sqrecii  12889  i4  12910  facp1  13008  hashf1  13182  binom  14490  prodf1  14551  prodfrec  14555  fprodmul  14618  fprodge1  14654  fallfac0  14687  binomfallfac  14700  pwp1fsum  15041  rpmul  15300  2503lem2  15772  2503lem3  15773  4001lem4  15778  abvtrivd  18764  iimulcl  22649  dvexp  23629  dvef  23654  mulcxplem  24337  cxpmul2  24342  dvsqrt  24390  dvcnsqrt  24392  abscxpbnd  24401  1cubr  24476  dchrmulcl  24881  dchr1cl  24883  dchrinvcl  24885  lgslem3  24931  lgsval2lem  24939  lgsneg  24953  lgsdilem  24956  lgsdir  24964  lgsdi  24966  lgsquad2lem1  25016  lgsquad2lem2  25017  dchrisum0flblem2  25105  rpvmasum2  25108  mudivsum  25126  pntibndlem2  25187  axlowdimlem6  25734  hisubcomi  27822  lnophmlem2  28737  1neg1t1neg1  29369  sgnmul  30397  subfacval2  30898  faclim2  31363  knoppndvlem18  32183  pell1234qrmulcl  36920  pellqrex  36944  binomcxplemnotnn0  38058  dvnprodlem3  39486  stoweidlem13  39553  stoweidlem16  39556  wallispi  39610  wallispi2lem2  39612  nn0sumshdiglemB  41722
  Copyright terms: Public domain W3C validator