Theorem 2t1e2 12381

Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
2t1e2	⊢ (2 · 1) = 2

Proof of Theorem 2t1e2

Step	Hyp	Ref	Expression
1		2cn 12294	. 2 ⊢ 2 ∈ ℂ
2	1	mulridi 11187	1 ⊢ (2 · 1) = 2

Syntax hints:   = wceq 1561  (class class class)co 7397  1c1 11075   · cmul 11079  2c2 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-mulcl 11136  ax-mulcom 11138  ax-mulass 11140  ax-distr 11141  ax-1rid 11144  ax-cnre 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530  df-ov 7400  df-2 12281

This theorem is referenced by:  decbin2  12837  expubnd  14192  01sqrexlem7  15276  trirecip  15894  bpoly3  16089  fsumcube  16091  ege2le3  16121  cos2tsin  16212  cos2bnd  16221  odd2np1  16376  opoe  16398  flodddiv4  16450  2mulprm  16728  pythagtriplem4  16856  2503lem2  17175  2503lem3  17176  4001lem4  17181  4001prm  17182  htpycc  25043  pco1  25078  pcohtpylem  25082  pcopt  25085  pcorevlem  25089  ovolunlem1a  25559  cos2pi  26542  coskpi  26589  dcubic2  26910  dcubic  26912  basellem3  27148  chtublem  27276  bcp1ctr  27344  bclbnd  27345  bposlem1  27349  bposlem2  27350  bposlem5  27353  2lgslem3d1  27468  2sqreultlem  27512  2sqreunnltlem  27515  chebbnd1lem1  27534  chebbnd1lem3  27536  chebbnd1  27537  frgrregord013  30598  ex-ind-dvds  30664  wrdt2ind  33132  knoppndvlem12  36962  heiborlem6  38316  3lexlogpow5ineq1  42672  aks4d1p1  42694  2np3bcnp1  42762  2ap1caineq  42763  flt4lem7  43242  jm2.23  43574  sumnnodd  46207  wallispilem4  46643  wallispi2lem1  46646  wallispi2lem2  46647  wallispi2  46648  stirlinglem11  46659  dirkertrigeqlem1  46673  fouriersw  46806  fmtnorec4  48159  lighneallem2  48216  lighneallem3  48217  3exp4mod41  48226  opoeALTV  48306  fppr2odd  48354  8exp8mod9  48359  ackval2  49305  ackval2012  49314