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

Theorem 10re 10664
Description: The number 10 is real. (Contributed by NM, 5-Feb-2007.)
Assertion
Ref Expression
10re  |-  10  e.  RR

Proof of Theorem 10re
StepHypRef Expression
1 df-10 10642 . 2  |-  10  =  ( 9  +  1 )
2 9re 10662 . . 3  |-  9  e.  RR
3 1re 9624 . . 3  |-  1  e.  RR
42, 3readdcli 9638 . 2  |-  ( 9  +  1 )  e.  RR
51, 4eqeltri 2486 1  |-  10  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842  (class class class)co 6277   RRcr 9520   1c1 9522    + caddc 9524   9c9 10632   10c10 10633
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 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-i2m1 9589  ax-1ne0 9590  ax-rrecex 9593  ax-cnre 9594
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 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5532  df-fv 5576  df-ov 6280  df-2 10634  df-3 10635  df-4 10636  df-5 10637  df-6 10638  df-7 10639  df-8 10640  df-9 10641  df-10 10642
This theorem is referenced by:  8lt10  10779  7lt10  10780  6lt10  10781  5lt10  10782  4lt10  10783  3lt10  10784  2lt10  10785  1lt10  10786  0.999...  13840  bpoly4  14002  thlle  19024  bposlem4  23941  bposlem5  23942  problem2  29859  evengpoap3  37828  bgoldbtbndlem1  37834  dp2cl  38790  dpfrac1  38793
  Copyright terms: Public domain W3C validator