![]() |
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 12275 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5nn 12294 | . . 3 ⊢ 5 ∈ ℕ | |
3 | peano2nn 12220 | . . 3 ⊢ (5 ∈ ℕ → (5 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (5 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2821 | 1 ⊢ 6 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 (class class class)co 7401 1c1 11106 + caddc 11108 ℕcn 12208 5c5 12266 6c6 12267 |
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-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 ax-un 7718 ax-1cn 11163 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7404 df-om 7849 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 |
This theorem is referenced by: 7nn 12300 6nn0 12489 ef01bndlem 16123 sin01bnd 16124 cos01bnd 16125 6gcd4e2 16476 6lcm4e12 16549 83prm 17052 139prm 17053 163prm 17054 prmo6 17059 vscandx 17260 vscaid 17261 lmodstr 17266 ipsstr 17277 lt6abl 19800 psrvalstr 21769 opsrvscaOLD 21914 tngvscaOLD 24471 sincos3rdpi 26356 1cubrlem 26677 quart1cl 26690 quart1lem 26691 quart1 26692 log2ub 26785 log2le1 26786 basellem5 26921 basellem8 26924 basellem9 26925 ppiublem1 27039 ppiublem2 27040 ppiub 27041 bpos1 27120 bposlem9 27129 itvndx 28112 itvid 28114 slotsinbpsd 28116 lngndxnitvndx 28118 trkgstr 28119 ttgvalOLD 28551 ttglemOLD 28553 ttgvscaOLD 28560 ttgdsOLD 28562 eengstr 28662 ex-cnv 30114 ex-dm 30116 ex-dvds 30133 ex-gcd 30134 ex-lcm 30135 resvvscaOLD 32879 hgt750lem 34118 60gcd6e6 41328 60gcd7e1 41329 12lcm5e60 41332 60lcm6e60 41333 60lcm7e420 41334 lcm6un 41342 lcmineqlem 41376 3lexlogpow5ineq1 41378 aks4d1p1p5 41399 aks4d1p1 41400 rmydioph 42208 expdiophlem2 42216 algstr 42374 mnringvscadOLD 43439 139prmALT 46715 31prm 46716 127prm 46718 6even 46830 gbowge7 46882 stgoldbwt 46895 sbgoldbwt 46896 mogoldbb 46904 sbgoldbo 46906 nnsum3primesle9 46913 nnsum4primeseven 46919 wtgoldbnnsum4prm 46921 bgoldbnnsum3prm 46923 zlmodzxzequa 47331 zlmodzxznm 47332 zlmodzxzequap 47334 zlmodzxzldeplem3 47337 zlmodzxzldep 47339 ldepsnlinclem2 47341 ldepsnlinc 47343 |
Copyright terms: Public domain | W3C validator |