Theorem 1t1e1 12402

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

Step	Hyp	Ref	Expression
1		ax-1cn 11158	. 2 ⊢ 1 ∈ ℂ
2	1	mulridi 11213	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   · cmul 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulcom 11164  ax-mulass 11166  ax-distr 11167  ax-1rid 11170  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  neg1mulneg1e1  12456  addltmul  12480  1exp  14127  expge1  14135  mulexp  14137  mulexpz  14138  expaddz  14142  m1expeven  14145  sqrecii  14219  i4  14240  facp1  14314  hashf1  14494  sgnmul  15144  binom  15884  prodf1  15945  prodfrec  15949  fprodmul  16014  fprodge1  16049  fallfac0  16082  binomfallfac  16095  pwp1fsum  16449  rpmul  16717  2503lem2  17198  2503lem3  17199  4001lem4  17204  abvtrivd  20913  pzriprng1ALT  21615  iimulcl  25065  dvexp  26081  dvef  26108  mulcxplem  26815  cxpmul2  26820  dvsqrt  26873  dvcnsqrt  26875  abscxpbnd  26884  1cubr  26973  dchrmulcl  27379  dchr1cl  27381  dchrinvcl  27383  lgslem3  27429  lgsval2lem  27437  lgsneg  27451  lgsdilem  27454  lgsdir  27462  lgsdi  27464  lgsquad2lem1  27514  lgsquad2lem2  27515  dchrisum0flblem2  27639  rpvmasum2  27642  mudivsum  27660  pntibndlem2  27721  axlowdimlem6  29238  hisubcomi  31397  lnophmlem2  32310  1nei  33023  1neg1t1neg1  33024  hgt750lem2  34984  subfacval2  35612  faclim2  36173  knoppndvlem18  37041  lcmineqlem12  42731  pell1234qrmulcl  43508  pellqrex  43532  imsqrtvalex  44298  binomcxplemnotnn0  44992  dvnprodlem3  46588  stoweidlem13  46653  stoweidlem16  46656  wallispi  46710  wallispi2lem2  46712  2exp340mod341  48421  8exp8mod9  48424  nn0sumshdiglemB  49319