Theorem 1t1e1 12316

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

Syntax hints:   = wceq 1542  (class class class)co 7370  1c1 11041   · cmul 11045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-mulcl 11102  ax-mulcom 11104  ax-mulass 11106  ax-distr 11107  ax-1rid 11110  ax-cnre 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  neg1mulneg1e1  12367  addltmul  12391  1exp  14028  expge1  14036  mulexp  14038  mulexpz  14039  expaddz  14043  m1expeven  14046  sqrecii  14120  i4  14141  facp1  14215  hashf1  14394  binom  15767  prodf1  15828  prodfrec  15832  fprodmul  15897  fprodge1  15932  fallfac0  15965  binomfallfac  15978  pwp1fsum  16332  rpmul  16600  2503lem2  17079  2503lem3  17080  4001lem4  17085  abvtrivd  20782  pzriprng1ALT  21468  iimulcl  24906  dvexp  25930  dvef  25957  mulcxplem  26666  cxpmul2  26671  dvsqrt  26724  dvcnsqrt  26726  abscxpbnd  26736  1cubr  26825  dchrmulcl  27233  dchr1cl  27235  dchrinvcl  27237  lgslem3  27283  lgsval2lem  27291  lgsneg  27305  lgsdilem  27308  lgsdir  27316  lgsdi  27318  lgsquad2lem1  27368  lgsquad2lem2  27369  dchrisum0flblem2  27493  rpvmasum2  27496  mudivsum  27514  pntibndlem2  27575  axlowdimlem6  29038  hisubcomi  31198  lnophmlem2  32111  1nei  32833  1neg1t1neg1  32834  sgnmul  32933  hgt750lem2  34836  subfacval2  35409  faclim2  35970  knoppndvlem18  36757  lcmineqlem12  42439  pell1234qrmulcl  43241  pellqrex  43265  imsqrtvalex  44031  binomcxplemnotnn0  44741  dvnprodlem3  46335  stoweidlem13  46400  stoweidlem16  46403  wallispi  46457  wallispi2lem2  46459  2exp340mod341  48122  8exp8mod9  48125  nn0sumshdiglemB  49009