Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  9re GIF version

Theorem 9re 8814
 Description: The number 9 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
9re 9 ∈ ℝ

Proof of Theorem 9re
StepHypRef Expression
1 df-9 8793 . 2 9 = (8 + 1)
2 8re 8812 . . 3 8 ∈ ℝ
3 1re 7772 . . 3 1 ∈ ℝ
42, 3readdcli 7786 . 2 (8 + 1) ∈ ℝ
51, 4eqeltri 2212 1 9 ∈ ℝ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1480  (class class class)co 5774  ℝcr 7626  1c1 7628   + caddc 7630  8c8 8784  9c9 8785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1re 7721  ax-addrcl 7724 This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8786  df-3 8787  df-4 8788  df-5 8789  df-6 8790  df-7 8791  df-8 8792  df-9 8793 This theorem is referenced by:  9cn  8815  7lt9  8925  6lt9  8926  5lt9  8927  4lt9  8928  3lt9  8929  2lt9  8930  1lt9  8931  9lt10  9319  8lt10  9320  0.999...  11297  cos2bnd  11474  sincos2sgn  11479  setsmsdsg  12659
 Copyright terms: Public domain W3C validator