# Metamath Proof Explorer

## Theorem elnn0nn

Description: The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elnn0nn ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℂ\wedge {N}+1\in ℕ\right)$

### Proof

Step Hyp Ref Expression
1 nn0cn ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℂ$
2 nn0p1nn ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in ℕ$
3 1 2 jca ${⊢}{N}\in {ℕ}_{0}\to \left({N}\in ℂ\wedge {N}+1\in ℕ\right)$
4 simpl ${⊢}\left({N}\in ℂ\wedge {N}+1\in ℕ\right)\to {N}\in ℂ$
5 ax-1cn ${⊢}1\in ℂ$
6 pncan ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\to {N}+1-1={N}$
7 4 5 6 sylancl ${⊢}\left({N}\in ℂ\wedge {N}+1\in ℕ\right)\to {N}+1-1={N}$
8 nnm1nn0 ${⊢}{N}+1\in ℕ\to {N}+1-1\in {ℕ}_{0}$
9 8 adantl ${⊢}\left({N}\in ℂ\wedge {N}+1\in ℕ\right)\to {N}+1-1\in {ℕ}_{0}$
10 7 9 eqeltrrd ${⊢}\left({N}\in ℂ\wedge {N}+1\in ℕ\right)\to {N}\in {ℕ}_{0}$
11 3 10 impbii ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℂ\wedge {N}+1\in ℕ\right)$