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 11895 | . 2 ⊢ 7 = (6 + 1) | |
2 | 6re 11917 | . . 3 ⊢ 6 ∈ ℝ | |
3 | 1re 10830 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10845 | . 2 ⊢ (6 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 7 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 (class class class)co 7210 ℝcr 10725 1c1 10727 + caddc 10729 6c6 11886 7c7 11887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-1cn 10784 ax-icn 10785 ax-addcl 10786 ax-addrcl 10787 ax-mulcl 10788 ax-mulrcl 10789 ax-i2m1 10794 ax-1ne0 10795 ax-rrecex 10798 ax-cnre 10799 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2940 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-iota 6335 df-fv 6385 df-ov 7213 df-2 11890 df-3 11891 df-4 11892 df-5 11893 df-6 11894 df-7 11895 |
This theorem is referenced by: 8re 11923 8pos 11939 5lt7 12014 4lt7 12015 3lt7 12016 2lt7 12017 1lt7 12018 7lt8 12019 6lt8 12020 7lt9 12027 6lt9 12028 7lt10 12423 6lt10 12424 bposlem8 26169 lgsdir2lem1 26203 hgt750lem2 32341 hgt750leme 32347 problem4 33336 60gcd7e1 39745 lcmineqlem 39792 3lexlogpow5ineq1 39794 3lexlogpow5ineq2 39795 3lexlogpow5ineq4 39796 3lexlogpow5ineq3 39797 aks4d1p1p3 39808 aks4d1p1p2 39809 aks4d1p1p4 39810 aks4d1p1p7 39813 aks4d1p2 39816 aks4d1p3 39817 mod42tp1mod8 44725 stgoldbwt 44899 sbgoldbwt 44900 nnsum3primesle9 44917 nnsum4primesoddALTV 44920 evengpoap3 44922 bgoldbtbndlem1 44928 bgoldbtbnd 44932 |
Copyright terms: Public domain | W3C validator |