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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7748 . 2 |- 5 = (4 + 1)
2 4re 7758 . . 3 |- 4 e. RR
3 1re 7098 . . 3 |- 1 e. RR
42, 3readdcli 7094 . 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 4922  RRcr 6991  1c1 6993   + caddc 6995  4c4 7738  5c5 7739
This theorem is referenced by:  6re 7760  6pos 7771  5p2e7 7787  5p3e8 7788  5p4e9 7789  5p5e10 7790  5t2e10 7801  3lt5 7819  2lt5 7820  1lt5 7821  5lt6 7822  4lt6 7823  5lt7 7828  4lt7 7829  5lt8 7835  4lt8 7836  ef01bndlem 9502  5t5e25 9950  prmlem1 9952  lmodlem1 10401  lmodlem2 10402  ppiublem 12875  ppiub 12876  bposlem3 12909  bposlem4 12910  bposlem5 12911  bposlem6 12912  bposlem8 12914  bposlem9 12915  phllem 19863
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 7047  ax-icn 7048  ax-addcl 7049  ax-addrcl 7050  ax-mulcl 7051  ax-mulrcl 7052  ax-i2m1 7057  ax-1ne0 7058  ax-rrecex 7061  ax-cnre 7062
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 3084  df-pr 3085  df-op 3087  df-uni 3218  df-br 3363  df-opab 3417  df-xp 4009  df-cnv 4011  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fv 4023  df-ov 4924  df-2 7745  df-3 7746  df-4 7747  df-5 7748
Copyright terms: Public domain