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

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

Proof

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