Theorem 1t1e1 12429

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414  1c1 11128   · cmul 11132

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 2732  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

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 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7417

This theorem is used by:  neg1mulneg1e1  12483  addltmul  12507  1exp  14158  expge1  14166  mulexp  14168  mulexpz  14169  expaddz  14173  m1expeven  14176  sqrecii  14250  i4  14271  facp1  14345  hashf1  14525  sgnmul  15183  binom  15922  prodf1  15983  prodfrec  15987  fprodmul  16050  fprodge1  16085  fallfac0  16117  binomfallfac  16130  pwp1fsum  16484  rpmul  16752  2503lem2  17233  2503lem3  17234  4001lem4  17239  abvtrivd  21001  pzriprng1ALT  21712  iimulcl  25168  dvexp  26183  dvef  26210  mulcxplem  26924  cxpmul2  26929  dvsqrt  26982  dvcnsqrt  26984  abscxpbnd  26993  1cubr  27082  dchrmulcl  27488  dchr1cl  27490  dchrinvcl  27492  lgslem3  27538  lgsval2lem  27546  lgsneg  27560  lgsdilem  27563  lgsdir  27571  lgsdi  27573  lgsquad2lem1  27623  lgsquad2lem2  27624  dchrisum0flblem2  27748  rpvmasum2  27751  mudivsum  27769  pntibndlem2  27830  axlowdimlem6  29407  hisubcomi  31588  lnophmlem2  32501  1nei  33211  1neg1t1neg1  33212  hgt750lem2  35163  subfacval2  35769  faclim2  36330  knoppndvlem18  37229  lcmineqlem12  42909  pell1234qrmulcl  43699  pellqrex  43723  imsqrtvalex  44489  binomcxplemnotnn0  45183  dvnprodlem3  46779  stoweidlem13  46844  stoweidlem16  46847  wallispi  46901  wallispi2lem2  46903  2exp340mod341  48652  8exp8mod9  48655  nn0sumshdiglemB  49553