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

Theorem 1t1e1 11787
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 10583 . 2 1 ∈ ℂ
21mulid1i 10633 1 (1 · 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145  1c1 10526   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulcom 10589  ax-mulass 10591  ax-distr 10592  ax-1rid 10595  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  neg1mulneg1e1  11838  addltmul  11861  1exp  13446  expge1  13454  mulexp  13456  mulexpz  13457  expaddz  13461  m1expeven  13464  sqrecii  13534  i4  13555  facp1  13626  hashf1  13803  binom  15173  prodf1  15235  prodfrec  15239  fprodmul  15302  fprodge1  15337  fallfac0  15370  binomfallfac  15383  pwp1fsum  15730  rpmul  15991  2503lem2  16459  2503lem3  16460  4001lem4  16465  abvtrivd  19540  iimulcl  23468  dvexp  24477  dvef  24504  mulcxplem  25194  cxpmul2  25199  dvsqrt  25250  dvcnsqrt  25252  abscxpbnd  25261  1cubr  25347  dchrmulcl  25752  dchr1cl  25754  dchrinvcl  25756  lgslem3  25802  lgsval2lem  25810  lgsneg  25824  lgsdilem  25827  lgsdir  25835  lgsdi  25837  lgsquad2lem1  25887  lgsquad2lem2  25888  dchrisum0flblem2  26012  rpvmasum2  26015  mudivsum  26033  pntibndlem2  26094  axlowdimlem6  26660  hisubcomi  28808  lnophmlem2  29721  1nei  30398  1neg1t1neg1  30399  sgnmul  31699  hgt750lem2  31822  subfacval2  32331  faclim2  32877  knoppndvlem18  33765  pell1234qrmulcl  39330  pellqrex  39354  binomcxplemnotnn0  40565  dvnprodlem3  42109  stoweidlem13  42175  stoweidlem16  42178  wallispi  42232  wallispi2lem2  42234  2exp340mod341  43775  8exp8mod9  43778  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator