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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7863 . 2
2 4re 7873 . . 3
3 1re 7213 . . 3
42, 3readdcli 7209 . 2
51, 4eqeltri 1986 1
Colors of variables: wff set class
Syntax hints:   wcel 1415  (class class class)co 4944  cr 7106  c1 7108   caddc 7110  c4 7853  c5 7854
This theorem is referenced by:  6re 7875  6pos 7886  5p2e7 7902  5p3e8 7903  5p4e9 7904  5p5e10 7905  5t2e10 7916  3lt5 7934  2lt5 7935  1lt5 7936  5lt6 7937  4lt6 7938  5lt7 7943  4lt7 7944  5lt8 7950  4lt8 7951  ef01bndlem 9636  5t5e25 10095  prmlem1 10097  lmodlem1 10203  lmodlem2 10204  algfn 10211  ppiublem 13506  ppiub 13507  bposlem3 13540  bposlem4 13541  bposlem5 13542  bposlem6 13543  bposlem8 13545  bposlem9 13546  phllem 21555
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-i2m1 7172  ax-1ne0 7173  ax-rrecex 7176  ax-cnre 7177
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-v 2324  df-un 2637  df-in 2639  df-ss 2641  df-sn 3079  df-pr 3080  df-op 3082  df-uni 3214  df-br 3359  df-opab 3413  df-xp 4009  df-cnv 4011  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fv 4023  df-ov 4946  df-2 7860  df-3 7861  df-4 7862  df-5 7863
Copyright terms: Public domain