![]() |
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 12222 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8re 12248 | . . 3 ⊢ 8 ∈ ℝ | |
3 | 1re 11154 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 11169 | . 2 ⊢ (8 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 9 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7356 ℝcr 11049 1c1 11051 + caddc 11053 8c8 12213 9c9 12214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-1cn 11108 ax-icn 11109 ax-addcl 11110 ax-addrcl 11111 ax-mulcl 11112 ax-mulrcl 11113 ax-i2m1 11118 ax-1ne0 11119 ax-rrecex 11122 ax-cnre 11123 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-iota 6448 df-fv 6504 df-ov 7359 df-2 12215 df-3 12216 df-4 12217 df-5 12218 df-6 12219 df-7 12220 df-8 12221 df-9 12222 |
This theorem is referenced by: 7lt9 12352 6lt9 12353 5lt9 12354 4lt9 12355 3lt9 12356 2lt9 12357 1lt9 12358 10re 12636 9lt10 12748 8lt10 12749 0.999... 15765 cos2bnd 16069 sincos2sgn 16075 slotsdifplendx 17255 dsndxntsetndx 17273 unifndxntsetndx 17280 cnfldfunALTOLD 20808 tuslemOLD 23617 setsmsdsOLD 23829 tnglemOLD 23995 tngdsOLD 24010 2logb9irr 26143 sqrt2cxp2logb9e3 26147 log2tlbnd 26293 bposlem4 26633 bposlem5 26634 bposlem7 26636 bposlem8 26637 bposlem9 26638 ex-fv 29334 dp2lt10 31684 hgt750lem 33204 hgt750lem2 33205 hgt750leme 33211 problem5 34197 60gcd7e1 40452 lcmineqlem23 40498 3lexlogpow5ineq1 40501 3lexlogpow5ineq2 40502 3lexlogpow5ineq4 40503 3lexlogpow5ineq3 40504 3lexlogpow2ineq2 40506 3lexlogpow5ineq5 40507 aks4d1lem1 40509 aks4d1p1 40523 aks4d1p6 40528 aks4d1p7d1 40529 aks4d1p7 40530 aks4d1p8 40534 31prm 45760 2exp340mod341 45896 341fppr2 45897 9fppr8 45900 nfermltl8rev 45905 nfermltl2rev 45906 wtgoldbnnsum4prm 45965 bgoldbnnsum3prm 45967 bgoldbtbndlem1 45968 ackval42 46753 |
Copyright terms: Public domain | W3C validator |