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