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

Theorem 5re 10690
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 10673 . 2  |-  5  =  ( 4  +  1 )
2 4re 10688 . . 3  |-  4  e.  RR
3 1re 9644 . . 3  |-  1  e.  RR
42, 3readdcli 9658 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2507 1  |-  5  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869  (class class class)co 6303   RRcr 9540   1c1 9542    + caddc 9544   4c4 10663   5c5 10664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-i2m1 9609  ax-1ne0 9610  ax-rrecex 9613  ax-cnre 9614
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607  df-ov 6306  df-2 10670  df-3 10671  df-4 10672  df-5 10673
This theorem is referenced by:  5cn  10691  6re  10692  6pos  10710  3lt5  10785  2lt5  10786  1lt5  10787  5lt6  10788  4lt6  10789  5lt7  10794  4lt7  10795  5lt8  10801  4lt8  10802  5lt9  10809  4lt9  10810  5lt10  10818  4lt10  10819  5recm6rec  11160  ef01bndlem  14231  prmlem1  15072  sralem  18393  srasca  18397  zlmlem  19080  zlmsca  19084  ppiublem1  24122  ppiub  24124  bposlem3  24206  bposlem4  24207  bposlem5  24208  bposlem6  24209  bposlem8  24211  bposlem9  24212  lgsdir2lem1  24243  cchhllem  24909  ex-id  25876  resvvsca  28599  zlmds  28770  zlmtset  28771  problem2  30300  stoweidlem13  37699  gbegt5  38580  gbogt5  38581  nnsum3primesle9  38607  nnsum4primesodd  38609  evengpop3  38611
  Copyright terms: Public domain W3C validator