Theorem 1t1e1 12421

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 11177	. 2 ⊢ 1 ∈ ℂ
2	1	mulridi 11232	1 ⊢ (1 · 1) = 1

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11120   · cmul 11124

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11176  ax-1cn 11177  ax-icn 11178  ax-addcl 11179  ax-mulcl 11181  ax-mulcom 11183  ax-mulass 11185  ax-distr 11186  ax-1rid 11189  ax-cnre 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  neg1mulneg1e1  12475  addltmul  12499  1exp  14149  expge1  14157  mulexp  14159  mulexpz  14160  expaddz  14164  m1expeven  14167  sqrecii  14241  i4  14262  facp1  14336  hashf1  14516  sgnmul  15172  binom  15911  prodf1  15972  prodfrec  15976  fprodmul  16041  fprodge1  16076  fallfac0  16108  binomfallfac  16121  pwp1fsum  16475  rpmul  16743  2503lem2  17224  2503lem3  17225  4001lem4  17230  abvtrivd  20989  pzriprng1ALT  21700  iimulcl  25151  dvexp  26167  dvef  26194  mulcxplem  26904  cxpmul2  26909  dvsqrt  26962  dvcnsqrt  26964  abscxpbnd  26973  1cubr  27062  dchrmulcl  27468  dchr1cl  27470  dchrinvcl  27472  lgslem3  27518  lgsval2lem  27526  lgsneg  27540  lgsdilem  27543  lgsdir  27551  lgsdi  27553  lgsquad2lem1  27603  lgsquad2lem2  27604  dchrisum0flblem2  27728  rpvmasum2  27731  mudivsum  27749  pntibndlem2  27810  axlowdimlem6  29356  hisubcomi  31531  lnophmlem2  32444  1nei  33156  1neg1t1neg1  33157  hgt750lem2  35108  subfacval2  35720  faclim2  36281  knoppndvlem18  37179  lcmineqlem12  42869  pell1234qrmulcl  43659  pellqrex  43683  imsqrtvalex  44449  binomcxplemnotnn0  45143  dvnprodlem3  46739  stoweidlem13  46804  stoweidlem16  46807  wallispi  46861  wallispi2lem2  46863  2exp340mod341  48575  8exp8mod9  48578  nn0sumshdiglemB  49476