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

Theorem 5re 7725
Description: The number 5 is real.
Assertion
Ref Expression
5re |- 5 e. RR

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7714 . 2 |- 5 = (4 + 1)
2 4re 7724 . . 3 |- 4 e. RR
3 1re 7070 . . 3 |- 1 e. RR
42, 3readdcli 7066 . 2 |- (4 + 1) e. RR
51, 4eqeltri 2029 1 |- 5 e. RR
Colors of variables: wff set class
Syntax hints:   e. wcel 1459  (class class class)co 4928  RRcr 6963  1c1 6965   + caddc 6967  4c4 7704  5c5 7705
This theorem is referenced by:  6re 7726  6pos 7737  5p2e7 7753  5p3e8 7754  5p4e9 7755  5p5e10 7756  5t2e10 7767  3lt5 7785  2lt5 7786  1lt5 7787  5lt6 7788  4lt6 7789  5lt7 7794  4lt7 7795  5lt8 7801  4lt8 7802  ef01bndlem 9421  5t5e25 9818  prmlem1 9820  lmodlem2 10243  prmpiub 11953  bposlem3 11961  bposlem4 11962  bposlem5 11963  bposlem7 11965  bposlem8 11966  phllem 19314
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-1cn 7019  ax-icn 7020  ax-addcl 7021  ax-addrcl 7022  ax-mulcl 7023  ax-mulrcl 7024  ax-i2m1 7029  ax-1ne0 7030  ax-rrecex 7033  ax-cnre 7034
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1633  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-v 2367  df-un 2667  df-in 2669  df-ss 2671  df-sn 3101  df-pr 3102  df-op 3105  df-uni 3234  df-br 3379  df-opab 3433  df-xp 4016  df-cnv 4018  df-dm 4020  df-rn 4021  df-res 4022  df-ima 4023  df-fv 4030  df-ov 4930  df-2 7711  df-3 7712  df-4 7713  df-5 7714
Copyright terms: Public domain