![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 9re | GIF version |
Description: The number 9 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
9re | ⊢ 9 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-9 8810 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8re 8829 | . . 3 ⊢ 8 ∈ ℝ | |
3 | 1re 7789 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7803 | . 2 ⊢ (8 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2213 | 1 ⊢ 9 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1481 (class class class)co 5782 ℝcr 7643 1c1 7645 + caddc 7647 8c8 8801 9c9 8802 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 ax-1re 7738 ax-addrcl 7741 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 df-2 8803 df-3 8804 df-4 8805 df-5 8806 df-6 8807 df-7 8808 df-8 8809 df-9 8810 |
This theorem is referenced by: 9cn 8832 7lt9 8942 6lt9 8943 5lt9 8944 4lt9 8945 3lt9 8946 2lt9 8947 1lt9 8948 9lt10 9336 8lt10 9337 0.999... 11322 cos2bnd 11503 sincos2sgn 11508 setsmsdsg 12688 2logb9irr 13096 2logb9irrap 13102 |
Copyright terms: Public domain | W3C validator |