Metamath Proof Explorer


Theorem nn0lt10b

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

Proof

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