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

Theorem 5re 8944
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 8933 . 2  |-  5  =  ( 4  +  1 )
2 4re 8943 . . 3  |-  4  e.  RR
3 1re 8264 . . 3  |-  1  e.  RR
42, 3readdcli 8260 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2132 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1520  (class class class)co 5356   RRcr 8152   1c1 8154    + caddc 8156   4c4 8923   5c5 8924
This theorem is referenced by:  6re  8945  6pos  8956  5p2e7  8980  5p3e8  8981  5p4e9  8982  5p5e10  8983  5t2e10  8994  3lt5  9012  2lt5  9013  1lt5  9014  5lt6  9015  4lt6  9016  5lt7  9021  4lt7  9022  5lt8  9028  4lt8  9029  5lt9  9036  4lt9  9037  5lt10  9045  4lt10  9046  ef01bndlem  11116  prmlem1  11679  sralem  14098  srasca  14102  zlmlem  14641  zlmsca  14645  ppiublem1  18383  ppiub  18385  bposlem3  18459  bposlem4  18460  bposlem5  18461  bposlem6  18462  bposlem8  18464  bposlem9  18465  lgsdir2lem1  18496  ex-id  18644
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587  ax-16 1773  ax-ext 2044  ax-1cn 8210  ax-icn 8211  ax-addcl 8212  ax-addrcl 8213  ax-mulcl 8214  ax-mulrcl 8215  ax-i2m1 8220  ax-1ne0 8221  ax-rrecex 8224  ax-cnre 8225
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 896  df-ex 1445  df-sb 1734  df-clab 2050  df-cleq 2055  df-clel 2058  df-ne 2182  df-ral 2276  df-rex 2277  df-rab 2279  df-v 2475  df-dif 2794  df-un 2796  df-in 2798  df-ss 2802  df-nul 3071  df-if 3180  df-sn 3259  df-pr 3260  df-op 3262  df-uni 3423  df-br 3585  df-opab 3639  df-xp 4268  df-cnv 4270  df-dm 4272  df-rn 4273  df-res 4274  df-ima 4275  df-fv 4282  df-ov 5359  df-2 8930  df-3 8931  df-4 8932  df-5 8933
Copyright terms: Public domain