![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 7re | Structured version Visualization version GIF version |
Description: The number 7 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
7re | ⊢ 7 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-7 12313 | . 2 ⊢ 7 = (6 + 1) | |
2 | 6re 12335 | . . 3 ⊢ 6 ∈ ℝ | |
3 | 1re 11246 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 11261 | . 2 ⊢ (6 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2821 | 1 ⊢ 7 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 (class class class)co 7419 ℝcr 11139 1c1 11141 + caddc 11143 6c6 12304 7c7 12305 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-1cn 11198 ax-icn 11199 ax-addcl 11200 ax-addrcl 11201 ax-mulcl 11202 ax-mulrcl 11203 ax-i2m1 11208 ax-1ne0 11209 ax-rrecex 11212 ax-cnre 11213 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 |
This theorem is referenced by: 8re 12341 8pos 12357 5lt7 12432 4lt7 12433 3lt7 12434 2lt7 12435 1lt7 12436 7lt8 12437 6lt8 12438 7lt9 12445 6lt9 12446 7lt10 12843 6lt10 12844 bposlem8 27269 lgsdir2lem1 27303 hgt750lem2 34415 hgt750leme 34421 problem4 35403 60gcd7e1 41608 lcmineqlem 41655 3lexlogpow5ineq1 41657 3lexlogpow5ineq2 41658 3lexlogpow5ineq4 41659 3lexlogpow5ineq3 41660 aks4d1p1p3 41672 aks4d1p1p2 41673 aks4d1p1p4 41674 aks4d1p1p7 41677 aks4d1p2 41680 aks4d1p3 41681 mod42tp1mod8 47079 stgoldbwt 47253 sbgoldbwt 47254 nnsum3primesle9 47271 nnsum4primesoddALTV 47274 evengpoap3 47276 bgoldbtbndlem1 47282 bgoldbtbnd 47286 |
Copyright terms: Public domain | W3C validator |