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