![]() |
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 12330 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4nn 12347 | . . 3 ⊢ 4 ∈ ℕ | |
3 | peano2nn 12276 | . . 3 ⊢ (4 ∈ ℕ → (4 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (4 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2822 | 1 ⊢ 5 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 (class class class)co 7424 1c1 11159 + caddc 11161 ℕcn 12264 4c4 12321 5c5 12322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746 ax-1cn 11216 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-ov 7427 df-om 7877 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 |
This theorem is referenced by: 6nn 12353 5nn0 12544 prm23ge5 16817 dec5dvds 17066 dec5nprm 17068 dec2nprm 17069 5prm 17111 10nprm 17116 23prm 17121 prmlem2 17122 43prm 17124 83prm 17125 317prm 17128 prmo5 17131 scandx 17328 scaid 17329 lmodstr 17339 ipsstr 17350 ccondx 17427 ccoid 17428 slotsbhcdif 17429 slotsbhcdifOLD 17430 slotsdifplendx2 17431 slotsdifocndx 17432 prdsvalstr 17467 oppchomfvalOLD 17728 oppcbasOLD 17733 resccoOLD 17850 catstr 17981 lt6abl 19893 mgpscaOLD 20126 psrvalstr 21913 opsrscaOLD 22067 tngscaOLD 24650 log2ublem1 26974 log2ublem2 26975 log2ub 26977 birthday 26982 ppiublem1 27231 ppiublem2 27232 ppiub 27233 bclbnd 27309 bposlem3 27315 bposlem4 27316 bposlem5 27317 bposlem6 27318 bposlem8 27320 bposlem9 27321 lgsdir2lem3 27356 ex-eprel 30366 ex-xp 30369 fib6 34240 hgt750lem2 34498 hgt750leme 34504 12gcd5e1 41702 12lcm5e60 41707 lcm5un 41716 lcmineqlem 41751 3lexlogpow5ineq1 41753 3lexlogpow2ineq1 41757 3lexlogpow2ineq2 41758 3lexlogpow5ineq5 41759 aks4d1p1p6 41772 aks4d1p1 41775 rmydioph 42672 expdiophlem2 42680 algstr 42838 inductionexd 43822 mnringscadOLD 43897 257prm 47133 fmtno4prmfac193 47145 31prm 47169 41prothprm 47191 gbowge7 47335 gbege6 47337 stgoldbwt 47348 sbgoldbwt 47349 sbgoldbm 47356 sbgoldbo 47359 nnsum3primesle9 47366 prstclevalOLD 48390 prstcocvalOLD 48393 |
Copyright terms: Public domain | W3C validator |