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