HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8913 . 2  |-  5  =  ( 4  +  1 )
2 4re 8923 . . 3  |-  4  e.  RR
3 1re 8248 . . 3  |-  1  e.  RR
42, 3readdcli 8244 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2151 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1538  (class class class)co 5354   RRcr 8136   1c1 8138    + caddc 8140   4c4 8903   5c5 8904
This theorem is referenced by:  6re  8925  6pos  8936  5p2e7  8960  5p3e8  8961  5p4e9  8962  5p5e10  8963  5t2e10  8974  3lt5  8992  2lt5  8993  1lt5  8994  5lt6  8995  4lt6  8996  5lt7  9001  4lt7  9002  5lt8  9008  4lt8  9009  5lt9  9016  4lt9  9017  5lt10  9025  4lt10  9026  ef01bndlem  11029  prmlem1  11563  sralem  13606  srasca  13610  zlmlem  14145  zlmsca  14149  ppiublem1  17898  ppiub  17900  bposlem3  17915  bposlem4  17916  bposlem5  17917  bposlem6  17918  bposlem8  17920  bposlem9  17921  lgsdir2lem1  17952  ex-id  18046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-1cn 8194  ax-icn 8195  ax-addcl 8196  ax-addrcl 8197  ax-mulcl 8198  ax-mulrcl 8199  ax-i2m1 8204  ax-1ne0 8205  ax-rrecex 8208  ax-cnre 8209
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 905  df-ex 1456  df-sb 1754  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-ral 2295  df-rex 2296  df-rab 2298  df-v 2494  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3089  df-if 3199  df-sn 3278  df-pr 3279  df-op 3281  df-uni 3439  df-br 3601  df-opab 3655  df-xp 4289  df-cnv 4291  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fv 4303  df-ov 5357  df-2 8910  df-3 8911  df-4 8912  df-5 8913
Copyright terms: Public domain