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 ) )