Theorem 1t1e1 12398

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

Syntax hints:   = wceq 1534  (class class class)co 7414  1c1 11133   · cmul 11137

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 2698  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-mulcl 11194  ax-mulcom 11196  ax-mulass 11198  ax-distr 11199  ax-1rid 11202  ax-cnre 11205

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 2705  df-cleq 2719  df-clel 2805  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417

This theorem is referenced by:  neg1mulneg1e1  12449  addltmul  12472  1exp  14082  expge1  14090  mulexp  14092  mulexpz  14093  expaddz  14097  m1expeven  14100  sqrecii  14172  i4  14193  facp1  14263  hashf1  14444  binom  15802  prodf1  15863  prodfrec  15867  fprodmul  15930  fprodge1  15965  fallfac0  15998  binomfallfac  16011  pwp1fsum  16361  rpmul  16623  2503lem2  17100  2503lem3  17101  4001lem4  17106  abvtrivd  20713  pzriprng1ALT  21415  iimulcl  24853  dvexp  25878  dvef  25905  mulcxplem  26611  cxpmul2  26616  dvsqrt  26669  dvcnsqrt  26671  abscxpbnd  26681  1cubr  26767  dchrmulcl  27175  dchr1cl  27177  dchrinvcl  27179  lgslem3  27225  lgsval2lem  27233  lgsneg  27247  lgsdilem  27250  lgsdir  27258  lgsdi  27260  lgsquad2lem1  27310  lgsquad2lem2  27311  dchrisum0flblem2  27435  rpvmasum2  27438  mudivsum  27456  pntibndlem2  27517  axlowdimlem6  28751  hisubcomi  30907  lnophmlem2  31820  1nei  32512  1neg1t1neg1  32513  sgnmul  34152  hgt750lem2  34274  subfacval2  34787  faclim2  35332  knoppndvlem18  35994  lcmineqlem12  41500  pell1234qrmulcl  42247  pellqrex  42271  imsqrtvalex  43048  binomcxplemnotnn0  43765  dvnprodlem3  45308  stoweidlem13  45373  stoweidlem16  45376  wallispi  45430  wallispi2lem2  45432  2exp340mod341  47045  8exp8mod9  47048  nn0sumshdiglemB  47665