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

Theorem 5re 9789
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 9775 . 2  |-  5  =  ( 4  +  1 )
2 4re 9787 . . 3  |-  4  e.  RR
3 1re 8805 . . 3  |-  1  e.  RR
42, 3readdcli 8818 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2328 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1621  (class class class)co 5792   RRcr 8704   1c1 8706    + caddc 8708   4c4 9765   5c5 9766
This theorem is referenced by:  6re  9790  6pos  9802  5p2e7  9827  5p3e8  9828  5p4e9  9829  5p5e10  9830  5t2e10  9842  3lt5  9860  2lt5  9861  1lt5  9862  5lt6  9863  4lt6  9864  5lt7  9869  4lt7  9870  5lt8  9876  4lt8  9877  5lt9  9884  4lt9  9885  5lt10  9893  4lt10  9894  ef01bndlem  12426  prmlem1  13071  sralem  15892  srasca  15896  zlmlem  16433  zlmsca  16437  ppiublem1  20403  ppiub  20405  bposlem3  20487  bposlem4  20488  bposlem5  20489  bposlem6  20490  bposlem8  20492  bposlem9  20493  lgsdir2lem1  20524  ex-id  20764  5recm6rec  23472  bpoly4  24169  stoweidlem13  27097
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-addrcl 8766  ax-mulcl 8767  ax-mulrcl 8768  ax-i2m1 8773  ax-1ne0 8774  ax-rrecex 8777  ax-cnre 8778
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fv 4689  df-ov 5795  df-2 9772  df-3 9773  df-4 9774  df-5 9775
  Copyright terms: Public domain W3C validator