Theorem fz0n

Description: The sequence ( 0 ... ( N - 1 ) ) is empty iff N is zero. (Contributed by Scott Fenton, 16-May-2014)

	Ref	Expression
Assertion	fz0n	⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ... ( 𝑁 − 1 ) ) = ∅ ↔ 𝑁 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
3		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
4	2 3	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℤ )
5		fzn	⊢ ( ( 0 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) < 0 ↔ ( 0 ... ( 𝑁 − 1 ) ) = ∅ ) )
6	1 4 5	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) < 0 ↔ ( 0 ... ( 𝑁 − 1 ) ) = ∅ ) )
7		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
8		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
9		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
10		1re	⊢ 1 ∈ ℝ
11		subge0	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 1 ) ↔ 1 ≤ 𝑁 ) )
12		0re	⊢ 0 ∈ ℝ
13		resubcl	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑁 − 1 ) ∈ ℝ )
14		lenlt	⊢ ( ( 0 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 1 ) ↔ ¬ ( 𝑁 − 1 ) < 0 ) )
15	12 13 14	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 1 ) ↔ ¬ ( 𝑁 − 1 ) < 0 ) )
16	11 15	bitr3d	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 ≤ 𝑁 ↔ ¬ ( 𝑁 − 1 ) < 0 ) )
17	9 10 16	sylancl	⊢ ( 𝑁 ∈ ℕ → ( 1 ≤ 𝑁 ↔ ¬ ( 𝑁 − 1 ) < 0 ) )
18	8 17	mpbid	⊢ ( 𝑁 ∈ ℕ → ¬ ( 𝑁 − 1 ) < 0 )
19		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
20	19	neneqd	⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 = 0 )
21	18 20	2falsed	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) < 0 ↔ 𝑁 = 0 ) )
22		oveq1	⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) = ( 0 − 1 ) )
23		df-neg	⊢ - 1 = ( 0 − 1 )
24	22 23	eqtr4di	⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) = - 1 )
25		neg1lt0	⊢ - 1 < 0
26	24 25	eqbrtrdi	⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) < 0 )
27		id	⊢ ( 𝑁 = 0 → 𝑁 = 0 )
28	26 27	2thd	⊢ ( 𝑁 = 0 → ( ( 𝑁 − 1 ) < 0 ↔ 𝑁 = 0 ) )
29	21 28	jaoi	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( 𝑁 − 1 ) < 0 ↔ 𝑁 = 0 ) )
30	7 29	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) < 0 ↔ 𝑁 = 0 ) )
31	6 30	bitr3d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ... ( 𝑁 − 1 ) ) = ∅ ↔ 𝑁 = 0 ) )