Theorem 1t1e1 12135

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 10929	. 2 ⊢ 1 ∈ ℂ
2	1	mulid1i 10979	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1539  (class class class)co 7275  1c1 10872   · cmul 10876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-mulcom 10935  ax-mulass 10937  ax-distr 10938  ax-1rid 10941  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  neg1mulneg1e1  12186  addltmul  12209  1exp  13812  expge1  13820  mulexp  13822  mulexpz  13823  expaddz  13827  m1expeven  13830  sqrecii  13900  i4  13921  facp1  13992  hashf1  14171  binom  15542  prodf1  15603  prodfrec  15607  fprodmul  15670  fprodge1  15705  fallfac0  15738  binomfallfac  15751  pwp1fsum  16100  rpmul  16364  2503lem2  16839  2503lem3  16840  4001lem4  16845  abvtrivd  20100  iimulcl  24100  dvexp  25117  dvef  25144  mulcxplem  25839  cxpmul2  25844  dvsqrt  25895  dvcnsqrt  25897  abscxpbnd  25906  1cubr  25992  dchrmulcl  26397  dchr1cl  26399  dchrinvcl  26401  lgslem3  26447  lgsval2lem  26455  lgsneg  26469  lgsdilem  26472  lgsdir  26480  lgsdi  26482  lgsquad2lem1  26532  lgsquad2lem2  26533  dchrisum0flblem2  26657  rpvmasum2  26660  mudivsum  26678  pntibndlem2  26739  axlowdimlem6  27315  hisubcomi  29466  lnophmlem2  30379  1nei  31071  1neg1t1neg1  31072  sgnmul  32509  hgt750lem2  32632  subfacval2  33149  faclim2  33714  knoppndvlem18  34709  lcmineqlem12  40048  pell1234qrmulcl  40677  pellqrex  40701  imsqrtvalex  41254  binomcxplemnotnn0  41974  dvnprodlem3  43489  stoweidlem13  43554  stoweidlem16  43557  wallispi  43611  wallispi2lem2  43613  2exp340mod341  45185  8exp8mod9  45188  nn0sumshdiglemB  45966