![]() |
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 12530 | . 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑁 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ℕcn 12263 ℕ0cn0 12523 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-un 3967 df-ss 3979 df-n0 12524 |
This theorem is referenced by: 1nn0 12539 2nn0 12540 3nn0 12541 4nn0 12542 5nn0 12543 6nn0 12544 7nn0 12545 8nn0 12546 9nn0 12547 numlt 12755 declei 12766 numlti 12767 faclbnd4lem1 14328 divalglem6 16431 pockthi 16940 dec5dvds2 17098 modxp1i 17103 mod2xnegi 17104 43prm 17155 83prm 17156 317prm 17159 log2ublem2 27004 rpdp2cl2 32849 ballotlemfmpn 34475 ballotth 34518 circlevma 34635 12gcd5e1 41984 60gcd6e6 41985 60gcd7e1 41986 420lcm8e840 41992 lcmineqlem 42033 tgblthelfgott 47739 tgoldbach 47741 |
Copyright terms: Public domain | W3C validator |