Metamath Proof Explorer

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 ⊢ N ∈ ℕ 0 → 0 … N − 1 = ∅ ↔ N = 0

Proof

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