![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 5nn | Structured version Visualization version GIF version |
Description: 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.) |
Ref | Expression |
---|---|
5nn | ⊢ 5 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-5 11540 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4nn 11557 | . . 3 ⊢ 4 ∈ ℕ | |
3 | peano2nn 11487 | . . 3 ⊢ (4 ∈ ℕ → (4 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (4 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2877 | 1 ⊢ 5 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2079 (class class class)co 7007 1c1 10373 + caddc 10375 ℕcn 11475 4c4 11531 5c5 11532 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-1cn 10430 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-ral 3108 df-rex 3109 df-reu 3110 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-ov 7010 df-om 7428 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-nn 11476 df-2 11537 df-3 11538 df-4 11539 df-5 11540 |
This theorem is referenced by: 6nn 11563 5nn0 11754 prm23ge5 15969 dec5dvds 16217 dec5nprm 16219 dec2nprm 16220 5prm 16259 10nprm 16264 23prm 16269 prmlem2 16270 43prm 16272 83prm 16273 317prm 16276 prmo5 16279 scandx 16449 scaid 16450 lmodstr 16453 ipsstr 16460 resssca 16467 ccondx 16506 ccoid 16507 ressco 16509 slotsbhcdif 16510 prdsvalstr 16543 oppchomfval 16801 oppcbas 16805 rescco 16919 catstr 17044 lt6abl 18724 mgpsca 18924 psrvalstr 19819 opsrsca 19938 tngsca 22925 log2ublem1 25194 log2ublem2 25195 log2ub 25197 birthday 25202 ppiublem1 25448 ppiublem2 25449 ppiub 25450 bclbnd 25526 bposlem3 25532 bposlem4 25533 bposlem5 25534 bposlem6 25535 bposlem8 25537 bposlem9 25538 lgsdir2lem3 25573 ex-eprel 27892 ex-xp 27895 fib6 31237 hgt750lem2 31496 hgt750leme 31502 rmydioph 39047 expdiophlem2 39055 algstr 39213 inductionexd 39941 257prm 43159 fmtno4prmfac193 43171 31prm 43196 41prothprm 43220 gbowge7 43364 gbege6 43366 stgoldbwt 43377 sbgoldbwt 43378 sbgoldbm 43385 sbgoldbo 43388 nnsum3primesle9 43395 |
Copyright terms: Public domain | W3C validator |