Theorem 1t1e1 12517

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430  1c1 11214   · cmul 11218

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-mulcl 11275  ax-mulcom 11277  ax-mulass 11279  ax-distr 11280  ax-1rid 11283  ax-cnre 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433

This theorem is used by:  neg1mulneg1e1  12571  addltmul  12595  1exp  14247  expge1  14255  mulexp  14257  mulexpz  14258  expaddz  14262  m1expeven  14265  sqrecii  14339  i4  14361  facp1  14435  hashf1  14615  sgnmul  15275  binom  16014  prodf1  16075  prodfrec  16079  fprodmul  16142  fprodge1  16177  fallfac0  16209  binomfallfac  16222  pwp1fsum  16576  rpmul  16849  2503lem2  17331  2503lem3  17332  4001lem4  17337  abvtrivd  21104  pzriprng1ALT  21817  iimulcl  25273  dvexp  26288  dvef  26315  mulcxplem  27027  cxpmul2  27032  dvsqrt  27085  dvcnsqrt  27087  abscxpbnd  27096  1cubr  27185  dchrmulcl  27591  dchr1cl  27593  dchrinvcl  27595  lgslem3  27641  lgsval2lem  27649  lgsneg  27663  lgsdilem  27666  lgsdir  27674  lgsdi  27676  lgsquad2lem1  27726  lgsquad2lem2  27727  dchrisum0flblem2  27851  rpvmasum2  27854  mudivsum  27872  pntibndlem2  27933  axlowdimlem6  29540  hisubcomi  31721  lnophmlem2  32634  1nei  33385  1neg1t1neg1  33386  hgt750lem2  35337  subfacval2  36076  faclim2  36643  knoppndvlem18  37525  lcmineqlem12  43233  pell1234qrmulcl  44005  pellqrex  44029  imsqrtvalex  44789  binomcxplemnotnn0  45483  dvnprodlem3  47100  stoweidlem13  47165  stoweidlem16  47168  wallispi  47222  wallispi2lem2  47224  2exp340mod341  48973  8exp8mod9  48976  nn0sumshdiglemB  49874