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 11893 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4re 11911 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 1re 10830 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10845 | . 2 ⊢ (4 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 5 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 (class class class)co 7210 ℝcr 10725 1c1 10727 + caddc 10729 4c4 11884 5c5 11885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-1cn 10784 ax-icn 10785 ax-addcl 10786 ax-addrcl 10787 ax-mulcl 10788 ax-mulrcl 10789 ax-i2m1 10794 ax-1ne0 10795 ax-rrecex 10798 ax-cnre 10799 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2940 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-iota 6335 df-fv 6385 df-ov 7213 df-2 11890 df-3 11891 df-4 11892 df-5 11893 |
This theorem is referenced by: 6re 11917 6pos 11937 3lt5 12005 2lt5 12006 1lt5 12007 5lt6 12008 4lt6 12009 5lt7 12014 4lt7 12015 5lt8 12021 4lt8 12022 5lt9 12029 4lt9 12030 5lt10 12425 4lt10 12426 5recm6rec 12434 ef01bndlem 15742 prm23ge5 16365 prmlem1 16658 rmodislmod 19964 sralem 20211 srasca 20215 zlmlem 20480 zlmsca 20484 ppiublem1 26080 ppiub 26082 bposlem3 26164 bposlem4 26165 bposlem5 26166 bposlem6 26167 bposlem8 26169 bposlem9 26170 lgsdir2lem1 26203 gausslemma2dlem4 26247 2lgslem3 26282 cchhllem 26975 ex-id 28514 ex-sqrt 28534 threehalves 30906 cyc3conja 31140 resvvsca 31249 zlmds 31623 zlmtset 31624 hgt750lem2 32341 hgt750leme 32347 problem2 33334 12gcd5e1 39743 lcmineqlem23 39791 3lexlogpow2ineq1 39798 3lexlogpow2ineq2 39799 aks4d1p1p4 39810 aks4d1p1p6 39812 aks4d1p1p7 39813 aks4d1p1p5 39814 stoweidlem13 43227 31prm 44720 gbegt5 44884 gbowgt5 44885 sbgoldbo 44910 nnsum3primesle9 44917 nnsum4primesodd 44919 evengpop3 44921 |
Copyright terms: Public domain | W3C validator |