MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4re Structured version   Unicode version

Theorem 4re 10619
Description: The number 4 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
4re  |-  4  e.  RR

Proof of Theorem 4re
StepHypRef Expression
1 df-4 10603 . 2  |-  4  =  ( 3  +  1 )
2 3re 10616 . . 3  |-  3  e.  RR
3 1re 9598 . . 3  |-  1  e.  RR
42, 3readdcli 9612 . 2  |-  ( 3  +  1 )  e.  RR
51, 4eqeltri 2527 1  |-  4  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804  (class class class)co 6281   RRcr 9494   1c1 9496    + caddc 9498   3c3 10593   4c4 10594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-2 10601  df-3 10602  df-4 10603
This theorem is referenced by:  4cn  10620  5re  10621  4ne0  10639  5pos  10640  2lt4  10713  1lt4  10714  4lt5  10715  3lt5  10716  2lt5  10717  1lt5  10718  4lt6  10720  3lt6  10721  4lt7  10726  3lt7  10727  4lt8  10733  3lt8  10734  4lt9  10741  3lt9  10742  4lt10  10750  3lt10  10751  fzo0to42pr  11882  iexpcyc  12253  discr  12284  faclbnd2  12350  sqrt2gt1lt2  13089  amgm2  13183  ef01bndlem  13900  sin01bnd  13901  cos01bnd  13902  cos2bnd  13904  4sqlem12  14455  pcoass  21501  csbren  21803  minveclem2  21818  uniioombllem5  21973  dveflem  22357  pilem2  22823  pilem3  22824  sinhalfpilem  22832  sincosq1lem  22866  tangtx  22874  sincos4thpi  22882  log2cnv  23251  ppiublem1  23453  chtublem  23462  bposlem2  23536  bposlem6  23540  bposlem7  23541  bposlem8  23542  bposlem9  23543  2sqlem11  23626  chebbnd1lem2  23631  chebbnd1lem3  23632  chebbnd1  23633  pntibndlem1  23750  pntlemb  23758  pntlemg  23759  pntlemr  23763  pntlemf  23766  usgraexvlem  24371  usgraex0elv  24372  usgraex1elv  24373  usgraex2elv  24374  usgraex3elv  24375  4cycl4v4e  24642  4cycl4dv4e  24644  ex-id  25131  ex-1st  25141  ex-2nd  25142  dipcj  25603  minvecolem2  25767  minvecolem3  25768  normlem6  26008  lnophmlem2  26912  sqsscirc1  27867  problem2  28997  problem3  28998  4bc2eq6  29089  bpoly4  29796  limclner  31565  stoweidlem13  31684  stoweidlem26  31697  stoweidlem34  31705  stoweid  31734  stirlinglem12  31756  stirlinglem13  31757  2p2ne5  32948
  Copyright terms: Public domain W3C validator