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 11919 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3nn 11933 | . . 3 ⊢ 3 ∈ ℕ | |
3 | peano2nn 11866 | . . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (3 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2835 | 1 ⊢ 4 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 (class class class)co 7231 1c1 10754 + caddc 10756 ℕcn 11854 3c3 11910 4c4 11911 |
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 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5206 ax-nul 5213 ax-pr 5336 ax-un 7541 ax-1cn 10811 |
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 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-ral 3067 df-rex 3068 df-reu 3069 df-rab 3071 df-v 3422 df-sbc 3709 df-csb 3826 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-pss 3899 df-nul 4252 df-if 4454 df-pw 4529 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4834 df-iun 4920 df-br 5068 df-opab 5130 df-mpt 5150 df-tr 5176 df-id 5469 df-eprel 5474 df-po 5482 df-so 5483 df-fr 5523 df-we 5525 df-xp 5571 df-rel 5572 df-cnv 5573 df-co 5574 df-dm 5575 df-rn 5576 df-res 5577 df-ima 5578 df-pred 6175 df-ord 6233 df-on 6234 df-lim 6235 df-suc 6236 df-iota 6355 df-fun 6399 df-fn 6400 df-f 6401 df-f1 6402 df-fo 6403 df-f1o 6404 df-fv 6405 df-ov 7234 df-om 7663 df-wrecs 8067 df-recs 8128 df-rdg 8166 df-nn 11855 df-2 11917 df-3 11918 df-4 11919 |
This theorem is referenced by: 5nn 11940 4nn0 12133 4z 12235 fldiv4p1lem1div2 13434 fldiv4lem1div2 13436 iexpcyc 13799 fsumcube 15646 ef01bndlem 15769 flodddiv4 15998 6lcm4e12 16197 2expltfac 16670 8nprm 16689 37prm 16698 43prm 16699 83prm 16700 139prm 16701 631prm 16704 prmo4 16705 1259prm 16713 2503lem2 16715 starvndx 16869 starvid 16870 srngstr 16874 homndx 16942 homid 16943 prdsvalstr 16981 oppchomfvalOLD 17242 oppcbas 17246 resccoOLD 17362 catstr 17489 lt6abl 19304 pcoass 23945 minveclem3 24350 iblitg 24690 dveflem 24900 tan4thpi 25428 atan1 25835 log2tlbnd 25852 log2ub 25856 bclbnd 26185 bpos1 26188 bposlem6 26194 bposlem7 26195 bposlem8 26196 bposlem9 26197 gausslemma2dlem4 26274 m1lgs 26293 2lgslem1a 26296 2lgslem3a 26301 2lgslem3b 26302 2lgslem3c 26303 2lgslem3d 26304 2sqreultlem 26352 2sqreunnltlem 26355 chebbnd1lem1 26374 chebbnd1lem2 26375 chebbnd1lem3 26376 pntibndlem1 26494 pntibndlem2 26496 pntibndlem3 26497 pntlema 26501 pntlemb 26502 pntlemg 26503 pntlemf 26510 upgr4cycl4dv4e 28292 fib5 32108 hgt750lem2 32368 hgt750leme 32374 iccioo01 35258 420gcd8e4 39774 420lcm8e840 39779 lcm4un 39784 lcmineqlem23 39819 lcmineqlem 39820 3lexlogpow5ineq2 39823 aks4d1p1p5 39842 rmydioph 40567 rmxdioph 40569 expdiophlem2 40575 inductionexd 41470 amgm4d 41517 257prm 44714 fmtno4sqrt 44724 fmtno4prmfac 44725 fmtno4prmfac193 44726 fmtno5nprm 44736 139prmALT 44749 mod42tp1mod8 44755 2exp340mod341 44886 341fppr2 44887 wtgoldbnnsum4prm 44955 bgoldbachlt 44966 tgblthelfgott 44968 prstcleval 46050 prstcocval 46052 |
Copyright terms: Public domain | W3C validator |