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 7104 . . 3 |- 1 e. RR
42, 3readdcli 7100 . 2 |- (4 + 1) e. RR
51, 4eqeltri 2022 1 |- 5 e. RR
Colors of variables: wff set class
Syntax hints:   e. wcel 1451  (class class class)co 4931  RRcr 6997  1c1 6999   + caddc 7001  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 9451  5t5e25 9864  prmlem1 9866  lmodlem2 10315  prmpiub 12712  bposlem3 12720  bposlem4 12721  bposlem5 12722  bposlem6 12723  bposlem8 12725  bposlem9 12726  phllem 19713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-1cn 7053  ax-icn 7054  ax-addcl 7055  ax-addrcl 7056  ax-mulcl 7057  ax-mulrcl 7058  ax-i2m1 7063  ax-1ne0 7064  ax-rrecex 7067  ax-cnre 7068
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3an 939  df-ex 1372  df-sb 1626  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-ral 2166  df-rex 2167  df-v 2360  df-un 2662  df-in 2664  df-ss 2666  df-sn 3096  df-pr 3097  df-op 3100  df-uni 3229  df-br 3374  df-opab 3428  df-xp 4018  df-cnv 4020  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fv 4032  df-ov 4933  df-2 7750  df-3 7751  df-4 7752  df-5 7753
Copyright terms: Public domain