![]() |
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 11551 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4re 11569 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 1re 10487 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10502 | . 2 ⊢ (4 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2879 | 1 ⊢ 5 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 (class class class)co 7016 ℝcr 10382 1c1 10384 + caddc 10386 4c4 11542 5c5 11543 |
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 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-i2m1 10451 ax-1ne0 10452 ax-rrecex 10455 ax-cnre 10456 |
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 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-iota 6189 df-fv 6233 df-ov 7019 df-2 11548 df-3 11549 df-4 11550 df-5 11551 |
This theorem is referenced by: 6re 11575 6pos 11595 3lt5 11663 2lt5 11664 1lt5 11665 5lt6 11666 4lt6 11667 5lt7 11672 4lt7 11673 5lt8 11679 4lt8 11680 5lt9 11687 4lt9 11688 5lt10 12083 4lt10 12084 5recm6rec 12092 ef01bndlem 15370 prm23ge5 15981 prmlem1 16270 rmodislmod 19392 sralem 19639 srasca 19643 zlmlem 20346 zlmsca 20350 ppiublem1 25460 ppiub 25462 bposlem3 25544 bposlem4 25545 bposlem5 25546 bposlem6 25547 bposlem8 25549 bposlem9 25550 lgsdir2lem1 25583 gausslemma2dlem4 25627 2lgslem3 25662 cchhllem 26356 ex-id 27905 ex-sqrt 27925 threehalves 30275 cyc3conja 30437 resvvsca 30561 zlmds 30822 zlmtset 30823 hgt750lem2 31540 hgt750leme 31546 problem2 32517 stoweidlem13 41840 31prm 43242 gbegt5 43408 gbowgt5 43409 sbgoldbo 43434 nnsum3primesle9 43441 nnsum4primesodd 43443 evengpop3 43445 |
Copyright terms: Public domain | W3C validator |