Theorem 1t1e1 12504

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  neg1mulneg1e1  12558  addltmul  12582  1exp  14234  expge1  14242  mulexp  14244  mulexpz  14245  expaddz  14249  m1expeven  14252  sqrecii  14326  i4  14348  facp1  14422  hashf1  14602  sgnmul  15260  binom  15999  prodf1  16060  prodfrec  16064  fprodmul  16127  fprodge1  16162  fallfac0  16194  binomfallfac  16207  pwp1fsum  16561  rpmul  16834  2503lem2  17316  2503lem3  17317  4001lem4  17322  abvtrivd  21089  pzriprng1ALT  21802  iimulcl  25258  dvexp  26273  dvef  26300  mulcxplem  27012  cxpmul2  27017  dvsqrt  27070  dvcnsqrt  27072  abscxpbnd  27081  1cubr  27170  dchrmulcl  27576  dchr1cl  27578  dchrinvcl  27580  lgslem3  27626  lgsval2lem  27634  lgsneg  27648  lgsdilem  27651  lgsdir  27659  lgsdi  27661  lgsquad2lem1  27711  lgsquad2lem2  27712  dchrisum0flblem2  27836  rpvmasum2  27839  mudivsum  27857  pntibndlem2  27918  axlowdimlem6  29525  hisubcomi  31706  lnophmlem2  32619  1nei  33329  1neg1t1neg1  33330  hgt750lem2  35281  subfacval2  35952  faclim2  36513  knoppndvlem18  37395  lcmineqlem12  43090  pell1234qrmulcl  43861  pellqrex  43885  imsqrtvalex  44645  binomcxplemnotnn0  45339  dvnprodlem3  46957  stoweidlem13  47022  stoweidlem16  47025  wallispi  47079  wallispi2lem2  47081  2exp340mod341  48830  8exp8mod9  48833  nn0sumshdiglemB  49731