This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ 0 ↔ N ∈ ℂ ∧ N + 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
2 nn0p1nn ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ
3 1 2 jca ⊢ N ∈ ℕ 0 → N ∈ ℂ ∧ N + 1 ∈ ℕ
4 simpl ⊢ N ∈ ℂ ∧ N + 1 ∈ ℕ → N ∈ ℂ
5 ax-1cn ⊢ 1 ∈ ℂ
6 pncan ⊢ N ∈ ℂ ∧ 1 ∈ ℂ → N + 1 - 1 = N
7 4 5 6 sylancl ⊢ N ∈ ℂ ∧ N + 1 ∈ ℕ → N + 1 - 1 = N
8 nnm1nn0 ⊢ N + 1 ∈ ℕ → N + 1 - 1 ∈ ℕ 0
9 8 adantl ⊢ N ∈ ℂ ∧ N + 1 ∈ ℕ → N + 1 - 1 ∈ ℕ 0
10 7 9 eqeltrrd ⊢ N ∈ ℂ ∧ N + 1 ∈ ℕ → N ∈ ℕ 0
11 3 10 impbii ⊢ N ∈ ℕ 0 ↔ N ∈ ℂ ∧ N + 1 ∈ ℕ