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

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

Proof of Theorem 9re
StepHypRef Expression
1 df-9 10096 . 2  |-  9  =  ( 8  +  1 )
2 8re 10109 . . 3  |-  8  e.  RR
3 1re 9121 . . 3  |-  1  e.  RR
42, 3readdcli 9134 . 2  |-  ( 8  +  1 )  e.  RR
51, 4eqeltri 2512 1  |-  9  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1727  (class class class)co 6110   RRcr 9020   1c1 9022    + caddc 9024   8c8 10086   9c9 10087
This theorem is referenced by:  10re  10111  10pos  10123  7lt9  10202  6lt9  10203  5lt9  10204  4lt9  10205  3lt9  10206  2lt9  10207  1lt9  10208  9lt10  10209  8lt10  10210  0.999...  12689  cos2bnd  12820  sincos2sgn  12826  tuslem  18328  setsmsds  18537  tnglem  18712  tngds  18720  log2tlbnd  20816  bposlem4  21102  bposlem5  21103  bposlem7  21105  bposlem8  21106  bposlem9  21107  ex-fv  21782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-i2m1 9089  ax-1ne0 9090  ax-rrecex 9093  ax-cnre 9094
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-iota 5447  df-fv 5491  df-ov 6113  df-2 10089  df-3 10090  df-4 10091  df-5 10092  df-6 10093  df-7 10094  df-8 10095  df-9 10096
  Copyright terms: Public domain W3C validator