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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8023 . 2
2 4re 8033 . . 3
3 1re 7364 . . 3
42, 3readdcli 7360 . 2
51, 4eqeltri 1987 1
Colors of variables: wff set class
Syntax hints:   wcel 1416  (class class class)co 5032  cr 7256  c1 7258   caddc 7260  c4 8013  c5 8014
This theorem is referenced by:  6re 8035  6pos 8046  5p2e7 8070  5p3e8 8071  5p4e9 8072  5p5e10 8073  5t2e10 8084  3lt5 8102  2lt5 8103  1lt5 8104  5lt6 8105  4lt6 8106  5lt7 8111  4lt7 8112  5lt8 8118  4lt8 8119  5lt9 8126  4lt9 8127  5lt10 8135  4lt10 8136  ef01bndlem 9949  prmlem1 10457  ppiublem 14699  ppiub 14700  bposlem3 14715  bposlem4 14716  bposlem5 14717  bposlem6 14718  bposlem8 14720  bposlem9 14721  lgsdir2lem1 16682  mgpsca 19919  phllem 23617
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-addrcl 7315  ax-mulcl 7316  ax-mulrcl 7317  ax-i2m1 7322  ax-1ne0 7323  ax-rrecex 7326  ax-cnre 7327
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-rab 2134  df-v 2329  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-nul 2908  df-if 3015  df-sn 3092  df-pr 3093  df-op 3095  df-uni 3247  df-br 3397  df-opab 3450  df-xp 4048  df-cnv 4050  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fv 4062  df-ov 5034  df-2 8020  df-3 8021  df-4 8022  df-5 8023
Copyright terms: Public domain