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

Theorem 5re 9212
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 9198 . 2  |-  5  =  ( 4  +  1 )
2 4re 9210 . . 3  |-  4  e.  RR
3 1re 8267 . . 3  |-  1  e.  RR
42, 3readdcli 8280 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2139 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1526  (class class class)co 5370   RRcr 8167   1c1 8169    + caddc 8171   4c4 9188   5c5 9189
This theorem is referenced by:  6re  9213  6pos  9225  5p2e7  9250  5p3e8  9251  5p4e9  9252  5p5e10  9253  5t2e10  9265  3lt5  9283  2lt5  9284  1lt5  9285  5lt6  9286  4lt6  9287  5lt7  9292  4lt7  9293  5lt8  9299  4lt8  9300  5lt9  9307  4lt9  9308  5lt10  9316  4lt10  9317  ef01bndlem  11667  prmlem1  12233  sralem  14656  srasca  14660  zlmlem  15199  zlmsca  15203  ppiublem1  19016  ppiub  19018  bposlem3  19100  bposlem4  19101  bposlem5  19102  bposlem6  19103  bposlem8  19105  bposlem9  19106  lgsdir2lem1  19137  ex-id  19377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1528  ax-11 1529  ax-17 1533  ax-12o 1567  ax-10 1581  ax-9 1587  ax-4 1594  ax-16 1780  ax-ext 2051  ax-1cn 8225  ax-icn 8226  ax-addcl 8227  ax-addrcl 8228  ax-mulcl 8229  ax-mulrcl 8230  ax-i2m1 8235  ax-1ne0 8236  ax-rrecex 8239  ax-cnre 8240
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 898  df-ex 1451  df-sb 1741  df-clab 2057  df-cleq 2062  df-clel 2065  df-ne 2189  df-ral 2283  df-rex 2284  df-rab 2286  df-v 2482  df-dif 2801  df-un 2803  df-in 2805  df-ss 2809  df-nul 3078  df-if 3187  df-sn 3266  df-pr 3267  df-op 3269  df-uni 3435  df-br 3597  df-opab 3651  df-xp 4280  df-cnv 4282  df-dm 4284  df-rn 4285  df-res 4286  df-ima 4287  df-fv 4294  df-ov 5373  df-2 9195  df-3 9196  df-4 9197  df-5 9198
  Copyright terms: Public domain W3C validator