![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 7re | Structured version Visualization version GIF version |
Description: The number 7 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
7re | ⊢ 7 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-7 11558 | . 2 ⊢ 7 = (6 + 1) | |
2 | 6re 11580 | . . 3 ⊢ 6 ∈ ℝ | |
3 | 1re 10492 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10507 | . 2 ⊢ (6 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2879 | 1 ⊢ 7 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 (class class class)co 7021 ℝcr 10387 1c1 10389 + caddc 10391 6c6 11549 7c7 11550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-i2m1 10456 ax-1ne0 10457 ax-rrecex 10460 ax-cnre 10461 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-iota 6194 df-fv 6238 df-ov 7024 df-2 11553 df-3 11554 df-4 11555 df-5 11556 df-6 11557 df-7 11558 |
This theorem is referenced by: 8re 11586 8pos 11602 5lt7 11677 4lt7 11678 3lt7 11679 2lt7 11680 1lt7 11681 7lt8 11682 6lt8 11683 7lt9 11690 6lt9 11691 7lt10 12086 6lt10 12087 bposlem8 25554 lgsdir2lem1 25588 hgt750lem2 31545 hgt750leme 31551 problem4 32525 mod42tp1mod8 43275 stgoldbwt 43449 sbgoldbwt 43450 nnsum3primesle9 43467 nnsum4primesoddALTV 43470 evengpoap3 43472 bgoldbtbndlem1 43478 bgoldbtbnd 43482 |
Copyright terms: Public domain | W3C validator |