Theorem 1t1e1 12285

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   · cmul 11014

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 2701  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082

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 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  neg1mulneg1e1  12336  addltmul  12360  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  20717  pzriprng1ALT  21403  iimulcl  24831  dvexp  25855  dvef  25882  mulcxplem  26591  cxpmul2  26596  dvsqrt  26649  dvcnsqrt  26651  abscxpbnd  26661  1cubr  26750  dchrmulcl  27158  dchr1cl  27160  dchrinvcl  27162  lgslem3  27208  lgsval2lem  27216  lgsneg  27230  lgsdilem  27233  lgsdir  27241  lgsdi  27243  lgsquad2lem1  27293  lgsquad2lem2  27294  dchrisum0flblem2  27418  rpvmasum2  27421  mudivsum  27439  pntibndlem2  27500  axlowdimlem6  28892  hisubcomi  31048  lnophmlem2  31961  1nei  32681  1neg1t1neg1  32682  sgnmul  32781  hgt750lem2  34626  subfacval2  35170  faclim2  35731  knoppndvlem18  36513  lcmineqlem12  42023  pell1234qrmulcl  42838  pellqrex  42862  imsqrtvalex  43629  binomcxplemnotnn0  44339  dvnprodlem3  45939  stoweidlem13  46004  stoweidlem16  46007  wallispi  46061  wallispi2lem2  46063  2exp340mod341  47727  8exp8mod9  47730  nn0sumshdiglemB  48615