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

Theorem 2t1e2 12323
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 12235 . 2 2 ∈ ℂ
21mulid1i 11166 1 (2 · 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7362  1c1 11059   · cmul 11063  2c2 12215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-mulcl 11120  ax-mulcom 11122  ax-mulass 11124  ax-distr 11125  ax-1rid 11128  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12223
This theorem is referenced by:  decbin2  12766  expubnd  14089  01sqrexlem7  15140  trirecip  15755  bpoly3  15948  fsumcube  15950  ege2le3  15979  cos2tsin  16068  cos2bnd  16077  odd2np1  16230  opoe  16252  flodddiv4  16302  2mulprm  16576  pythagtriplem4  16698  2503lem2  17017  2503lem3  17018  4001lem4  17023  4001prm  17024  htpycc  24359  pco1  24394  pcohtpylem  24398  pcopt  24401  pcorevlem  24405  ovolunlem1a  24876  cos2pi  25849  coskpi  25895  dcubic2  26210  dcubic  26212  basellem3  26448  chtublem  26575  bcp1ctr  26643  bclbnd  26644  bposlem1  26648  bposlem2  26649  bposlem5  26652  2lgslem3d1  26767  2sqreultlem  26811  2sqreunnltlem  26814  chebbnd1lem1  26833  chebbnd1lem3  26835  chebbnd1  26836  frgrregord013  29381  ex-ind-dvds  29447  wrdt2ind  31849  knoppndvlem12  35015  heiborlem6  36304  3lexlogpow5ineq1  40540  aks4d1p1  40562  2np3bcnp1  40581  2ap1caineq  40582  flt4lem7  41026  jm2.23  41349  sumnnodd  43945  wallispilem4  44383  wallispi2lem1  44386  wallispi2lem2  44387  wallispi2  44388  stirlinglem11  44399  dirkertrigeqlem1  44413  fouriersw  44546  fmtnorec4  45815  lighneallem2  45872  lighneallem3  45873  3exp4mod41  45882  opoeALTV  45949  fppr2odd  45997  8exp8mod9  46002  ackval2  46842  ackval2012  46851
  Copyright terms: Public domain W3C validator