Theorem 1t1e1 12282

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   · cmul 11011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulcom 11070  ax-mulass 11072  ax-distr 11073  ax-1rid 11076  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  neg1mulneg1e1  12333  addltmul  12357  1exp  13998  expge1  14006  mulexp  14008  mulexpz  14009  expaddz  14013  m1expeven  14016  sqrecii  14090  i4  14111  facp1  14185  hashf1  14364  binom  15737  prodf1  15798  prodfrec  15802  fprodmul  15867  fprodge1  15902  fallfac0  15935  binomfallfac  15948  pwp1fsum  16302  rpmul  16570  2503lem2  17049  2503lem3  17050  4001lem4  17055  abvtrivd  20747  pzriprng1ALT  21433  iimulcl  24860  dvexp  25884  dvef  25911  mulcxplem  26620  cxpmul2  26625  dvsqrt  26678  dvcnsqrt  26680  abscxpbnd  26690  1cubr  26779  dchrmulcl  27187  dchr1cl  27189  dchrinvcl  27191  lgslem3  27237  lgsval2lem  27245  lgsneg  27259  lgsdilem  27262  lgsdir  27270  lgsdi  27272  lgsquad2lem1  27322  lgsquad2lem2  27323  dchrisum0flblem2  27447  rpvmasum2  27450  mudivsum  27468  pntibndlem2  27529  axlowdimlem6  28925  hisubcomi  31084  lnophmlem2  31997  1nei  32720  1neg1t1neg1  32721  sgnmul  32818  hgt750lem2  34665  subfacval2  35231  faclim2  35792  knoppndvlem18  36573  lcmineqlem12  42132  pell1234qrmulcl  42947  pellqrex  42971  imsqrtvalex  43738  binomcxplemnotnn0  44448  dvnprodlem3  46045  stoweidlem13  46110  stoweidlem16  46113  wallispi  46167  wallispi2lem2  46169  2exp340mod341  47832  8exp8mod9  47835  nn0sumshdiglemB  48720