| 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 12336 | . 2 ⊢ 9 = (8 + 1) | |
| 2 | 8re 12362 | . . 3 ⊢ 8 ∈ ℝ | |
| 3 | 1re 11261 | . . 3 ⊢ 1 ∈ ℝ | |
| 4 | 2, 3 | readdcli 11276 | . 2 ⊢ (8 + 1) ∈ ℝ |
| 5 | 1, 4 | eqeltri 2837 | 1 ⊢ 9 ∈ ℝ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 (class class class)co 7431 ℝcr 11154 1c1 11156 + caddc 11158 8c8 12327 9c9 12328 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-i2m1 11223 ax-1ne0 11224 ax-rrecex 11227 ax-cnre 11228 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 |
| This theorem is referenced by: 7lt9 12466 6lt9 12467 5lt9 12468 4lt9 12469 3lt9 12470 2lt9 12471 1lt9 12472 10re 12752 9lt10 12864 8lt10 12865 0.999... 15917 cos2bnd 16224 sincos2sgn 16230 slotsdifplendx 17419 dsndxntsetndx 17437 unifndxntsetndx 17444 cnfldfunALTOLDOLD 21393 tuslemOLD 24276 setsmsdsOLD 24488 tnglemOLD 24654 tngdsOLD 24669 2logb9irr 26838 sqrt2cxp2logb9e3 26842 log2tlbnd 26988 bposlem4 27331 bposlem5 27332 bposlem7 27334 bposlem8 27335 bposlem9 27336 ex-fv 30462 dp2lt10 32866 hgt750lem 34666 hgt750lem2 34667 hgt750leme 34673 problem5 35674 60gcd7e1 42006 lcmineqlem23 42052 3lexlogpow5ineq1 42055 3lexlogpow5ineq2 42056 3lexlogpow5ineq4 42057 3lexlogpow5ineq3 42058 3lexlogpow2ineq2 42060 3lexlogpow5ineq5 42061 aks4d1lem1 42063 aks4d1p1 42077 aks4d1p6 42082 aks4d1p7d1 42083 aks4d1p7 42084 aks4d1p8 42088 9rp 42338 31prm 47584 2exp340mod341 47720 341fppr2 47721 9fppr8 47724 nfermltl8rev 47729 nfermltl2rev 47730 wtgoldbnnsum4prm 47789 bgoldbnnsum3prm 47791 bgoldbtbndlem1 47792 ackval42 48617 |
| Copyright terms: Public domain | W3C validator |