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 11893 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4nn 11910 | . . 3 ⊢ 4 ∈ ℕ | |
3 | peano2nn 11839 | . . 3 ⊢ (4 ∈ ℕ → (4 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (4 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 5 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 (class class class)co 7210 1c1 10727 + caddc 10729 ℕcn 11827 4c4 11884 5c5 11885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 ax-un 7520 ax-1cn 10784 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2940 df-ral 3063 df-rex 3064 df-reu 3065 df-rab 3067 df-v 3407 df-sbc 3692 df-csb 3809 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-pss 3882 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-tp 4543 df-op 4545 df-uni 4817 df-iun 4903 df-br 5051 df-opab 5113 df-mpt 5133 df-tr 5159 df-id 5452 df-eprel 5457 df-po 5465 df-so 5466 df-fr 5506 df-we 5508 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6157 df-ord 6213 df-on 6214 df-lim 6215 df-suc 6216 df-iota 6335 df-fun 6379 df-fn 6380 df-f 6381 df-f1 6382 df-fo 6383 df-f1o 6384 df-fv 6385 df-ov 7213 df-om 7642 df-wrecs 8044 df-recs 8105 df-rdg 8143 df-nn 11828 df-2 11890 df-3 11891 df-4 11892 df-5 11893 |
This theorem is referenced by: 6nn 11916 5nn0 12107 prm23ge5 16365 dec5dvds 16614 dec5nprm 16616 dec2nprm 16617 5prm 16659 10nprm 16664 23prm 16669 prmlem2 16670 43prm 16672 83prm 16673 317prm 16676 prmo5 16679 scandx 16852 scaid 16853 lmodstr 16858 ipsstr 16866 ccondx 16917 ccoid 16918 slotsbhcdif 16919 prdsvalstr 16954 oppchomfvalOLD 17215 oppcbas 17219 resccoOLD 17335 catstr 17462 lt6abl 19277 mgpsca 19508 psrvalstr 20872 opsrsca 21008 tngsca 23540 log2ublem1 25826 log2ublem2 25827 log2ub 25829 birthday 25834 ppiublem1 26080 ppiublem2 26081 ppiub 26082 bclbnd 26158 bposlem3 26164 bposlem4 26165 bposlem5 26166 bposlem6 26167 bposlem8 26169 bposlem9 26170 lgsdir2lem3 26205 ex-eprel 28513 ex-xp 28516 fib6 32082 hgt750lem2 32341 hgt750leme 32347 12gcd5e1 39743 12lcm5e60 39748 lcm5un 39757 lcmineqlem 39792 3lexlogpow5ineq1 39794 3lexlogpow2ineq1 39798 3lexlogpow2ineq2 39799 3lexlogpow5ineq5 39800 aks4d1p1p6 39812 aks4d1p1 39815 rmydioph 40537 expdiophlem2 40545 algstr 40703 inductionexd 41440 mnringscad 41513 257prm 44684 fmtno4prmfac193 44696 31prm 44720 41prothprm 44742 gbowge7 44886 gbege6 44888 stgoldbwt 44899 sbgoldbwt 44900 sbgoldbm 44907 sbgoldbo 44910 nnsum3primesle9 44917 prstcleval 46020 prstcocval 46022 |
Copyright terms: Public domain | W3C validator |