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 11176 | . 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑁 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 ℕcn 10897 ℕ0cn0 11169 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 df-n0 11170 |
This theorem is referenced by: 1nn0 11185 2nn0 11186 3nn0 11187 4nn0 11188 5nn0 11189 6nn0 11190 7nn0 11191 8nn0 11192 9nn0 11193 10nn0OLD 11194 numlt 11403 declei 11418 numlti 11421 faclbnd4lem1 12942 divalglem6 14959 pockthi 15449 dec5dvds2 15607 modxp1i 15612 mod2xnegi 15613 43prm 15667 83prm 15668 317prm 15671 strlemor2 15797 strlemor3 15798 log2ublem2 24474 ballotlemfmpn 29883 ballotth 29926 tgblthelfgott 40229 tgoldbach 40232 bgoldbachltOLD 40234 tgblthelfgottOLD 40236 tgoldbachOLD 40239 |
Copyright terms: Public domain | W3C validator |