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

Theorem 7re 10694
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 10675 . 2  |-  7  =  ( 6  +  1 )
2 6re 10692 . . 3  |-  6  e.  RR
3 1re 9644 . . 3  |-  1  e.  RR
42, 3readdcli 9658 . 2  |-  ( 6  +  1 )  e.  RR
51, 4eqeltri 2507 1  |-  7  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869  (class class class)co 6303   RRcr 9540   1c1 9542    + caddc 9544   6c6 10665   7c7 10666
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  df-6 10674  df-7 10675
This theorem is referenced by:  7cn  10695  8re  10696  8pos  10712  5lt7  10794  4lt7  10795  3lt7  10796  2lt7  10797  1lt7  10798  7lt8  10799  6lt8  10800  7lt9  10807  6lt9  10808  7lt10  10816  6lt10  10817  bposlem8  24211  lgsdir2lem1  24243  problem4  30302  stgoldbwt  38633  bgoldbwt  38634  nnsum3primesle9  38645  nnsum4primesoddALTV  38648  evengpoap3  38650  bgoldbtbndlem1  38656  bgoldbtbnd  38660
  Copyright terms: Public domain W3C validator