MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  5re Unicode version

Theorem 5re 9641
Description: The number 5 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
5re  |-  5  e.  RR

Proof of Theorem 5re
StepHypRef Expression
1 df-5 9627 . 2  |-  5  =  ( 4  +  1 )
2 4re 9639 . . 3  |-  4  e.  RR
3 1re 8691 . . 3  |-  1  e.  RR
42, 3readdcli 8704 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2311 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1610  (class class class)co 5685   RRcr 8590   1c1 8592    + caddc 8594   4c4 9617   5c5 9618
This theorem is referenced by:  6re  9642  6pos  9654  5p2e7  9679  5p3e8  9680  5p4e9  9681  5p5e10  9682  5t2e10  9694  3lt5  9712  2lt5  9713  1lt5  9714  5lt6  9715  4lt6  9716  5lt7  9721  4lt7  9722  5lt8  9728  4lt8  9729  5lt9  9736  4lt9  9737  5lt10  9745  4lt10  9746  ef01bndlem  12272  prmlem1  12917  sralem  15608  srasca  15612  zlmlem  16149  zlmsca  16153  ppiublem1  20091  ppiub  20093  bposlem3  20175  bposlem4  20176  bposlem5  20177  bposlem6  20178  bposlem8  20180  bposlem9  20181  lgsdir2lem1  20212  ex-id  20452  5recm6rec  23077  bpoly4  23774
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-1cn 8649  ax-icn 8650  ax-addcl 8651  ax-addrcl 8652  ax-mulcl 8653  ax-mulrcl 8654  ax-i2m1 8659  ax-1ne0 8660  ax-rrecex 8663  ax-cnre 8664
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-3an 935  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-ne 2402  df-ral 2499  df-rex 2500  df-rab 2502  df-v 2714  df-dif 3061  df-un 3063  df-in 3065  df-ss 3069  df-nul 3343  df-if 3451  df-sn 3530  df-pr 3531  df-op 3533  df-uni 3708  df-br 3901  df-opab 3955  df-xp 4573  df-cnv 4575  df-dm 4577  df-rn 4578  df-res 4579  df-ima 4580  df-fv 4587  df-ov 5688  df-2 9624  df-3 9625  df-4 9626  df-5 9627
  Copyright terms: Public domain W3C validator