![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 6re | Structured version Visualization version GIF version |
Description: The number 6 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
6re | ⊢ 6 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-6 11121 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 11137 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 10077 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10091 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2726 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 (class class class)co 6690 ℝcr 9973 1c1 9975 + caddc 9977 5c5 11111 6c6 11112 |
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 df-6 11121 |
This theorem is referenced by: 6cn 11140 7re 11141 7pos 11158 4lt6 11243 3lt6 11244 2lt6 11245 1lt6 11246 6lt7 11247 5lt7 11248 6lt8 11254 5lt8 11255 6lt9 11262 5lt9 11263 6lt10OLD 11271 5lt10OLD 11272 8th4div3 11290 halfpm6th 11291 div4p1lem1div2 11325 6lt10 11714 5lt10 11715 5recm6rec 11724 bpoly2 14832 bpoly3 14833 efi4p 14911 resin4p 14912 recos4p 14913 ef01bndlem 14958 sin01bnd 14959 cos01bnd 14960 lt6abl 18342 sralem 19225 sravsca 19230 zlmlem 19913 sincos6thpi 24312 basellem5 24856 basellem8 24859 basellem9 24860 ppiublem1 24972 ppiublem2 24973 ppiub 24974 chtub 24982 bposlem6 25059 bposlem8 25061 ex-res 27428 zlmds 30136 zlmtset 30137 hgt750lemd 30854 hgt750lem2 30858 hgt750leme 30864 problem4 31688 problem5 31689 pigt3 33532 gbegt5 41974 gbowgt5 41975 gbowge7 41976 gboge9 41977 sbgoldbwt 41990 sgoldbeven3prm 41996 mogoldbb 41998 sbgoldbo 42000 nnsum3primesle9 42007 nnsum4primesodd 42009 wtgoldbnnsum4prm 42015 bgoldbnnsum3prm 42017 pgrple2abl 42471 |
Copyright terms: Public domain | W3C validator |