![]() |
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 12357 | . 2 ⊢ 3 = (2 + 1) | |
2 | 2nn 12366 | . . 3 ⊢ 2 ∈ ℕ | |
3 | peano2nn 12305 | . . 3 ⊢ (2 ∈ ℕ → (2 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (2 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2840 | 1 ⊢ 3 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2108 (class class class)co 7448 1c1 11185 + caddc 11187 ℕcn 12293 2c2 12348 3c3 12349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770 ax-1cn 11242 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-ov 7451 df-om 7904 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-nn 12294 df-2 12356 df-3 12357 |
This theorem is referenced by: 4nn 12376 3nn0 12571 3z 12676 ige3m2fz 13608 fvf1tp 13840 tpf1ofv0 14545 tpf1ofv1 14546 tpf1ofv2 14547 tpfo 14549 f1oun2prg 14966 01sqrexlem7 15297 bpoly4 16107 fsumcube 16108 sin01bnd 16233 egt2lt3 16254 rpnnen2lem2 16263 rpnnen2lem3 16264 rpnnen2lem4 16265 rpnnen2lem9 16270 rpnnen2lem11 16272 3lcm2e6woprm 16662 3lcm2e6 16779 prmo3 17088 5prm 17156 6nprm 17157 7prm 17158 9nprm 17160 11prm 17162 13prm 17163 17prm 17164 19prm 17165 23prm 17166 prmlem2 17167 37prm 17168 43prm 17169 83prm 17170 139prm 17171 163prm 17172 317prm 17173 631prm 17174 1259lem5 17182 2503lem1 17184 2503lem2 17185 2503lem3 17186 4001lem4 17191 4001prm 17192 mulrndx 17352 mulridx 17353 rngstr 17357 unifndx 17454 unifid 17455 unifndxnn 17456 slotsdifunifndx 17460 lt6abl 19937 sramulrOLD 21205 cnfldstr 21389 cnfldstrOLD 21404 cnfldfunALTOLDOLD 21416 zlmmulrOLD 21557 znmulOLD 21583 opsrmulrOLD 22097 tuslemOLD 24297 tngmulrOLD 24682 tangtx 26565 1cubrlem 26902 1cubr 26903 dcubic1lem 26904 dcubic2 26905 dcubic 26907 mcubic 26908 cubic2 26909 cubic 26910 quartlem3 26920 quart 26922 log2cnv 27005 log2tlbnd 27006 log2ublem1 27007 log2ublem2 27008 log2ub 27010 ppiublem1 27264 ppiub 27266 chtub 27274 bposlem3 27348 bposlem4 27349 bposlem5 27350 bposlem6 27351 bposlem9 27354 lgsdir2lem5 27391 dchrvmasumlem2 27560 dchrvmasumlema 27562 pntleml 27673 tgcgr4 28557 axlowdimlem16 28990 axlowdimlem17 28991 usgrexmpldifpr 29293 upgr3v3e3cycl 30212 ex-cnv 30469 ex-rn 30472 ex-mod 30481 resvmulrOLD 33331 2sqr3minply 33738 fib4 34369 circlevma 34619 circlemethhgt 34620 hgt750lema 34634 sinccvglem 35640 cnndvlem1 36503 mblfinlem3 37619 itg2addnclem2 37632 itg2addnc 37634 hlhilsmulOLD 41902 lcm3un 41972 aks4d1p1 42033 3cubeslem2 42641 3cubeslem3r 42643 3cubes 42646 rmydioph 42971 rmxdioph 42973 expdiophlem2 42979 expdioph 42980 amgm3d 44161 lhe4.4ex1a 44298 257prm 47435 fmtno4prmfac193 47447 fmtno4nprmfac193 47448 3ndvds4 47469 139prmALT 47470 31prm 47471 127prm 47473 41prothprm 47493 341fppr2 47608 nfermltl2rev 47617 wtgoldbnnsum4prm 47676 bgoldbnnsum3prm 47678 bgoldbtbndlem1 47679 tgoldbach 47691 grtriclwlk3 47796 |
Copyright terms: Public domain | W3C validator |