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 12097 | . 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝑁 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 ℕcn 11830 ℕ0cn0 12090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-un 3871 df-in 3873 df-ss 3883 df-n0 12091 |
This theorem is referenced by: 1nn0 12106 2nn0 12107 3nn0 12108 4nn0 12109 5nn0 12110 6nn0 12111 7nn0 12112 8nn0 12113 9nn0 12114 numlt 12318 declei 12329 numlti 12330 faclbnd4lem1 13859 divalglem6 15959 pockthi 16460 dec5dvds2 16618 modxp1i 16623 mod2xnegi 16624 43prm 16675 83prm 16676 317prm 16679 log2ublem2 25830 rpdp2cl2 30877 ballotlemfmpn 32173 ballotth 32216 circlevma 32334 12gcd5e1 39745 60gcd6e6 39746 60gcd7e1 39747 420lcm8e840 39753 lcmineqlem 39794 tgblthelfgott 44940 tgoldbach 44942 |
Copyright terms: Public domain | W3C validator |