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

Theorem 2t1e2 11794
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 11706 . 2 2 ∈ ℂ
21mulid1i 10639 1 (2 · 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7150  1c1 10532   · cmul 10536  2c2 11686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-mulcl 10593  ax-mulcom 10595  ax-mulass 10597  ax-distr 10598  ax-1rid 10601  ax-cnre 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6313  df-fv 6362  df-ov 7153  df-2 11694
This theorem is referenced by:  decbin2  12233  expubnd  13536  sqrlem7  14603  trirecip  15213  bpoly3  15407  fsumcube  15409  ege2le3  15438  cos2tsin  15527  cos2bnd  15536  odd2np1  15685  opoe  15707  flodddiv4  15759  2mulprm  16032  pythagtriplem4  16151  2503lem2  16466  2503lem3  16467  4001lem4  16472  4001prm  16473  htpycc  23518  pco1  23553  pcohtpylem  23557  pcopt  23560  pcorevlem  23564  ovolunlem1a  24031  cos2pi  24996  coskpi  25042  dcubic2  25354  dcubic  25356  basellem3  25593  chtublem  25720  bcp1ctr  25788  bclbnd  25789  bposlem1  25793  bposlem2  25794  bposlem5  25797  2lgslem3d1  25912  2sqreultlem  25956  2sqreunnltlem  25959  chebbnd1lem1  25978  chebbnd1lem3  25980  chebbnd1  25981  frgrregord013  28107  ex-ind-dvds  28173  wrdt2ind  30560  knoppndvlem12  33765  heiborlem6  34981  jm2.23  39477  sumnnodd  41795  wallispilem4  42238  wallispi2lem1  42241  wallispi2lem2  42242  wallispi2  42243  stirlinglem11  42254  dirkertrigeqlem1  42268  fouriersw  42401  fmtnorec4  43562  lighneallem2  43622  lighneallem3  43623  3exp4mod41  43632  opoeALTV  43699  fppr2odd  43747  8exp8mod9  43752
  Copyright terms: Public domain W3C validator