![]() |
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 11550 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3nn 11564 | . . 3 ⊢ 3 ∈ ℕ | |
3 | peano2nn 11498 | . . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (3 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2879 | 1 ⊢ 4 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 (class class class)co 7016 1c1 10384 + caddc 10386 ℕcn 11486 3c3 11541 4c4 11542 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-1cn 10441 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-om 7437 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-nn 11487 df-2 11548 df-3 11549 df-4 11550 |
This theorem is referenced by: 5nn 11571 4nn0 11764 4z 11865 fldiv4p1lem1div2 13055 fldiv4lem1div2 13057 iexpcyc 13419 fsumcube 15247 ef01bndlem 15370 flodddiv4 15597 6lcm4e12 15789 2expltfac 16255 8nprm 16274 37prm 16283 43prm 16284 83prm 16285 139prm 16286 631prm 16289 prmo4 16290 1259prm 16298 2503lem2 16300 starvndx 16452 starvid 16453 ressstarv 16455 srngstr 16456 homndx 16516 homid 16517 resshom 16520 prdsvalstr 16555 oppchomfval 16813 oppcbas 16817 rescco 16931 catstr 17056 lt6abl 18736 pcoass 23311 minveclem3 23715 iblitg 24052 dveflem 24259 tan4thpi 24783 atan1 25187 log2tlbnd 25205 log2ub 25209 bclbnd 25538 bpos1 25541 bposlem6 25547 bposlem7 25548 bposlem8 25549 bposlem9 25550 gausslemma2dlem4 25627 m1lgs 25646 2lgslem1a 25649 2lgslem3a 25654 2lgslem3b 25655 2lgslem3c 25656 2lgslem3d 25657 2sqreultlem 25705 2sqreunnltlem 25708 chebbnd1lem1 25727 chebbnd1lem2 25728 chebbnd1lem3 25729 pntibndlem1 25847 pntibndlem2 25849 pntibndlem3 25850 pntlema 25854 pntlemb 25855 pntlemg 25856 pntlemf 25863 upgr4cycl4dv4e 27651 fib5 31280 hgt750lem2 31540 hgt750leme 31546 rmydioph 39115 rmxdioph 39117 expdiophlem2 39123 inductionexd 40009 amgm4d 40058 257prm 43225 fmtno4sqrt 43235 fmtno4prmfac 43236 fmtno4prmfac193 43237 fmtno5nprm 43247 139prmALT 43261 mod42tp1mod8 43269 2exp340mod341 43400 341fppr2 43401 wtgoldbnnsum4prm 43469 bgoldbachlt 43480 tgblthelfgott 43482 |
Copyright terms: Public domain | W3C validator |