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

Theorem 5re 10657
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 10640 . 2  |-  5  =  ( 4  +  1 )
2 4re 10655 . . 3  |-  4  e.  RR
3 1re 9627 . . 3  |-  1  e.  RR
42, 3readdcli 9641 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2488 1  |-  5  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1844  (class class class)co 6280   RRcr 9523   1c1 9525    + caddc 9527   4c4 10630   5c5 10631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-i2m1 9592  ax-1ne0 9593  ax-rrecex 9596  ax-cnre 9597
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-iota 5535  df-fv 5579  df-ov 6283  df-2 10637  df-3 10638  df-4 10639  df-5 10640
This theorem is referenced by:  5cn  10658  6re  10659  6pos  10677  3lt5  10752  2lt5  10753  1lt5  10754  5lt6  10755  4lt6  10756  5lt7  10761  4lt7  10762  5lt8  10768  4lt8  10769  5lt9  10776  4lt9  10777  5lt10  10785  4lt10  10786  5recm6rec  11128  ef01bndlem  14130  prmlem1  14804  sralem  18145  srasca  18149  zlmlem  18856  zlmsca  18860  ppiublem1  23860  ppiub  23862  bposlem3  23944  bposlem4  23945  bposlem5  23946  bposlem6  23947  bposlem8  23949  bposlem9  23950  lgsdir2lem1  23981  cchhllem  24619  ex-id  25585  resvvsca  28290  zlmds  28410  zlmtset  28411  problem2  29885  stoweidlem13  37176  gbegt5  37828  gbogt5  37829  nnsum3primesle9  37855  nnsum4primesodd  37857  evengpop3  37859
  Copyright terms: Public domain W3C validator