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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7763 . 2 |- 5 = (4 + 1)
2 4re 7773 . . 3 |- 4 e. RR
3 1re 7113 . . 3 |- 1 e. RR
42, 3readdcli 7109 . 2 |- (4 + 1) e. RR
51, 4eqeltri 2007 1 |- 5 e. RR
Colors of variables: wff set class
Syntax hints:   e. wcel 1436  (class class class)co 4927  RRcr 7006  1c1 7008   + caddc 7010  4c4 7753  5c5 7754
This theorem is referenced by:  6re 7775  6pos 7786  5p2e7 7802  5p3e8 7803  5p4e9 7804  5p5e10 7805  5t2e10 7816  3lt5 7834  2lt5 7835  1lt5 7836  5lt6 7837  4lt6 7838  5lt7 7843  4lt7 7844  5lt8 7850  4lt8 7851  ef01bndlem 9517  5t5e25 9967  prmlem1 9969  lmodlem1 10422  lmodlem2 10423  ppiublem 12897  ppiub 12898  bposlem3 12931  bposlem4 12932  bposlem5 12933  bposlem6 12934  bposlem8 12936  bposlem9 12937  phllem 19885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-1cn 7062  ax-icn 7063  ax-addcl 7064  ax-addrcl 7065  ax-mulcl 7066  ax-mulrcl 7067  ax-i2m1 7072  ax-1ne0 7073  ax-rrecex 7076  ax-cnre 7077
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3an 923  df-ex 1356  df-sb 1611  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-ral 2151  df-rex 2152  df-v 2345  df-un 2647  df-in 2649  df-ss 2651  df-sn 3085  df-pr 3086  df-op 3088  df-uni 3219  df-br 3364  df-opab 3418  df-xp 4010  df-cnv 4012  df-dm 4014  df-rn 4015  df-res 4016  df-ima 4017  df-fv 4024  df-ov 4929  df-2 7760  df-3 7761  df-4 7762  df-5 7763
Copyright terms: Public domain