![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 6nn | Structured version Visualization version GIF version |
Description: 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Ref | Expression |
---|---|
6nn | ⊢ 6 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-6 11552 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5nn 11571 | . . 3 ⊢ 5 ∈ ℕ | |
3 | peano2nn 11498 | . . 3 ⊢ (5 ∈ ℕ → (5 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (5 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2879 | 1 ⊢ 6 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 (class class class)co 7016 1c1 10384 + caddc 10386 ℕcn 11486 5c5 11543 6c6 11544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-1cn 10441 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-om 7437 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-nn 11487 df-2 11548 df-3 11549 df-4 11550 df-5 11551 df-6 11552 |
This theorem is referenced by: 7nn 11577 6nn0 11766 ef01bndlem 15370 sin01bnd 15371 cos01bnd 15372 6gcd4e2 15715 6lcm4e12 15789 83prm 16285 139prm 16286 163prm 16287 prmo6 16292 vscandx 16463 vscaid 16464 lmodstr 16465 ipsstr 16472 ressvsca 16480 lt6abl 18736 psrvalstr 19831 opsrvsca 19949 tngvsca 22938 sincos3rdpi 24785 1cubrlem 25100 quart1cl 25113 quart1lem 25114 quart1 25115 log2ub 25209 log2le1 25210 basellem5 25344 basellem8 25347 basellem9 25348 ppiublem1 25460 ppiublem2 25461 ppiub 25462 bpos1 25541 bposlem9 25550 itvndx 25908 itvid 25910 trkgstr 25912 ttgval 26344 ttglem 26345 ttgvsca 26349 ttgds 26350 eengstr 26449 ex-cnv 27908 ex-dm 27910 ex-dvds 27927 ex-gcd 27928 ex-lcm 27929 resvvsca 30561 hgt750lem 31539 rmydioph 39115 expdiophlem2 39123 algstr 39281 139prmALT 43261 31prm 43262 127prm 43265 6even 43378 gbowge7 43430 stgoldbwt 43443 sbgoldbwt 43444 mogoldbb 43452 sbgoldbo 43454 nnsum3primesle9 43461 nnsum4primeseven 43467 wtgoldbnnsum4prm 43469 bgoldbnnsum3prm 43471 zlmodzxzequa 44051 zlmodzxznm 44052 zlmodzxzequap 44054 zlmodzxzldeplem3 44057 zlmodzxzldep 44059 ldepsnlinclem2 44061 ldepsnlinc 44063 |
Copyright terms: Public domain | W3C validator |