| 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 12533 | . 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑁 ∈ ℕ0 |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ℕcn 12266 ℕ0cn0 12526 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-ss 3968 df-n0 12527 |
| This theorem is referenced by: 1nn0 12542 2nn0 12543 3nn0 12544 4nn0 12545 5nn0 12546 6nn0 12547 7nn0 12548 8nn0 12549 9nn0 12550 numlt 12758 declei 12769 numlti 12770 faclbnd4lem1 14332 divalglem6 16435 pockthi 16945 dec5dvds2 17103 modxp1i 17108 mod2xnegi 17109 43prm 17159 83prm 17160 317prm 17163 log2ublem2 26990 rpdp2cl2 32865 ballotlemfmpn 34497 ballotth 34540 circlevma 34657 12gcd5e1 42004 60gcd6e6 42005 60gcd7e1 42006 420lcm8e840 42012 lcmineqlem 42053 tgblthelfgott 47802 tgoldbach 47804 |
| Copyright terms: Public domain | W3C validator |