Theorem 1t1e1 12399

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

Syntax hints:   = wceq 1534  (class class class)co 7415  1c1 11134   · cmul 11138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-mulcl 11195  ax-mulcom 11197  ax-mulass 11199  ax-distr 11200  ax-1rid 11203  ax-cnre 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418

This theorem is referenced by:  neg1mulneg1e1  12450  addltmul  12473  1exp  14083  expge1  14091  mulexp  14093  mulexpz  14094  expaddz  14098  m1expeven  14101  sqrecii  14173  i4  14194  facp1  14264  hashf1  14445  binom  15803  prodf1  15864  prodfrec  15868  fprodmul  15931  fprodge1  15966  fallfac0  15999  binomfallfac  16012  pwp1fsum  16362  rpmul  16624  2503lem2  17101  2503lem3  17102  4001lem4  17107  abvtrivd  20714  pzriprng1ALT  21416  iimulcl  24854  dvexp  25879  dvef  25906  mulcxplem  26612  cxpmul2  26617  dvsqrt  26670  dvcnsqrt  26672  abscxpbnd  26682  1cubr  26768  dchrmulcl  27176  dchr1cl  27178  dchrinvcl  27180  lgslem3  27226  lgsval2lem  27234  lgsneg  27248  lgsdilem  27251  lgsdir  27259  lgsdi  27261  lgsquad2lem1  27311  lgsquad2lem2  27312  dchrisum0flblem2  27436  rpvmasum2  27439  mudivsum  27457  pntibndlem2  27518  axlowdimlem6  28752  hisubcomi  30908  lnophmlem2  31821  1nei  32513  1neg1t1neg1  32514  sgnmul  34157  hgt750lem2  34279  subfacval2  34792  faclim2  35337  knoppndvlem18  35999  lcmineqlem12  41506  pell1234qrmulcl  42266  pellqrex  42290  imsqrtvalex  43067  binomcxplemnotnn0  43784  dvnprodlem3  45327  stoweidlem13  45392  stoweidlem16  45395  wallispi  45449  wallispi2lem2  45451  2exp340mod341  47064  8exp8mod9  47067  nn0sumshdiglemB  47684