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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 7762 . 2
2 4re 7772 . . 3
3 1re 7112 . . 3
42, 3readdcli 7108 . 2
51, 4eqeltri 1998 1
Colors of variables: wff set class
Syntax hints:   wcel 1427  (class class class)co 4924  cr 7005  c1 7007   caddc 7009  c4 7752  c5 7753
This theorem is referenced by:  6re 7774  6pos 7785  5p2e7 7801  5p3e8 7802  5p4e9 7803  5p5e10 7804  5t2e10 7815  3lt5 7833  2lt5 7834  1lt5 7835  5lt6 7836  4lt6 7837  5lt7 7842  4lt7 7843  5lt8 7849  4lt8 7850  ef01bndlem 9519  5t5e25 9969  prmlem1 9971  lmodlem1 10424  lmodlem2 10425  ppiublem 12899  ppiub 12900  bposlem3 12933  bposlem4 12934  bposlem5 12935  bposlem6 12936  bposlem8 12938  bposlem9 12939  algfn 18249  phllem 20435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-addrcl 7064  ax-mulcl 7065  ax-mulrcl 7066  ax-i2m1 7071  ax-1ne0 7072  ax-rrecex 7075  ax-cnre 7076
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-v 2337  df-un 2639  df-in 2641  df-ss 2643  df-sn 3080  df-pr 3081  df-op 3083  df-uni 3214  df-br 3359  df-opab 3413  df-xp 4005  df-cnv 4007  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fv 4019  df-ov 4926  df-2 7759  df-3 7760  df-4 7761  df-5 7762
Copyright terms: Public domain