![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 5re | Structured version Visualization version GIF version |
Description: The number 5 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
5re | ⊢ 5 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-5 11120 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4re 11135 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 1re 10077 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10091 | . 2 ⊢ (4 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2726 | 1 ⊢ 5 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 (class class class)co 6690 ℝcr 9973 1c1 9975 + caddc 9977 4c4 11110 5c5 11111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-i2m1 10042 ax-1ne0 10043 ax-rrecex 10046 ax-cnre 10047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-2 11117 df-3 11118 df-4 11119 df-5 11120 |
This theorem is referenced by: 5cn 11138 6re 11139 6pos 11157 3lt5 11239 2lt5 11240 1lt5 11241 5lt6 11242 4lt6 11243 5lt7 11248 4lt7 11249 5lt8 11255 4lt8 11256 5lt9 11263 4lt9 11264 5lt10OLD 11272 4lt10OLD 11273 5lt10 11715 4lt10 11716 5recm6rec 11724 ef01bndlem 14958 prm23ge5 15567 prmlem1 15861 rmodislmod 18979 sralem 19225 srasca 19229 zlmlem 19913 zlmsca 19917 ppiublem1 24972 ppiub 24974 bposlem3 25056 bposlem4 25057 bposlem5 25058 bposlem6 25059 bposlem8 25061 bposlem9 25062 lgsdir2lem1 25095 gausslemma2dlem4 25139 2lgslem3 25174 cchhllem 25812 ex-id 27421 ex-sqrt 27441 threehalves 29751 resvvsca 29962 zlmds 30136 zlmtset 30137 hgt750lem2 30858 hgt750leme 30864 problem2 31685 problem2OLD 31686 stoweidlem13 40548 31prm 41837 gbegt5 41974 gbowgt5 41975 sbgoldbo 42000 nnsum3primesle9 42007 nnsum4primesodd 42009 evengpop3 42011 |
Copyright terms: Public domain | W3C validator |