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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7753 . 2 |- 5 = (4 + 1)
2 4re 7763 . . 3 |- 4 e. RR
3 1re 7105 . . 3 |- 1 e. RR
42, 3readdcli 7101 . 2 |- (4 + 1) e. RR
51, 4eqeltri 2030 1 |- 5 e. RR
Colors of variables: wff set class
Syntax hints:   e. wcel 1459  (class class class)co 4935  RRcr 6998  1c1 7000   + caddc 7002  4c4 7743  5c5 7744
This theorem is referenced by:  6re 7765  6pos 7776  5p2e7 7792  5p3e8 7793  5p4e9 7794  5p5e10 7795  5t2e10 7806  3lt5 7824  2lt5 7825  1lt5 7826  5lt6 7827  4lt6 7828  5lt7 7833  4lt7 7834  5lt8 7840  4lt8 7841  ef01bndlem 9435  5t5e25 9842  prmlem1 9844  lmodlem2 10267  prmpiub 12544  bposlem3 12552  bposlem4 12553  bposlem5 12554  bposlem6 12555  bposlem8 12557  bposlem9 12558  phllem 19518
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 1672  ax-ext 1943  ax-1cn 7054  ax-icn 7055  ax-addcl 7056  ax-addrcl 7057  ax-mulcl 7058  ax-mulrcl 7059  ax-i2m1 7064  ax-1ne0 7065  ax-rrecex 7068  ax-cnre 7069
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1634  df-clab 1949  df-cleq 1954  df-clel 1957  df-ne 2081  df-ral 2174  df-rex 2175  df-v 2368  df-un 2668  df-in 2670  df-ss 2672  df-sn 3102  df-pr 3103  df-op 3106  df-uni 3235  df-br 3380  df-opab 3434  df-xp 4022  df-cnv 4024  df-dm 4026  df-rn 4027  df-res 4028  df-ima 4029  df-fv 4036  df-ov 4937  df-2 7750  df-3 7751  df-4 7752  df-5 7753
Copyright terms: Public domain