Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3nn | Structured version Visualization version GIF version |
Description: 3 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3nn | ⊢ 3 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 11891 | . 2 ⊢ 3 = (2 + 1) | |
2 | 2nn 11900 | . . 3 ⊢ 2 ∈ ℕ | |
3 | peano2nn 11839 | . . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (2 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 3 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 (class class class)co 7210 1c1 10727 + caddc 10729 ℕcn 11827 2c2 11882 3c3 11883 |
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 |
This theorem is referenced by: 4nn 11910 3nn0 12105 3z 12207 ige3m2fz 13133 f1oun2prg 14479 sqrlem7 14809 bpoly4 15618 fsumcube 15619 sin01bnd 15743 egt2lt3 15764 rpnnen2lem2 15773 rpnnen2lem3 15774 rpnnen2lem4 15775 rpnnen2lem9 15780 rpnnen2lem11 15782 3lcm2e6woprm 16169 3lcm2e6 16285 prmo3 16591 5prm 16659 6nprm 16660 7prm 16661 9nprm 16663 11prm 16665 13prm 16666 17prm 16667 19prm 16668 23prm 16669 prmlem2 16670 37prm 16671 43prm 16672 83prm 16673 139prm 16674 163prm 16675 317prm 16676 631prm 16677 1259lem5 16685 2503lem1 16687 2503lem2 16688 2503lem3 16689 4001lem4 16694 4001prm 16695 mulrndx 16834 mulrid 16835 rngstr 16838 unifndx 16903 unifid 16904 lt6abl 19277 sramulr 20214 cnfldstr 20362 cnfldfun 20372 zlmmulr 20483 znmul 20503 opsrmulr 21006 tuslem 23161 tngmulr 23539 tangtx 25392 1cubrlem 25721 1cubr 25722 dcubic1lem 25723 dcubic2 25724 dcubic 25726 mcubic 25727 cubic2 25728 cubic 25729 quartlem3 25739 quart 25741 log2cnv 25824 log2tlbnd 25825 log2ublem1 25826 log2ublem2 25827 log2ub 25829 ppiublem1 26080 ppiub 26082 chtub 26090 bposlem3 26164 bposlem4 26165 bposlem5 26166 bposlem6 26167 bposlem9 26170 lgsdir2lem5 26207 dchrvmasumlem2 26376 dchrvmasumlema 26378 pntleml 26489 tgcgr4 26619 axlowdimlem16 27045 axlowdimlem17 27046 usgrexmpldifpr 27343 upgr3v3e3cycl 28260 ex-cnv 28517 ex-rn 28520 ex-mod 28529 resvmulr 31250 fib4 32080 circlevma 32331 circlemethhgt 32332 hgt750lema 32346 sinccvglem 33340 cnndvlem1 34451 mblfinlem3 35551 itg2addnclem2 35564 itg2addnc 35566 hlhilsmul 39690 lcm3un 39755 aks4d1p1 39815 3cubeslem2 40208 3cubeslem3r 40210 3cubes 40213 rmydioph 40537 rmxdioph 40539 expdiophlem2 40545 expdioph 40546 amgm3d 41486 lhe4.4ex1a 41618 257prm 44684 fmtno4prmfac193 44696 fmtno4nprmfac193 44697 3ndvds4 44718 139prmALT 44719 31prm 44720 127prm 44722 41prothprm 44742 341fppr2 44857 nfermltl2rev 44866 wtgoldbnnsum4prm 44925 bgoldbnnsum3prm 44927 bgoldbtbndlem1 44928 tgoldbach 44940 |
Copyright terms: Public domain | W3C validator |