![]() |
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 12333 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 12357 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 11259 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 11274 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2835 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7431 ℝcr 11152 1c1 11154 + caddc 11156 7c7 12324 8c8 12325 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-i2m1 11221 ax-1ne0 11222 ax-rrecex 11225 ax-cnre 11226 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-iota 6516 df-fv 6571 df-ov 7434 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 |
This theorem is referenced by: 9re 12363 9pos 12377 6lt8 12457 5lt8 12458 4lt8 12459 3lt8 12460 2lt8 12461 1lt8 12462 8lt9 12463 7lt9 12464 8th4div3 12484 8lt10 12863 7lt10 12864 ef01bndlem 16217 cos2bnd 16221 slotstnscsi 17406 slotsdnscsi 17438 sralemOLD 21194 chtub 27271 bposlem8 27350 bposlem9 27351 lgsdir2lem1 27384 lgsdir2lem4 27387 lgsdir2lem5 27388 2lgsoddprmlem1 27467 2lgsoddprmlem2 27468 chebbnd1lem2 27529 chebbnd1lem3 27530 chebbnd1 27531 pntlemf 27664 cchhllemOLD 28917 hgt750lem 34645 hgt750lem2 34646 hgt750leme 34652 lcmineqlem23 42033 lcmineqlem 42034 3lexlogpow5ineq2 42037 aks4d1p1 42058 8rp 42316 resqrtvalex 43635 imsqrtvalex 43636 fmtnoprmfac2lem1 47491 mod42tp1mod8 47527 nnsum3primesle9 47719 nnsum4primesoddALTV 47722 nnsum4primesevenALTV 47726 bgoldbtbndlem1 47730 tgoldbach 47742 |
Copyright terms: Public domain | W3C validator |