Description: A nonnegative integer less than 1 is 0 . (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by OpenAI, 25-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0lt10b | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 ↔ 𝑁 = 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0 | ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) | |
2 | nnnlt1 | ⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 < 1 ) | |
3 | 2 | pm2.21d | ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 < 1 → 𝑁 = 0 ) ) |
4 | ax-1 | ⊢ ( 𝑁 = 0 → ( 𝑁 < 1 → 𝑁 = 0 ) ) | |
5 | 3 4 | jaoi | ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑁 < 1 → 𝑁 = 0 ) ) |
6 | 1 5 | sylbi | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 → 𝑁 = 0 ) ) |
7 | 0lt1 | ⊢ 0 < 1 | |
8 | breq1 | ⊢ ( 𝑁 = 0 → ( 𝑁 < 1 ↔ 0 < 1 ) ) | |
9 | 7 8 | mpbiri | ⊢ ( 𝑁 = 0 → 𝑁 < 1 ) |
10 | 6 9 | impbid1 | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 ↔ 𝑁 = 0 ) ) |