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

Theorem 4re 9819
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 9806 . 2  |-  4  =  ( 3  +  1 )
2 3re 9817 . . 3  |-  3  e.  RR
3 1re 8837 . . 3  |-  1  e.  RR
42, 3readdcli 8850 . 2  |-  ( 3  +  1 )  e.  RR
51, 4eqeltri 2353 1  |-  4  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1684  (class class class)co 5858   RRcr 8736   1c1 8738    + caddc 8740   3c3 9796   4c4 9797
This theorem is referenced by:  4cn  9820  5re  9821  5pos  9833  2lt4  9890  1lt4  9891  4lt5  9892  3lt5  9893  2lt5  9894  1lt5  9895  4lt6  9897  3lt6  9898  4lt7  9903  3lt7  9904  4lt8  9910  3lt8  9911  4lt9  9918  3lt9  9919  4lt10  9927  3lt10  9928  8th4div3  9935  iexpcyc  11207  discr  11238  faclbnd2  11304  sqr2gt1lt2  11760  amgm2  11853  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  cos2bnd  12468  4sqlem12  13003  pcoass  18522  minveclem2  18790  uniioombllem5  18942  dveflem  19326  pilem2  19828  pilem3  19829  sinhalfpilem  19834  sincosq1lem  19865  tangtx  19873  sincos4thpi  19881  sincos6thpi  19883  log2cnv  20240  ppiublem1  20441  chtublem  20450  bposlem2  20524  bposlem6  20528  bposlem7  20529  bposlem8  20530  bposlem9  20531  2sqlem11  20614  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  pntibndlem1  20738  pntlemb  20746  pntlemg  20747  pntlemr  20751  pntlemf  20754  ex-id  20821  ex-1st  20831  ex-2nd  20832  4ipval2  21281  4ipval3  21285  ipidsq  21286  dipcl  21288  dipcj  21290  dip0r  21293  ip1ilem  21404  ipasslem10  21417  minvecolem2  21454  minvecolem3  21455  normlem6  21694  polid2i  21736  lnopeq0i  22587  lnophmlem2  22597  sqsscirc1  23292  4bc2eq6  24099  bpoly3  24793  bpoly4  24794  csbrn  26462  stoweidlem13  27762  stoweidlem26  27775  stoweidlem34  27783  stoweid  27812  stirlinglem12  27834  stirlinglem13  27835  usgraexvlem  28127  2p2ne5  28260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-2 9804  df-3 9805  df-4 9806
  Copyright terms: Public domain W3C validator