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

Theorem 5re 11379
Description: The number 5 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
5re 5 ∈ ℝ

Proof of Theorem 5re
StepHypRef Expression
1 df-5 11363 . 2 5 = (4 + 1)
2 4re 11377 . . 3 4 ∈ ℝ
3 1re 10321 . . 3 1 ∈ ℝ
42, 3readdcli 10336 . 2 (4 + 1) ∈ ℝ
51, 4eqeltri 2881 1 5 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  (class class class)co 6870  cr 10216  1c1 10218   + caddc 10220  4c4 11354  5c5 11355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-i2m1 10285  ax-1ne0 10286  ax-rrecex 10289  ax-cnre 10290
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105  df-ov 6873  df-2 11360  df-3 11361  df-4 11362  df-5 11363
This theorem is referenced by:  5cn  11380  6re  11381  6pos  11398  3lt5  11473  2lt5  11474  1lt5  11475  5lt6  11476  4lt6  11477  5lt7  11482  4lt7  11483  5lt8  11489  4lt8  11490  5lt9  11497  4lt9  11498  5lt10  11890  4lt10  11891  5recm6rec  11899  ef01bndlem  15130  prm23ge5  15733  prmlem1  16022  rmodislmod  19131  sralem  19382  srasca  19386  zlmlem  20069  zlmsca  20073  ppiublem1  25140  ppiub  25142  bposlem3  25224  bposlem4  25225  bposlem5  25226  bposlem6  25227  bposlem8  25229  bposlem9  25230  lgsdir2lem1  25263  gausslemma2dlem4  25307  2lgslem3  25342  cchhllem  25980  ex-id  27621  ex-sqrt  27641  threehalves  29947  resvvsca  30158  zlmds  30332  zlmtset  30333  hgt750lem2  31054  hgt750leme  31060  problem2  31880  stoweidlem13  40706  31prm  42084  gbegt5  42221  gbowgt5  42222  sbgoldbo  42247  nnsum3primesle9  42254  nnsum4primesodd  42256  evengpop3  42258
  Copyright terms: Public domain W3C validator