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

Theorem 2t2e4 11789
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 11700 . . 3 2 ∈ ℂ
212timesi 11763 . 2 (2 · 2) = (2 + 2)
3 2p2e4 11760 . 2 (2 + 2) = 4
42, 3eqtri 2841 1 (2 · 2) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145   + caddc 10528   · cmul 10530  2c2 11680  4c4 11682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-1rid 10595  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-2 11688  df-3 11689  df-4 11690
This theorem is referenced by:  4d2e2  11795  halfpm6th  11846  div4p1lem1div2  11880  3halfnz  12049  decbin0  12226  fldiv4lem1div2uz2  13194  sq2  13548  sq4e2t8  13550  discr  13589  sqoddm1div8  13592  faclbnd2  13639  4bc2eq6  13677  amgm2  14717  bpoly3  15400  sin4lt0  15536  z4even  15711  flodddiv4  15752  flodddiv4t2lthalf  15755  4nprm  16027  2exp4  16409  2exp16  16412  5prm  16430  631prm  16448  1259lem1  16452  1259lem4  16455  2503lem1  16458  2503lem2  16459  2503lem3  16460  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001prm  16466  pcoass  23555  minveclem2  23956  uniioombllem5  24115  uniioombl  24117  dveflem  24503  pilem2  24967  sinhalfpilem  24976  sincosq1lem  25010  tangtx  25018  sincos4thpi  25026  heron  25343  quad2  25344  dquartlem1  25356  dquart  25358  quart1  25361  atan1  25433  log2ublem3  25453  log2ub  25454  chtub  25715  bclbnd  25783  bpos1  25786  bposlem2  25788  bposlem6  25792  bposlem9  25795  gausslemma2dlem3  25871  m1lgs  25891  2lgslem1a2  25893  2lgslem3a  25899  2lgslem3b  25900  2lgslem3c  25901  2lgslem3d  25902  pntibndlem2  26094  pntlemg  26101  pntlemr  26105  ex-fl  28153  minvecolem2  28579  polid2i  28861  quad3  32810  3cubeslem3l  39161  3cubeslem3r  39162  wallispi2lem1  42233  wallispi2lem2  42234  stirlinglem3  42238  stirlinglem10  42245  fmtnorec4  43588  2exp340mod341  43775  8exp8mod9  43778
  Copyright terms: Public domain W3C validator