![]() |
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 12274 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4re 12292 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 1re 11210 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 11225 | . 2 ⊢ (4 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2830 | 1 ⊢ 5 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 (class class class)co 7404 ℝcr 11105 1c1 11107 + caddc 11109 4c4 12265 5c5 12266 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-i2m1 11174 ax-1ne0 11175 ax-rrecex 11178 ax-cnre 11179 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-ov 7407 df-2 12271 df-3 12272 df-4 12273 df-5 12274 |
This theorem is referenced by: 6re 12298 6pos 12318 3lt5 12386 2lt5 12387 1lt5 12388 5lt6 12389 4lt6 12390 5lt7 12395 4lt7 12396 5lt8 12402 4lt8 12403 5lt9 12410 4lt9 12411 5lt10 12808 4lt10 12809 5recm6rec 12817 ef01bndlem 16123 prm23ge5 16744 prmlem1 17037 vscandxnscandx 17265 slotsdifipndx 17276 slotstnscsi 17301 plendxnscandx 17314 slotsdnscsi 17333 rmodislmodOLD 20529 sralemOLD 20779 srascaOLD 20787 zlmlemOLD 21051 ppiublem1 26685 ppiub 26687 bposlem3 26769 bposlem4 26770 bposlem5 26771 bposlem6 26772 bposlem8 26774 bposlem9 26775 lgsdir2lem1 26808 gausslemma2dlem4 26852 2lgslem3 26887 cchhllemOLD 28125 ex-id 29667 ex-sqrt 29687 threehalves 32059 cyc3conja 32294 resvvscaOLD 32421 zlmdsOLD 32881 zlmtsetOLD 32883 hgt750lem2 33602 hgt750leme 33608 problem2 34589 12gcd5e1 40806 lcmineqlem23 40854 3lexlogpow2ineq1 40861 3lexlogpow2ineq2 40862 aks4d1p1p4 40874 aks4d1p1p6 40876 aks4d1p1p7 40877 aks4d1p1p5 40878 stoweidlem13 44664 31prm 46200 gbegt5 46364 gbowgt5 46365 sbgoldbo 46390 nnsum3primesle9 46397 nnsum4primesodd 46399 evengpop3 46401 |
Copyright terms: Public domain | W3C validator |