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

Theorem 5re 11262
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 11245 . 2 5 = (4 + 1)
2 4re 11260 . . 3 4 ∈ ℝ
3 1re 10202 . . 3 1 ∈ ℝ
42, 3readdcli 10216 . 2 (4 + 1) ∈ ℝ
51, 4eqeltri 2823 1 5 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2127  (class class class)co 6801  cr 10098  1c1 10100   + caddc 10102  4c4 11235  5c5 11236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-i2m1 10167  ax-1ne0 10168  ax-rrecex 10171  ax-cnre 10172
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804  df-2 11242  df-3 11243  df-4 11244  df-5 11245
This theorem is referenced by:  5cn  11263  6re  11264  6pos  11282  3lt5  11364  2lt5  11365  1lt5  11366  5lt6  11367  4lt6  11368  5lt7  11373  4lt7  11374  5lt8  11380  4lt8  11381  5lt9  11388  4lt9  11389  5lt10OLD  11397  4lt10OLD  11398  5lt10  11840  4lt10  11841  5recm6rec  11849  ef01bndlem  15084  prm23ge5  15693  prmlem1  15987  rmodislmod  19104  sralem  19350  srasca  19354  zlmlem  20038  zlmsca  20042  ppiublem1  25097  ppiub  25099  bposlem3  25181  bposlem4  25182  bposlem5  25183  bposlem6  25184  bposlem8  25186  bposlem9  25187  lgsdir2lem1  25220  gausslemma2dlem4  25264  2lgslem3  25299  cchhllem  25937  ex-id  27573  ex-sqrt  27593  threehalves  29903  resvvsca  30114  zlmds  30288  zlmtset  30289  hgt750lem2  31010  hgt750leme  31016  problem2  31837  problem2OLD  31838  stoweidlem13  40702  31prm  41991  gbegt5  42128  gbowgt5  42129  sbgoldbo  42154  nnsum3primesle9  42161  nnsum4primesodd  42163  evengpop3  42165
  Copyright terms: Public domain W3C validator