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

Theorem 1t1e1 12322
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 11116 . 2 1 ∈ ℂ
21mulid1i 11166 1 (1 · 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7362  1c1 11059   · cmul 11063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-mulcl 11120  ax-mulcom 11122  ax-mulass 11124  ax-distr 11125  ax-1rid 11128  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365
This theorem is referenced by:  neg1mulneg1e1  12373  addltmul  12396  1exp  14004  expge1  14012  mulexp  14014  mulexpz  14015  expaddz  14019  m1expeven  14022  sqrecii  14094  i4  14115  facp1  14185  hashf1  14363  binom  15722  prodf1  15783  prodfrec  15787  fprodmul  15850  fprodge1  15885  fallfac0  15918  binomfallfac  15931  pwp1fsum  16280  rpmul  16542  2503lem2  17017  2503lem3  17018  4001lem4  17023  abvtrivd  20315  iimulcl  24316  dvexp  25333  dvef  25360  mulcxplem  26055  cxpmul2  26060  dvsqrt  26111  dvcnsqrt  26113  abscxpbnd  26122  1cubr  26208  dchrmulcl  26613  dchr1cl  26615  dchrinvcl  26617  lgslem3  26663  lgsval2lem  26671  lgsneg  26685  lgsdilem  26688  lgsdir  26696  lgsdi  26698  lgsquad2lem1  26748  lgsquad2lem2  26749  dchrisum0flblem2  26873  rpvmasum2  26876  mudivsum  26894  pntibndlem2  26955  axlowdimlem6  27938  hisubcomi  30088  lnophmlem2  31001  1nei  31695  1neg1t1neg1  31696  sgnmul  33182  hgt750lem2  33305  subfacval2  33821  faclim2  34360  knoppndvlem18  35021  lcmineqlem12  40526  pell1234qrmulcl  41207  pellqrex  41231  imsqrtvalex  41992  binomcxplemnotnn0  42710  dvnprodlem3  44263  stoweidlem13  44328  stoweidlem16  44331  wallispi  44385  wallispi2lem2  44387  2exp340mod341  45999  8exp8mod9  46002  nn0sumshdiglemB  46780
  Copyright terms: Public domain W3C validator