Theorem 1t1e1 12406

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7410  1c1 11105   · cmul 11109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-mulcl 11166  ax-mulcom 11168  ax-mulass 11170  ax-distr 11171  ax-1rid 11174  ax-cnre 11177

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is used by:  neg1mulneg1e1  12460  addltmul  12484  1exp  14132  expge1  14140  mulexp  14142  mulexpz  14143  expaddz  14147  m1expeven  14150  sqrecii  14224  i4  14245  facp1  14319  hashf1  14499  sgnmul  15149  binom  15889  prodf1  15950  prodfrec  15954  fprodmul  16019  fprodge1  16054  fallfac0  16086  binomfallfac  16099  pwp1fsum  16453  rpmul  16721  2503lem2  17202  2503lem3  17203  4001lem4  17208  abvtrivd  20944  pzriprng1ALT  21655  iimulcl  25105  dvexp  26121  dvef  26148  mulcxplem  26858  cxpmul2  26863  dvsqrt  26916  dvcnsqrt  26918  abscxpbnd  26927  1cubr  27016  dchrmulcl  27422  dchr1cl  27424  dchrinvcl  27426  lgslem3  27472  lgsval2lem  27480  lgsneg  27494  lgsdilem  27497  lgsdir  27505  lgsdi  27507  lgsquad2lem1  27557  lgsquad2lem2  27558  dchrisum0flblem2  27682  rpvmasum2  27685  mudivsum  27703  pntibndlem2  27764  axlowdimlem6  29306  hisubcomi  31465  lnophmlem2  32378  1nei  33091  1neg1t1neg1  33092  hgt750lem2  35048  subfacval2  35687  faclim2  36248  knoppndvlem18  37146  lcmineqlem12  42835  pell1234qrmulcl  43610  pellqrex  43634  imsqrtvalex  44400  binomcxplemnotnn0  45094  dvnprodlem3  46690  stoweidlem13  46755  stoweidlem16  46758  wallispi  46812  wallispi2lem2  46814  2exp340mod341  48526  8exp8mod9  48529  nn0sumshdiglemB  49428