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

Theorem 5re 9196
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 9185 . 2  |-  5  =  ( 4  +  1 )
2 4re 9195 . . 3  |-  4  e.  RR
3 1re 8255 . . 3  |-  1  e.  RR
42, 3readdcli 8268 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2134 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1522  (class class class)co 5360   RRcr 8157   1c1 8159    + caddc 8161   4c4 9175   5c5 9176
This theorem is referenced by:  6re  9197  6pos  9208  5p2e7  9232  5p3e8  9233  5p4e9  9234  5p5e10  9235  5t2e10  9246  3lt5  9264  2lt5  9265  1lt5  9266  5lt6  9267  4lt6  9268  5lt7  9273  4lt7  9274  5lt8  9280  4lt8  9281  5lt9  9288  4lt9  9289  5lt10  9297  4lt10  9298  ef01bndlem  11647  prmlem1  12213  sralem  14635  srasca  14639  zlmlem  15178  zlmsca  15182  ppiublem1  18995  ppiub  18997  bposlem3  19079  bposlem4  19080  bposlem5  19081  bposlem6  19082  bposlem8  19084  bposlem9  19085  lgsdir2lem1  19116  ex-id  19354
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 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-1cn 8215  ax-icn 8216  ax-addcl 8217  ax-addrcl 8218  ax-mulcl 8219  ax-mulrcl 8220  ax-i2m1 8225  ax-1ne0 8226  ax-rrecex 8229  ax-cnre 8230
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1447  df-sb 1736  df-clab 2052  df-cleq 2057  df-clel 2060  df-ne 2184  df-ral 2278  df-rex 2279  df-rab 2281  df-v 2477  df-dif 2796  df-un 2798  df-in 2800  df-ss 2804  df-nul 3073  df-if 3182  df-sn 3261  df-pr 3262  df-op 3264  df-uni 3425  df-br 3587  df-opab 3641  df-xp 4270  df-cnv 4272  df-dm 4274  df-rn 4275  df-res 4276  df-ima 4277  df-fv 4284  df-ov 5363  df-2 9182  df-3 9183  df-4 9184  df-5 9185
Copyright terms: Public domain