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 11695 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4re 11713 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 1re 10633 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10648 | . 2 ⊢ (4 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2907 | 1 ⊢ 5 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2108 (class class class)co 7148 ℝcr 10528 1c1 10530 + caddc 10532 4c4 11686 5c5 11687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-1cn 10587 ax-icn 10588 ax-addcl 10589 ax-addrcl 10590 ax-mulcl 10591 ax-mulrcl 10592 ax-i2m1 10597 ax-1ne0 10598 ax-rrecex 10601 ax-cnre 10602 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7151 df-2 11692 df-3 11693 df-4 11694 df-5 11695 |
This theorem is referenced by: 6re 11719 6pos 11739 3lt5 11807 2lt5 11808 1lt5 11809 5lt6 11810 4lt6 11811 5lt7 11816 4lt7 11817 5lt8 11823 4lt8 11824 5lt9 11831 4lt9 11832 5lt10 12225 4lt10 12226 5recm6rec 12234 ef01bndlem 15529 prm23ge5 16144 prmlem1 16433 rmodislmod 19694 sralem 19941 srasca 19945 zlmlem 20656 zlmsca 20660 ppiublem1 25770 ppiub 25772 bposlem3 25854 bposlem4 25855 bposlem5 25856 bposlem6 25857 bposlem8 25859 bposlem9 25860 lgsdir2lem1 25893 gausslemma2dlem4 25937 2lgslem3 25972 cchhllem 26665 ex-id 28205 ex-sqrt 28225 threehalves 30584 cyc3conja 30792 resvvsca 30900 zlmds 31198 zlmtset 31199 hgt750lem2 31916 hgt750leme 31922 problem2 32902 stoweidlem13 42289 31prm 43751 gbegt5 43917 gbowgt5 43918 sbgoldbo 43943 nnsum3primesle9 43950 nnsum4primesodd 43952 evengpop3 43954 |
Copyright terms: Public domain | W3C validator |