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

Theorem 2t1e2 11388
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 11303 . 2 2 ∈ ℂ
21mulid1i 10254 1 (2 · 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6814  1c1 10149   · cmul 10153  2c2 11282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rrecex 10220  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-2 11291
This theorem is referenced by:  decbin2  11895  expubnd  13135  sqrlem7  14208  trirecip  14814  bpoly3  15008  fsumcube  15010  ege2le3  15039  cos2tsin  15128  cos2bnd  15137  odd2np1  15287  opoe  15309  flodddiv4  15359  pythagtriplem4  15746  2503lem2  16067  2503lem3  16068  4001lem4  16073  4001prm  16074  htpycc  23000  pco1  23035  pcohtpylem  23039  pcopt  23042  pcorevlem  23046  ovolunlem1a  23484  cos2pi  24448  coskpi  24492  dcubic1lem  24790  dcubic2  24791  dcubic  24793  mcubic  24794  basellem3  25029  chtublem  25156  bcp1ctr  25224  bclbnd  25225  bposlem1  25229  bposlem2  25230  bposlem5  25233  2lgslem3d1  25348  chebbnd1lem1  25378  chebbnd1lem3  25380  chebbnd1  25381  frgrregord013  27584  ex-ind-dvds  27650  knoppndvlem12  32841  heiborlem6  33946  jm2.23  38083  sumnnodd  40383  wallispilem4  40806  wallispi2lem1  40809  wallispi2lem2  40810  wallispi2  40811  stirlinglem11  40822  dirkertrigeqlem1  40836  fouriersw  40969  fmtnorec4  41989  lighneallem2  42051  lighneallem3  42052  3exp4mod41  42061  opoeALTV  42122
  Copyright terms: Public domain W3C validator