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

Theorem 2t2e4 11790
Description: 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
Assertion
Ref Expression
2t2e4 (2 · 2) = 4

Proof of Theorem 2t2e4
StepHypRef Expression
1 2cn 11701 . . 3 2 ∈ ℂ
212timesi 11764 . 2 (2 · 2) = (2 + 2)
3 2p2e4 11761 . 2 (2 + 2) = 4
42, 3eqtri 2849 1 (2 · 2) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7148   + caddc 10529   · cmul 10531  2c2 11681  4c4 11683
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 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
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 6312  df-fv 6360  df-ov 7151  df-2 11689  df-3 11690  df-4 11691
This theorem is referenced by:  4d2e2  11796  halfpm6th  11847  div4p1lem1div2  11881  3halfnz  12050  decbin0  12227  fldiv4lem1div2uz2  13196  sq2  13550  sq4e2t8  13552  discr  13591  sqoddm1div8  13594  faclbnd2  13641  4bc2eq6  13679  amgm2  14719  bpoly3  15402  sin4lt0  15538  z4even  15713  flodddiv4  15754  flodddiv4t2lthalf  15757  4nprm  16029  2exp4  16411  2exp16  16414  5prm  16432  631prm  16450  1259lem1  16454  1259lem4  16457  2503lem1  16460  2503lem2  16461  2503lem3  16462  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001prm  16468  pcoass  23543  minveclem2  23944  uniioombllem5  24103  uniioombl  24105  dveflem  24491  pilem2  24955  sinhalfpilem  24964  sincosq1lem  24998  tangtx  25006  sincos4thpi  25014  heron  25329  quad2  25330  dquartlem1  25342  dquart  25344  quart1  25347  atan1  25419  log2ublem3  25440  log2ub  25441  chtub  25702  bclbnd  25770  bpos1  25773  bposlem2  25775  bposlem6  25779  bposlem9  25782  gausslemma2dlem3  25858  m1lgs  25878  2lgslem1a2  25880  2lgslem3a  25886  2lgslem3b  25887  2lgslem3c  25888  2lgslem3d  25889  pntibndlem2  26081  pntlemg  26088  pntlemr  26092  ex-fl  28140  minvecolem2  28566  polid2i  28848  quad3  32797  3cubeslem3l  39148  3cubeslem3r  39149  wallispi2lem1  42222  wallispi2lem2  42223  stirlinglem3  42227  stirlinglem10  42234  fmtnorec4  43543  2exp340mod341  43730  8exp8mod9  43733
  Copyright terms: Public domain W3C validator