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

Theorem 5re 9246
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 9232 . 2  |-  5  =  ( 4  +  1 )
2 4re 9244 . . 3  |-  4  e.  RR
3 1re 8301 . . 3  |-  1  e.  RR
42, 3readdcli 8314 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2170 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1533  (class class class)co 5404   RRcr 8201   1c1 8203    + caddc 8205   4c4 9222   5c5 9223
This theorem is referenced by:  6re  9247  6pos  9259  5p2e7  9284  5p3e8  9285  5p4e9  9286  5p5e10  9287  5t2e10  9299  3lt5  9317  2lt5  9318  1lt5  9319  5lt6  9320  4lt6  9321  5lt7  9326  4lt7  9327  5lt8  9333  4lt8  9334  5lt9  9341  4lt9  9342  5lt10  9350  4lt10  9351  ef01bndlem  11701  prmlem1  12267  sralem  14690  srasca  14694  zlmlem  15233  zlmsca  15237  ppiublem1  19050  ppiub  19052  bposlem3  19134  bposlem4  19135  bposlem5  19136  bposlem6  19137  bposlem8  19139  bposlem9  19140  lgsdir2lem1  19171  ex-id  19411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-1cn 8259  ax-icn 8260  ax-addcl 8261  ax-addrcl 8262  ax-mulcl 8263  ax-mulrcl 8264  ax-i2m1 8269  ax-1ne0 8270  ax-rrecex 8273  ax-cnre 8274
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 902  df-ex 1457  df-sb 1748  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-ral 2315  df-rex 2316  df-rab 2318  df-v 2514  df-dif 2833  df-un 2835  df-in 2837  df-ss 2841  df-nul 3111  df-if 3221  df-sn 3300  df-pr 3301  df-op 3303  df-uni 3469  df-br 3631  df-opab 3685  df-xp 4314  df-cnv 4316  df-dm 4318  df-rn 4319  df-res 4320  df-ima 4321  df-fv 4328  df-ov 5407  df-2 9229  df-3 9230  df-4 9231  df-5 9232
  Copyright terms: Public domain W3C validator