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

Theorem 5re 9208
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 9194 . 2  |-  5  =  ( 4  +  1 )
2 4re 9206 . . 3  |-  4  e.  RR
3 1re 8263 . . 3  |-  1  e.  RR
42, 3readdcli 8276 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2135 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1522  (class class class)co 5366   RRcr 8163   1c1 8165    + caddc 8167   4c4 9184   5c5 9185
This theorem is referenced by:  6re  9209  6pos  9221  5p2e7  9246  5p3e8  9247  5p4e9  9248  5p5e10  9249  5t2e10  9261  3lt5  9279  2lt5  9280  1lt5  9281  5lt6  9282  4lt6  9283  5lt7  9288  4lt7  9289  5lt8  9295  4lt8  9296  5lt9  9303  4lt9  9304  5lt10  9312  4lt10  9313  ef01bndlem  11663  prmlem1  12229  sralem  14652  srasca  14656  zlmlem  15195  zlmsca  15199  ppiublem1  19012  ppiub  19014  bposlem3  19096  bposlem4  19097  bposlem5  19098  bposlem6  19099  bposlem8  19101  bposlem9  19102  lgsdir2lem1  19133  ex-id  19373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-17 1529  ax-12o 1563  ax-10 1577  ax-9 1583  ax-4 1590  ax-16 1776  ax-ext 2047  ax-1cn 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-mulrcl 8226  ax-i2m1 8231  ax-1ne0 8232  ax-rrecex 8235  ax-cnre 8236
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1447  df-sb 1737  df-clab 2053  df-cleq 2058  df-clel 2061  df-ne 2185  df-ral 2279  df-rex 2280  df-rab 2282  df-v 2478  df-dif 2797  df-un 2799  df-in 2801  df-ss 2805  df-nul 3074  df-if 3183  df-sn 3262  df-pr 3263  df-op 3265  df-uni 3431  df-br 3593  df-opab 3647  df-xp 4276  df-cnv 4278  df-dm 4280  df-rn 4281  df-res 4282  df-ima 4283  df-fv 4290  df-ov 5369  df-2 9191  df-3 9192  df-4 9193  df-5 9194
Copyright terms: Public domain