![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 8nn | Structured version Visualization version GIF version |
Description: 8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Ref | Expression |
---|---|
8nn | ⊢ 8 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 11269 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7nn 11374 | . . 3 ⊢ 7 ∈ ℕ | |
3 | peano2nn 11216 | . . 3 ⊢ (7 ∈ ℕ → (7 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (7 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2827 | 1 ⊢ 8 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2131 (class class class)co 6805 1c1 10121 + caddc 10123 ℕcn 11204 7c7 11259 8c8 11260 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-1cn 10178 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-reu 3049 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-pss 3723 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-tp 4318 df-op 4320 df-uni 4581 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-tr 4897 df-id 5166 df-eprel 5171 df-po 5179 df-so 5180 df-fr 5217 df-we 5219 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-pred 5833 df-ord 5879 df-on 5880 df-lim 5881 df-suc 5882 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-ov 6808 df-om 7223 df-wrecs 7568 df-recs 7629 df-rdg 7667 df-nn 11205 df-2 11263 df-3 11264 df-4 11265 df-5 11266 df-6 11267 df-7 11268 df-8 11269 |
This theorem is referenced by: 9nn 11376 8nn0 11499 37prm 16022 43prm 16023 83prm 16024 317prm 16027 1259lem4 16035 1259lem5 16036 2503prm 16041 4001prm 16046 ipndx 16216 ipid 16217 ipsstr 16218 ressip 16227 phlstr 16228 tngip 22644 quart1cl 24772 quart1lem 24773 quart1 24774 log2tlbnd 24863 bposlem8 25207 lgsdir2lem2 25242 lgsdir2lem3 25243 2lgslem3a1 25316 2lgslem3b1 25317 2lgslem3c1 25318 2lgslem3d1 25319 2lgslem4 25322 2lgsoddprmlem2 25325 pntlemr 25482 pntlemj 25483 edgfid 26060 edgfndxnn 26061 edgfndxid 26062 baseltedgf 26063 ex-prmo 27619 hgt750lem 31030 hgt750lem2 31031 rmydioph 38075 fmtnoprmfac2lem1 41980 127prm 42017 mod42tp1mod8 42021 8even 42124 nnsum4primesevenALTV 42191 wtgoldbnnsum4prm 42192 bgoldbnnsum3prm 42194 bgoldbtbndlem1 42195 tgblthelfgott 42205 tgoldbachlt 42206 bgoldbachltOLD 42209 tgblthelfgottOLD 42211 tgoldbachltOLD 42212 |
Copyright terms: Public domain | W3C validator |