![]() |
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 12420 | . 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑁 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ℕcn 12153 ℕ0cn0 12413 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3447 df-un 3915 df-in 3917 df-ss 3927 df-n0 12414 |
This theorem is referenced by: 1nn0 12429 2nn0 12430 3nn0 12431 4nn0 12432 5nn0 12433 6nn0 12434 7nn0 12435 8nn0 12436 9nn0 12437 numlt 12643 declei 12654 numlti 12655 faclbnd4lem1 14193 divalglem6 16280 pockthi 16779 dec5dvds2 16937 modxp1i 16942 mod2xnegi 16943 43prm 16994 83prm 16995 317prm 16998 log2ublem2 26297 rpdp2cl2 31739 ballotlemfmpn 33094 ballotth 33137 circlevma 33255 12gcd5e1 40460 60gcd6e6 40461 60gcd7e1 40462 420lcm8e840 40468 lcmineqlem 40509 tgblthelfgott 45997 tgoldbach 45999 |
Copyright terms: Public domain | W3C validator |