Theorem 1t1e1 11377

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

Syntax hints:   = wceq 1631  (class class class)co 6793  1c1 10139   · cmul 10143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-mulcl 10200  ax-mulcom 10202  ax-mulass 10204  ax-distr 10205  ax-1rid 10208  ax-cnre 10211

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796

This theorem is referenced by:  neg1mulneg1e1  11447  addltmul  11470  1exp  13096  expge1  13104  mulexp  13106  mulexpz  13107  expaddz  13111  m1expeven  13114  sqrecii  13153  i4  13174  facp1  13269  hashf1  13443  binom  14769  prodf1  14830  prodfrec  14834  fprodmul  14897  fprodge1  14932  fallfac0  14965  binomfallfac  14978  pwp1fsum  15322  rpmul  15580  2503lem2  16052  2503lem3  16053  4001lem4  16058  abvtrivd  19050  iimulcl  22956  dvexp  23936  dvef  23963  mulcxplem  24651  cxpmul2  24656  dvsqrt  24704  dvcnsqrt  24706  abscxpbnd  24715  1cubr  24790  dchrmulcl  25195  dchr1cl  25197  dchrinvcl  25199  lgslem3  25245  lgsval2lem  25253  lgsneg  25267  lgsdilem  25270  lgsdir  25278  lgsdi  25280  lgsquad2lem1  25330  lgsquad2lem2  25331  dchrisum0flblem2  25419  rpvmasum2  25422  mudivsum  25440  pntibndlem2  25501  axlowdimlem6  26048  hisubcomi  28301  lnophmlem2  29216  1neg1t1neg1  29854  sgnmul  30944  hgt750lem2  31070  subfacval2  31507  faclim2  31972  knoppndvlem18  32857  pell1234qrmulcl  37945  pellqrex  37969  binomcxplemnotnn0  39081  dvnprodlem3  40681  stoweidlem13  40747  stoweidlem16  40750  wallispi  40804  wallispi2lem2  40806  nn0sumshdiglemB  42942