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 10584 . 2 1 ∈ ℂ
21mulid1i 10634 1 (1 · 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7140  1c1 10527   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-rex 3136  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143
This theorem is referenced by:  neg1mulneg1e1  11838  addltmul  11861  1exp  13454  expge1  13462  mulexp  13464  mulexpz  13465  expaddz  13469  m1expeven  13472  sqrecii  13542  i4  13563  facp1  13634  hashf1  13811  binom  15176  prodf1  15238  prodfrec  15242  fprodmul  15305  fprodge1  15340  fallfac0  15373  binomfallfac  15386  pwp1fsum  15731  rpmul  15992  2503lem2  16462  2503lem3  16463  4001lem4  16468  abvtrivd  19602  iimulcl  23540  dvexp  24554  dvef  24581  mulcxplem  25273  cxpmul2  25278  dvsqrt  25329  dvcnsqrt  25331  abscxpbnd  25340  1cubr  25426  dchrmulcl  25831  dchr1cl  25833  dchrinvcl  25835  lgslem3  25881  lgsval2lem  25889  lgsneg  25903  lgsdilem  25906  lgsdir  25914  lgsdi  25916  lgsquad2lem1  25966  lgsquad2lem2  25967  dchrisum0flblem2  26091  rpvmasum2  26094  mudivsum  26112  pntibndlem2  26173  axlowdimlem6  26739  hisubcomi  28885  lnophmlem2  29798  1nei  30482  1neg1t1neg1  30483  sgnmul  31874  hgt750lem2  31997  subfacval2  32508  faclim2  33054  knoppndvlem18  33942  lcmineqlem12  39289  3lexlogpow5ineq1  39302  pell1234qrmulcl  39726  pellqrex  39750  imsqrtvalex  40276  binomcxplemnotnn0  40994  dvnprodlem3  42529  stoweidlem13  42594  stoweidlem16  42597  wallispi  42651  wallispi2lem2  42653  2exp340mod341  44190  8exp8mod9  44193  nn0sumshdiglemB  44973
  Copyright terms: Public domain W3C validator