Metamath Proof Explorer

Theorem elnnnn0

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004)

Ref Expression
Assertion elnnnn0 ⊢ N ∈ ℕ ↔ N ∈ ℂ ∧ N − 1 ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 nncn ⊢ N ∈ ℕ → N ∈ ℂ
2 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
3 2 eleq1d ⊢ N ∈ ℂ → N - 1 + 1 ∈ ℕ ↔ N ∈ ℕ
4 peano2cnm ⊢ N ∈ ℂ → N − 1 ∈ ℂ
5 4 biantrurd ⊢ N ∈ ℂ → N - 1 + 1 ∈ ℕ ↔ N − 1 ∈ ℂ ∧ N - 1 + 1 ∈ ℕ
6 3 5 bitr3d ⊢ N ∈ ℂ → N ∈ ℕ ↔ N − 1 ∈ ℂ ∧ N - 1 + 1 ∈ ℕ
7 elnn0nn ⊢ N − 1 ∈ ℕ 0 ↔ N − 1 ∈ ℂ ∧ N - 1 + 1 ∈ ℕ
8 6 7 bitr4di ⊢ N ∈ ℂ → N ∈ ℕ ↔ N − 1 ∈ ℕ 0
9 1 8 biadanii ⊢ N ∈ ℕ ↔ N ∈ ℂ ∧ N − 1 ∈ ℕ 0