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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7803 . 2 |- 5 = (4 + 1)
2 4re 7813 . . 3 |- 4 e. RR
3 1re 7195 . . 3 |- 1 e. RR
42, 3readdcli 7191 . 2 |- (4 + 1) e. RR
51, 4eqeltri 2148 1 |- 5 e. RR
Colors of variables: wff set class
Syntax hints:   e. wcel 1575  (class class class)co 5050  RRcr 7088  1c1 7090   + caddc 7092  4c4 7793  5c5 7794
This theorem is referenced by:  6re 7815  6pos 7826  5p2e7 7841  5p3e8 7842  5p4e9 7843  5p5e10 7844  5t2e10 7855  3lt5 7873  2lt5 7874  1lt5 7875  5lt6 7876  4lt6 7877  5lt7 7882  4lt7 7883  5lt8 7889  4lt8 7890  sin01bndlem1 9664  lmodlem1 10274  lmodlem2 10275  lmodlem3 10276  5t5e25 13765  prmlem1 13767  prmpiub 13814  bposlem3 13822  bposlem4 13823  bposlem5 13824  bposlem7 13826  bposlem8 13827  phllem1 19436  phllem2 19437
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1497  ax-6 1498  ax-7 1499  ax-gen 1500  ax-8 1577  ax-10 1578  ax-11 1579  ax-12 1580  ax-14 1582  ax-17 1589  ax-9 1603  ax-4 1609  ax-16 1786  ax-ext 2057  ax-sep 3592  ax-nul 3602  ax-pr 3662  ax-1cn 7144  ax-icn 7145  ax-addcl 7146  ax-addrcl 7147  ax-mulcl 7148  ax-mulrcl 7149  ax-i2m1 7154  ax-1ne0 7155  ax-rrecex 7158  ax-cnre 7159
This theorem depends on definitions:  df-bi 204  df-or 413  df-an 414  df-3an 1020  df-ex 1502  df-sb 1748  df-eu 1975  df-mo 1976  df-clab 2063  df-cleq 2068  df-clel 2071  df-ne 2203  df-ral 2297  df-rex 2298  df-v 2484  df-dif 2787  df-un 2789  df-in 2791  df-ss 2793  df-nul 3049  df-sn 3220  df-pr 3221  df-op 3224  df-uni 3348  df-br 3493  df-opab 3551  df-xp 4134  df-cnv 4136  df-dm 4138  df-rn 4139  df-res 4140  df-ima 4141  df-fv 4148  df-opr 5052  df-2 7800  df-3 7801  df-4 7802  df-5 7803
Copyright terms: Public domain