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

Proof

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