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

Theorem 5re 8934
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 8923 . 2  |-  5  =  ( 4  +  1 )
2 4re 8933 . . 3  |-  4  e.  RR
3 1re 8258 . . 3  |-  1  e.  RR
42, 3readdcli 8254 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2131 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1519  (class class class)co 5353   RRcr 8146   1c1 8148    + caddc 8150   4c4 8913   5c5 8914
This theorem is referenced by:  6re  8935  6pos  8946  5p2e7  8970  5p3e8  8971  5p4e9  8972  5p5e10  8973  5t2e10  8984  3lt5  9002  2lt5  9003  1lt5  9004  5lt6  9005  4lt6  9006  5lt7  9011  4lt7  9012  5lt8  9018  4lt8  9019  5lt9  9026  4lt9  9027  5lt10  9035  4lt10  9036  ef01bndlem  11057  prmlem1  11591  sralem  13697  srasca  13701  zlmlem  14236  zlmsca  14240  ppiublem1  17989  ppiub  17991  bposlem3  18006  bposlem4  18007  bposlem5  18008  bposlem6  18009  bposlem8  18011  bposlem9  18012  lgsdir2lem1  18043  ex-id  18137
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-1cn 8204  ax-icn 8205  ax-addcl 8206  ax-addrcl 8207  ax-mulcl 8208  ax-mulrcl 8209  ax-i2m1 8214  ax-1ne0 8215  ax-rrecex 8218  ax-cnre 8219
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 895  df-ex 1444  df-sb 1733  df-clab 2049  df-cleq 2054  df-clel 2057  df-ne 2181  df-ral 2275  df-rex 2276  df-rab 2278  df-v 2474  df-dif 2793  df-un 2795  df-in 2797  df-ss 2801  df-nul 3070  df-if 3178  df-sn 3257  df-pr 3258  df-op 3260  df-uni 3421  df-br 3583  df-opab 3637  df-xp 4266  df-cnv 4268  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-fv 4280  df-ov 5356  df-2 8920  df-3 8921  df-4 8922  df-5 8923
Copyright terms: Public domain