MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2t1e2 Structured version   Visualization version   GIF version

Theorem 2t1e2 12316
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
StepHypRef Expression
1 2cn 12228 . 2 2 ∈ ℂ
21mulid1i 11159 1 (2 · 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7357  1c1 11052   · cmul 11056  2c2 12208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-mulcl 11113  ax-mulcom 11115  ax-mulass 11117  ax-distr 11118  ax-1rid 11121  ax-cnre 11124
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-2 12216
This theorem is referenced by:  decbin2  12759  expubnd  14082  01sqrexlem7  15133  trirecip  15748  bpoly3  15941  fsumcube  15943  ege2le3  15972  cos2tsin  16061  cos2bnd  16070  odd2np1  16223  opoe  16245  flodddiv4  16295  2mulprm  16569  pythagtriplem4  16691  2503lem2  17010  2503lem3  17011  4001lem4  17016  4001prm  17017  htpycc  24343  pco1  24378  pcohtpylem  24382  pcopt  24385  pcorevlem  24389  ovolunlem1a  24860  cos2pi  25833  coskpi  25879  dcubic2  26194  dcubic  26196  basellem3  26432  chtublem  26559  bcp1ctr  26627  bclbnd  26628  bposlem1  26632  bposlem2  26633  bposlem5  26636  2lgslem3d1  26751  2sqreultlem  26795  2sqreunnltlem  26798  chebbnd1lem1  26817  chebbnd1lem3  26819  chebbnd1  26820  frgrregord013  29339  ex-ind-dvds  29405  wrdt2ind  31807  knoppndvlem12  34986  heiborlem6  36275  3lexlogpow5ineq1  40511  aks4d1p1  40533  2np3bcnp1  40552  2ap1caineq  40553  flt4lem7  40983  jm2.23  41306  sumnnodd  43861  wallispilem4  44299  wallispi2lem1  44302  wallispi2lem2  44303  wallispi2  44304  stirlinglem11  44315  dirkertrigeqlem1  44329  fouriersw  44462  fmtnorec4  45731  lighneallem2  45788  lighneallem3  45789  3exp4mod41  45798  opoeALTV  45865  fppr2odd  45913  8exp8mod9  45918  ackval2  46758  ackval2012  46767
  Copyright terms: Public domain W3C validator