Theorem 1t1e1 12350

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   · cmul 11080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  neg1mulneg1e1  12401  addltmul  12425  1exp  14063  expge1  14071  mulexp  14073  mulexpz  14074  expaddz  14078  m1expeven  14081  sqrecii  14155  i4  14176  facp1  14250  hashf1  14429  binom  15803  prodf1  15864  prodfrec  15868  fprodmul  15933  fprodge1  15968  fallfac0  16001  binomfallfac  16014  pwp1fsum  16368  rpmul  16636  2503lem2  17115  2503lem3  17116  4001lem4  17121  abvtrivd  20748  pzriprng1ALT  21413  iimulcl  24840  dvexp  25864  dvef  25891  mulcxplem  26600  cxpmul2  26605  dvsqrt  26658  dvcnsqrt  26660  abscxpbnd  26670  1cubr  26759  dchrmulcl  27167  dchr1cl  27169  dchrinvcl  27171  lgslem3  27217  lgsval2lem  27225  lgsneg  27239  lgsdilem  27242  lgsdir  27250  lgsdi  27252  lgsquad2lem1  27302  lgsquad2lem2  27303  dchrisum0flblem2  27427  rpvmasum2  27430  mudivsum  27448  pntibndlem2  27509  axlowdimlem6  28881  hisubcomi  31040  lnophmlem2  31953  1nei  32667  1neg1t1neg1  32668  sgnmul  32767  hgt750lem2  34650  subfacval2  35181  faclim2  35742  knoppndvlem18  36524  lcmineqlem12  42035  pell1234qrmulcl  42850  pellqrex  42874  imsqrtvalex  43642  binomcxplemnotnn0  44352  dvnprodlem3  45953  stoweidlem13  46018  stoweidlem16  46021  wallispi  46075  wallispi2lem2  46077  2exp340mod341  47738  8exp8mod9  47741  nn0sumshdiglemB  48613