Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 4nn | Structured version Visualization version GIF version |
Description: 4 is a positive integer. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
4nn | ⊢ 4 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-4 11690 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3nn 11704 | . . 3 ⊢ 3 ∈ ℕ | |
3 | peano2nn 11638 | . . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (3 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2906 | 1 ⊢ 4 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 (class class class)co 7145 1c1 10526 + caddc 10528 ℕcn 11626 3c3 11681 4c4 11682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 ax-1cn 10583 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-reu 3142 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-pss 3951 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 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 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-ov 7148 df-om 7570 df-wrecs 7936 df-recs 7997 df-rdg 8035 df-nn 11627 df-2 11688 df-3 11689 df-4 11690 |
This theorem is referenced by: 5nn 11711 4nn0 11904 4z 12004 fldiv4p1lem1div2 13193 fldiv4lem1div2 13195 iexpcyc 13557 fsumcube 15402 ef01bndlem 15525 flodddiv4 15752 6lcm4e12 15948 2expltfac 16414 8nprm 16433 37prm 16442 43prm 16443 83prm 16444 139prm 16445 631prm 16448 prmo4 16449 1259prm 16457 2503lem2 16459 starvndx 16611 starvid 16612 ressstarv 16614 srngstr 16615 homndx 16675 homid 16676 resshom 16679 prdsvalstr 16714 oppchomfval 16972 oppcbas 16976 rescco 17090 catstr 17215 lt6abl 18944 pcoass 23555 minveclem3 23959 iblitg 24296 dveflem 24503 tan4thpi 25027 atan1 25433 log2tlbnd 25450 log2ub 25454 bclbnd 25783 bpos1 25786 bposlem6 25792 bposlem7 25793 bposlem8 25794 bposlem9 25795 gausslemma2dlem4 25872 m1lgs 25891 2lgslem1a 25894 2lgslem3a 25899 2lgslem3b 25900 2lgslem3c 25901 2lgslem3d 25902 2sqreultlem 25950 2sqreunnltlem 25953 chebbnd1lem1 25972 chebbnd1lem2 25973 chebbnd1lem3 25974 pntibndlem1 26092 pntibndlem2 26094 pntibndlem3 26095 pntlema 26099 pntlemb 26100 pntlemg 26101 pntlemf 26108 upgr4cycl4dv4e 27891 fib5 31562 hgt750lem2 31822 hgt750leme 31828 rmydioph 39489 rmxdioph 39491 expdiophlem2 39497 inductionexd 40383 amgm4d 40431 257prm 43600 fmtno4sqrt 43610 fmtno4prmfac 43611 fmtno4prmfac193 43612 fmtno5nprm 43622 139prmALT 43636 mod42tp1mod8 43644 2exp340mod341 43775 341fppr2 43776 wtgoldbnnsum4prm 43844 bgoldbachlt 43855 tgblthelfgott 43857 |
Copyright terms: Public domain | W3C validator |