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

Theorem 5re 8685
Description: The number 5 is real.
Assertion
Ref Expression
5re

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8674 . 2
2 4re 8684 . . 3
3 1re 8015 . . 3
42, 3readdcli 8011 . 2
51, 4eqeltri 2099 1
Colors of variables: wff set class
Syntax hints:   wcel 1528  (class class class)co 5206  cr 7907  c1 7909   caddc 7911  c4 8664  c5 8665
This theorem is referenced by:  6re 8686  6pos 8697  5p2e7 8721  5p3e8 8722  5p4e9 8723  5p5e10 8724  5t2e10 8735  3lt5 8753  2lt5 8754  1lt5 8755  5lt6 8756  4lt6 8757  5lt7 8762  4lt7 8763  5lt8 8769  4lt8 8770  5lt9 8777  4lt9 8778  5lt10 8786  4lt10 8787  ef01bndlem 10610  prmlem1 11121  mgpsca 12198  ppiublem 15704  ppiub 15705  bposlem3 15720  bposlem4 15721  bposlem5 15722  bposlem6 15723  bposlem8 15725  bposlem9 15726  lgsdir2lem1 15757  ex-id 15851  phllem 24217
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-addrcl 7966  ax-mulcl 7967  ax-mulrcl 7968  ax-i2m1 7973  ax-1ne0 7974  ax-rrecex 7977  ax-cnre 7978
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-rab 2246  df-v 2442  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-nul 3026  df-if 3135  df-sn 3214  df-pr 3215  df-op 3217  df-uni 3375  df-br 3532  df-opab 3585  df-xp 4186  df-cnv 4188  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fv 4200  df-ov 5208  df-2 8671  df-3 8672  df-4 8673  df-5 8674
Copyright terms: Public domain