Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 9re | Structured version Visualization version 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 11701 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8re 11727 | . . 3 ⊢ 8 ∈ ℝ | |
3 | 1re 10635 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10650 | . 2 ⊢ (8 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2909 | 1 ⊢ 9 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 (class class class)co 7150 ℝcr 10530 1c1 10532 + caddc 10534 8c8 11692 9c9 11693 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-i2m1 10599 ax-1ne0 10600 ax-rrecex 10603 ax-cnre 10604 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-iota 6308 df-fv 6357 df-ov 7153 df-2 11694 df-3 11695 df-4 11696 df-5 11697 df-6 11698 df-7 11699 df-8 11700 df-9 11701 |
This theorem is referenced by: 7lt9 11831 6lt9 11832 5lt9 11833 4lt9 11834 3lt9 11835 2lt9 11836 1lt9 11837 10re 12111 9lt10 12223 8lt10 12224 0.999... 15231 cos2bnd 15535 sincos2sgn 15541 cnfldfun 20551 tuslem 22870 setsmsds 23080 tnglem 23243 tngds 23251 2logb9irr 25367 sqrt2cxp2logb9e3 25371 log2tlbnd 25517 bposlem4 25857 bposlem5 25858 bposlem7 25860 bposlem8 25861 bposlem9 25862 ex-fv 28216 dp2lt10 30555 hgt750lem 31917 hgt750lem2 31918 hgt750leme 31924 problem5 32907 31prm 43754 2exp340mod341 43892 341fppr2 43893 9fppr8 43896 nfermltl8rev 43901 nfermltl2rev 43902 wtgoldbnnsum4prm 43961 bgoldbnnsum3prm 43963 bgoldbtbndlem1 43964 |
Copyright terms: Public domain | W3C validator |