Metamath Proof Explorer


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