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

Theorem 5re 12248
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 12227 . 2 5 = (4 + 1)
2 4re 12245 . . 3 4 ∈ ℝ
3 1re 11163 . . 3 1 ∈ ℝ
42, 3readdcli 11178 . 2 (4 + 1) ∈ ℝ
51, 4eqeltri 2830 1 5 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7361  cr 11058  1c1 11060   + caddc 11062  4c4 12218  5c5 12219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-i2m1 11127  ax-1ne0 11128  ax-rrecex 11131  ax-cnre 11132
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-ov 7364  df-2 12224  df-3 12225  df-4 12226  df-5 12227
This theorem is referenced by:  6re  12251  6pos  12271  3lt5  12339  2lt5  12340  1lt5  12341  5lt6  12342  4lt6  12343  5lt7  12348  4lt7  12349  5lt8  12355  4lt8  12356  5lt9  12363  4lt9  12364  5lt10  12761  4lt10  12762  5recm6rec  12770  ef01bndlem  16074  prm23ge5  16695  prmlem1  16988  vscandxnscandx  17213  slotsdifipndx  17224  slotstnscsi  17249  plendxnscandx  17262  slotsdnscsi  17281  rmodislmodOLD  20435  sralemOLD  20684  srascaOLD  20692  zlmlemOLD  20941  ppiublem1  26573  ppiub  26575  bposlem3  26657  bposlem4  26658  bposlem5  26659  bposlem6  26660  bposlem8  26662  bposlem9  26663  lgsdir2lem1  26696  gausslemma2dlem4  26740  2lgslem3  26775  cchhllemOLD  27885  ex-id  29427  ex-sqrt  29447  threehalves  31827  cyc3conja  32062  resvvscaOLD  32183  zlmdsOLD  32608  zlmtsetOLD  32610  hgt750lem2  33329  hgt750leme  33335  problem2  34318  12gcd5e1  40510  lcmineqlem23  40558  3lexlogpow2ineq1  40565  3lexlogpow2ineq2  40566  aks4d1p1p4  40578  aks4d1p1p6  40580  aks4d1p1p7  40581  aks4d1p1p5  40582  stoweidlem13  44344  31prm  45879  gbegt5  46043  gbowgt5  46044  sbgoldbo  46069  nnsum3primesle9  46076  nnsum4primesodd  46078  evengpop3  46080
  Copyright terms: Public domain W3C validator