Theorem 2t1e2 12505

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

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

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  df-2 12405

This theorem is used by:  decbin2  12962  expubnd  14321  01sqrexlem7  15415  trirecip  16032  bpoly3  16224  fsumcube  16226  ege2le3  16256  cos2tsin  16347  cos2bnd  16356  odd2np1  16511  opoe  16533  flodddiv4  16585  2mulprm  16868  pythagtriplem4  16997  2503lem2  17316  2503lem3  17317  4001lem4  17322  4001prm  17323  htpycc  25301  pco1  25336  pcohtpylem  25340  pcopt  25343  pcorevlem  25347  ovolunlem1a  25817  cos2pi  26805  coskpi  26851  dcubic2  27172  dcubic  27174  basellem3  27410  chtublem  27538  bcp1ctr  27606  bclbnd  27607  bposlem1  27611  bposlem2  27612  bposlem5  27615  2lgslem3d1  27730  2sqreultlem  27774  2sqreunnltlem  27777  chebbnd1lem1  27796  chebbnd1lem3  27798  chebbnd1  27799  flt4lem7  27989  frgrregord013  30996  ex-ind-dvds  31062  wrdt2ind  33516  knoppndvlem12  37389  heiborlem6  38750  3lexlogpow5ineq1  43104  aks4d1p1  43126  2np3bcnp1  43194  2ap1caineq  43195  jm2.23  44002  sumnnodd  46641  wallispilem4  47077  wallispi2lem1  47080  wallispi2lem2  47081  wallispi2  47082  stirlinglem11  47093  dirkertrigeqlem1  47107  fouriersw  47240  goldratval  47935  fmtnorec4  48633  lighneallem2  48690  lighneallem3  48691  3exp4mod41  48700  opoeALTV  48780  fppr2odd  48828  8exp8mod9  48833  ackval2  49793  ackval2012  49802