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