Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnnn0i | Structured version Visualization version GIF version |
Description: A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.) |
Ref | Expression |
---|---|
nnnn0i.1 | ⊢ 𝑁 ∈ ℕ |
Ref | Expression |
---|---|
nnnn0i | ⊢ 𝑁 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnnn0i.1 | . 2 ⊢ 𝑁 ∈ ℕ | |
2 | nnnn0 11898 | . 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑁 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 ℕcn 11632 ℕ0cn0 11891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-un 3941 df-in 3943 df-ss 3952 df-n0 11892 |
This theorem is referenced by: 1nn0 11907 2nn0 11908 3nn0 11909 4nn0 11910 5nn0 11911 6nn0 11912 7nn0 11913 8nn0 11914 9nn0 11915 numlt 12117 declei 12128 numlti 12129 faclbnd4lem1 13647 divalglem6 15743 pockthi 16237 dec5dvds2 16395 modxp1i 16400 mod2xnegi 16401 43prm 16449 83prm 16450 317prm 16453 log2ublem2 25519 rpdp2cl2 30554 ballotlemfmpn 31747 ballotth 31790 circlevma 31908 tgblthelfgott 43973 tgoldbach 43975 |
Copyright terms: Public domain | W3C validator |