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

Theorem 7re 10659
Description: The number 7 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
7re  |-  7  e.  RR

Proof of Theorem 7re
StepHypRef Expression
1 df-7 10640 . 2  |-  7  =  ( 6  +  1 )
2 6re 10657 . . 3  |-  6  e.  RR
3 1re 9625 . . 3  |-  1  e.  RR
42, 3readdcli 9639 . 2  |-  ( 6  +  1 )  e.  RR
51, 4eqeltri 2486 1  |-  7  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842  (class class class)co 6278   RRcr 9521   1c1 9523    + caddc 9525   6c6 10630   7c7 10631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-i2m1 9590  ax-1ne0 9591  ax-rrecex 9594  ax-cnre 9595
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-2 10635  df-3 10636  df-4 10637  df-5 10638  df-6 10639  df-7 10640
This theorem is referenced by:  7cn  10660  8re  10661  8pos  10677  5lt7  10759  4lt7  10760  3lt7  10761  2lt7  10762  1lt7  10763  7lt8  10764  6lt8  10765  7lt9  10772  6lt9  10773  7lt10  10781  6lt10  10782  bposlem8  23947  lgsdir2lem1  23979  problem4  29874  stgoldbwt  37830  bgoldbwt  37831  nnsum3primesle9  37842  nnsum4primesoddALTV  37845  evengpoap3  37847  bgoldbtbndlem1  37853  bgoldbtbnd  37857
  Copyright terms: Public domain W3C validator