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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7972 . 2
2 4re 7982 . . 3
3 1re 7320 . . 3
42, 3readdcli 7316 . 2
51, 4eqeltri 1987 1
Colors of variables: wff set class
Syntax hints:   wcel 1416  (class class class)co 5004  cr 7213  c1 7215   caddc 7217  c4 7962  c5 7963
This theorem is referenced by:  6re 7984  6pos 7995  5p2e7 8011  5p3e8 8012  5p4e9 8013  5p5e10 8014  5t2e10 8025  3lt5 8043  2lt5 8044  1lt5 8045  5lt6 8046  4lt6 8047  5lt7 8052  4lt7 8053  5lt8 8059  4lt8 8060  5lt9 8067  4lt9 8068  5lt10 8076  4lt10 8077  ef01bndlem 9801  5t5e25 10263  prmlem1 10265  lmodlem1 10375  lmodlem2 10376  algfn 10383  ppiublem 14397  ppiub 14398  bposlem3 14431  bposlem4 14432  bposlem5 14433  bposlem6 14434  bposlem8 14436  bposlem9 14437  lgsdir2lem1 16173  phllem 22928
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 7269  ax-icn 7270  ax-addcl 7271  ax-addrcl 7272  ax-mulcl 7273  ax-mulrcl 7274  ax-i2m1 7279  ax-1ne0 7280  ax-rrecex 7283  ax-cnre 7284
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-v 2328  df-un 2641  df-in 2643  df-ss 2647  df-sn 3091  df-pr 3092  df-op 3094  df-uni 3236  df-br 3386  df-opab 3440  df-xp 4037  df-cnv 4039  df-dm 4041  df-rn 4042  df-res 4043  df-ima 4044  df-fv 4051  df-ov 5006  df-2 7969  df-3 7970  df-4 7971  df-5 7972
Copyright terms: Public domain