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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7819 . 2 |- 5 = (4 + 1)
2 4re 7829 . . 3 |- 4 e. RR
3 1re 7212 . . 3 |- 1 e. RR
42, 3readdcli 7208 . 2 |- (4 + 1) e. RR
51, 4eqeltri 2165 1 |- 5 e. RR
Colors of variables: wff set class
Syntax hints:   e. wcel 1594  (class class class)co 5067  RRcr 7105  1c1 7107   + caddc 7109  4c4 7809  5c5 7810
This theorem is referenced by:  6re 7831  6pos 7842  5p2e7 7857  5p3e8 7858  5p4e9 7859  5p5e10 7860  5t2e10 7871  3lt5 7889  2lt5 7890  1lt5 7891  5lt6 7892  4lt6 7893  5lt7 7898  4lt7 7899  5lt8 7905  4lt8 7906  sin01bndlem1 9679  lmodlem1 10262  lmodlem2 10263  lmodlem3 10264  5t5e25 13728  prmlem1 13730  prmpiub 13777  bposlem3 13785  bposlem4 13786  bposlem5 13787  bposlem7 13789  bposlem8 13790  phllem1 19214  phllem2 19215
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609  ax-nul 3619  ax-pr 3679  ax-1cn 7161  ax-icn 7162  ax-addcl 7163  ax-addrcl 7164  ax-mulcl 7165  ax-mulrcl 7166  ax-i2m1 7171  ax-1ne0 7172  ax-rrecex 7175  ax-cnre 7176
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-v 2501  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-nul 3066  df-sn 3237  df-pr 3238  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-xp 4151  df-cnv 4153  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fv 4165  df-opr 5069  df-2 7816  df-3 7817  df-4 7818  df-5 7819
Copyright terms: Public domain