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

Theorem 9re 9870
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 9856 . 2  |-  9  =  ( 8  +  1 )
2 8re 9869 . . 3  |-  8  e.  RR
3 1re 8882 . . 3  |-  1  e.  RR
42, 3readdcli 8895 . 2  |-  ( 8  +  1 )  e.  RR
51, 4eqeltri 2386 1  |-  9  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1701  (class class class)co 5900   RRcr 8781   1c1 8783    + caddc 8785   8c8 9846   9c9 9847
This theorem is referenced by:  10re  9871  10pos  9883  7lt9  9962  6lt9  9963  5lt9  9964  4lt9  9965  3lt9  9966  2lt9  9967  1lt9  9968  9lt10  9969  8lt10  9970  0.999...  12384  cos2bnd  12515  sincos2sgn  12521  setsmsds  18074  tnglem  18208  tngds  18216  log2tlbnd  20294  bposlem4  20579  bposlem5  20580  bposlem7  20582  bposlem8  20583  bposlem9  20584  ex-fv  20883  tuslem  23463
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-i2m1 8850  ax-1ne0 8851  ax-rrecex 8854  ax-cnre 8855
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-2 9849  df-3 9850  df-4 9851  df-5 9852  df-6 9853  df-7 9854  df-8 9855  df-9 9856
  Copyright terms: Public domain W3C validator