![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 8re | Structured version Visualization version GIF version |
Description: The number 8 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
8re | ⊢ 8 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 11512 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 11540 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 10441 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10457 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2862 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2050 (class class class)co 6978 ℝcr 10336 1c1 10338 + caddc 10340 7c7 11503 8c8 11504 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-i2m1 10405 ax-1ne0 10406 ax-rrecex 10409 ax-cnre 10410 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-iota 6154 df-fv 6198 df-ov 6981 df-2 11506 df-3 11507 df-4 11508 df-5 11509 df-6 11510 df-7 11511 df-8 11512 |
This theorem is referenced by: 8cnOLD 11546 9re 11548 9pos 11563 6lt8 11643 5lt8 11644 4lt8 11645 3lt8 11646 2lt8 11647 1lt8 11648 8lt9 11649 7lt9 11650 8th4div3 11670 8lt10 12048 7lt10 12049 ef01bndlem 15400 cos2bnd 15404 sralem 19674 chtub 25493 bposlem8 25572 bposlem9 25573 lgsdir2lem1 25606 lgsdir2lem4 25609 lgsdir2lem5 25610 2lgsoddprmlem1 25689 2lgsoddprmlem2 25690 chebbnd1lem2 25751 chebbnd1lem3 25752 chebbnd1 25753 pntlemf 25886 cchhllem 26379 hgt750lem 31570 hgt750lem2 31571 hgt750leme 31577 fmtnoprmfac2lem1 43097 mod42tp1mod8 43136 nnsum3primesle9 43328 nnsum4primesoddALTV 43331 nnsum4primesevenALTV 43335 bgoldbtbndlem1 43339 tgoldbach 43351 |
Copyright terms: Public domain | W3C validator |