Theorem 1t1e1 12381

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

Syntax hints:   = wceq 1562  (class class class)co 7398  1c1 11076   · cmul 11080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  neg1mulneg1e1  12435  addltmul  12459  1exp  14106  expge1  14114  mulexp  14116  mulexpz  14117  expaddz  14121  m1expeven  14124  sqrecii  14198  i4  14219  facp1  14293  hashf1  14472  sgnmul  15122  binom  15862  prodf1  15923  prodfrec  15927  fprodmul  15992  fprodge1  16027  fallfac0  16060  binomfallfac  16073  pwp1fsum  16427  rpmul  16695  2503lem2  17176  2503lem3  17177  4001lem4  17182  abvtrivd  20883  pzriprng1ALT  21550  iimulcl  25001  dvexp  26017  dvef  26044  mulcxplem  26751  cxpmul2  26756  dvsqrt  26809  dvcnsqrt  26811  abscxpbnd  26820  1cubr  26909  dchrmulcl  27315  dchr1cl  27317  dchrinvcl  27319  lgslem3  27365  lgsval2lem  27373  lgsneg  27387  lgsdilem  27390  lgsdir  27398  lgsdi  27400  lgsquad2lem1  27450  lgsquad2lem2  27451  dchrisum0flblem2  27575  rpvmasum2  27578  mudivsum  27596  pntibndlem2  27657  axlowdimlem6  29150  hisubcomi  31309  lnophmlem2  32222  1nei  32941  1neg1t1neg1  32942  hgt750lem2  34948  subfacval2  35542  faclim2  36103  knoppndvlem18  36972  lcmineqlem12  42662  pell1234qrmulcl  43437  pellqrex  43461  imsqrtvalex  44227  binomcxplemnotnn0  44937  dvnprodlem3  46527  stoweidlem13  46592  stoweidlem16  46595  wallispi  46649  wallispi2lem2  46651  2exp340mod341  48360  8exp8mod9  48363  nn0sumshdiglemB  49247