![]() |
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 11694 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 11718 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 10630 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10645 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2886 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 (class class class)co 7135 ℝcr 10525 1c1 10527 + caddc 10529 7c7 11685 8c8 11686 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-i2m1 10594 ax-1ne0 10595 ax-rrecex 10598 ax-cnre 10599 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-ral 3111 df-rex 3112 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-ov 7138 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 |
This theorem is referenced by: 9re 11724 9pos 11738 6lt8 11818 5lt8 11819 4lt8 11820 3lt8 11821 2lt8 11822 1lt8 11823 8lt9 11824 7lt9 11825 8th4div3 11845 8lt10 12218 7lt10 12219 ef01bndlem 15529 cos2bnd 15533 sralem 19942 chtub 25796 bposlem8 25875 bposlem9 25876 lgsdir2lem1 25909 lgsdir2lem4 25912 lgsdir2lem5 25913 2lgsoddprmlem1 25992 2lgsoddprmlem2 25993 chebbnd1lem2 26054 chebbnd1lem3 26055 chebbnd1 26056 pntlemf 26189 cchhllem 26681 hgt750lem 32032 hgt750lem2 32033 hgt750leme 32039 lcmineqlem23 39339 lcmineqlem 39340 resqrtvalex 40345 imsqrtvalex 40346 fmtnoprmfac2lem1 44083 mod42tp1mod8 44120 nnsum3primesle9 44312 nnsum4primesoddALTV 44315 nnsum4primesevenALTV 44319 bgoldbtbndlem1 44323 tgoldbach 44335 |
Copyright terms: Public domain | W3C validator |