Theorem nn0le0eq0

Description: A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005)

	Ref	Expression
Assertion	nn0le0eq0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 0 ↔ 𝑁 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
2	1	biantrud	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
3		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
4		0re	⊢ 0 ∈ ℝ
5		letri3	⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
6	3 4 5	sylancl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
7	2 6	bitr4d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 0 ↔ 𝑁 = 0 ) )