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

Theorem 2t2e4 12275
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 12186 . . 3 2 ∈ ℂ
212timesi 12249 . 2 (2 · 2) = (2 + 2)
3 2p2e4 12246 . 2 (2 + 2) = 4
42, 3eqtri 2765 1 (2 · 2) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7351   + caddc 11012   · cmul 11014  2c2 12166  4c4 12168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6445  df-fv 6501  df-ov 7354  df-2 12174  df-3 12175  df-4 12176
This theorem is referenced by:  4d2e2  12281  halfpm6th  12332  div4p1lem1div2  12366  3halfnz  12540  decbin0  12716  fldiv4lem1div2uz2  13695  sq2  14055  sq4e2t8  14057  discr  14097  sqoddm1div8  14100  faclbnd2  14145  4bc2eq6  14183  amgm2  15214  bpoly3  15901  sin4lt0  16037  z4even  16214  flodddiv4  16255  flodddiv4t2lthalf  16258  4nprm  16531  2exp4  16917  2exp16  16923  5prm  16941  631prm  16959  1259lem1  16963  1259lem4  16966  2503lem1  16969  2503lem2  16970  2503lem3  16971  4001lem1  16973  4001lem2  16974  4001lem3  16975  4001prm  16977  pcoass  24339  minveclem2  24742  uniioombllem5  24903  uniioombl  24905  dveflem  25295  pilem2  25763  sinhalfpilem  25772  sincosq1lem  25806  tangtx  25814  sincos4thpi  25822  heron  26140  quad2  26141  dquartlem1  26153  dquart  26155  quart1  26158  atan1  26230  log2ublem3  26250  log2ub  26251  chtub  26512  bclbnd  26580  bpos1  26583  bposlem2  26585  bposlem6  26589  bposlem9  26592  gausslemma2dlem3  26668  m1lgs  26688  2lgslem1a2  26690  2lgslem3a  26696  2lgslem3b  26697  2lgslem3c  26698  2lgslem3d  26699  pntibndlem2  26891  pntlemg  26898  pntlemr  26902  ex-fl  29220  minvecolem2  29646  polid2i  29928  quad3  34070  420lcm8e840  40406  3exp7  40448  3lexlogpow5ineq1  40449  3lexlogpow2ineq2  40454  3lexlogpow5ineq5  40455  aks4d1p1p2  40465  aks4d1p1  40471  2ap1caineq  40491  flt4lem  40892  3cubeslem3l  40918  3cubeslem3r  40919  wallispi2lem1  44213  wallispi2lem2  44214  stirlinglem3  44218  stirlinglem10  44225  fmtnorec4  45642  2exp340mod341  45826  8exp8mod9  45829  ackval2012  46678
  Copyright terms: Public domain W3C validator