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

Theorem 4re 9835
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 9822 . 2  |-  4  =  ( 3  +  1 )
2 3re 9833 . . 3  |-  3  e.  RR
3 1re 8853 . . 3  |-  1  e.  RR
42, 3readdcli 8866 . 2  |-  ( 3  +  1 )  e.  RR
51, 4eqeltri 2366 1  |-  4  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1696  (class class class)co 5874   RRcr 8752   1c1 8754    + caddc 8756   3c3 9812   4c4 9813
This theorem is referenced by:  4cn  9836  5re  9837  5pos  9849  2lt4  9906  1lt4  9907  4lt5  9908  3lt5  9909  2lt5  9910  1lt5  9911  4lt6  9913  3lt6  9914  4lt7  9919  3lt7  9920  4lt8  9926  3lt8  9927  4lt9  9934  3lt9  9935  4lt10  9943  3lt10  9944  8th4div3  9951  iexpcyc  11223  discr  11254  faclbnd2  11320  sqr2gt1lt2  11776  amgm2  11869  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  cos2bnd  12484  4sqlem12  13019  pcoass  18538  minveclem2  18806  uniioombllem5  18958  dveflem  19342  pilem2  19844  pilem3  19845  sinhalfpilem  19850  sincosq1lem  19881  tangtx  19889  sincos4thpi  19897  sincos6thpi  19899  log2cnv  20256  ppiublem1  20457  chtublem  20466  bposlem2  20540  bposlem6  20544  bposlem7  20545  bposlem8  20546  bposlem9  20547  2sqlem11  20630  chebbnd1lem2  20635  chebbnd1lem3  20636  chebbnd1  20637  pntibndlem1  20754  pntlemb  20762  pntlemg  20763  pntlemr  20767  pntlemf  20770  ex-id  20837  ex-1st  20847  ex-2nd  20848  4ipval2  21297  4ipval3  21301  ipidsq  21302  dipcl  21304  dipcj  21306  dip0r  21309  ip1ilem  21420  ipasslem10  21433  minvecolem2  21470  minvecolem3  21471  normlem6  21710  polid2i  21752  lnopeq0i  22603  lnophmlem2  22613  sqsscirc1  23307  4bc2eq6  24114  bpoly3  24865  bpoly4  24866  csbrn  26565  stoweidlem13  27865  stoweidlem26  27878  stoweidlem34  27886  stoweid  27915  stirlinglem12  27937  stirlinglem13  27938  fzo0to42pr  28211  usgraexvlem  28261  4cycl4v4e  28412  4cycl4dv4e  28414  2p2ne5  28517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-2 9820  df-3 9821  df-4 9822
  Copyright terms: Public domain W3C validator