Metamath Proof Explorer

Theorem elfzom1elp1fzo

Description: Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Proof shortened by AV, 5-Jan-2020)

Ref Expression
Assertion elfzom1elp1fzo ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → I + 1 ∈ 0 ..^ N

Proof

Step Hyp Ref Expression
1 elfzofz ⊢ I ∈ 0 ..^ N − 1 → I ∈ 0 … N − 1
2 elfzuz2 ⊢ I ∈ 0 … N − 1 → N − 1 ∈ ℤ ≥ 0
3 elnn0uz ⊢ N − 1 ∈ ℕ 0 ↔ N − 1 ∈ ℤ ≥ 0
4 zcn ⊢ N ∈ ℤ → N ∈ ℂ
5 4 anim1i ⊢ N ∈ ℤ ∧ N − 1 ∈ ℕ 0 → N ∈ ℂ ∧ N − 1 ∈ ℕ 0
6 elnnnn0 ⊢ N ∈ ℕ ↔ N ∈ ℂ ∧ N − 1 ∈ ℕ 0
7 5 6 sylibr ⊢ N ∈ ℤ ∧ N − 1 ∈ ℕ 0 → N ∈ ℕ
8 7 expcom ⊢ N − 1 ∈ ℕ 0 → N ∈ ℤ → N ∈ ℕ
9 3 8 sylbir ⊢ N − 1 ∈ ℤ ≥ 0 → N ∈ ℤ → N ∈ ℕ
10 1 2 9 3syl ⊢ I ∈ 0 ..^ N − 1 → N ∈ ℤ → N ∈ ℕ
11 10 impcom ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → N ∈ ℕ
12 1nn0 ⊢ 1 ∈ ℕ 0
13 12 a1i ⊢ N ∈ ℕ → 1 ∈ ℕ 0
14 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
15 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
16 13 14 15 3jca ⊢ N ∈ ℕ → 1 ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ 1 ≤ N
17 11 16 syl ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → 1 ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ 1 ≤ N
18 elfz2nn0 ⊢ 1 ∈ 0 … N ↔ 1 ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ 1 ≤ N
19 17 18 sylibr ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → 1 ∈ 0 … N
20 fzossrbm1 ⊢ N ∈ ℤ → 0 ..^ N − 1 ⊆ 0 ..^ N
21 20 adantr ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → 0 ..^ N − 1 ⊆ 0 ..^ N
22 fzossfz ⊢ 0 ..^ N ⊆ 0 … N
23 21 22 sstrdi ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → 0 ..^ N − 1 ⊆ 0 … N
24 simpr ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → I ∈ 0 ..^ N − 1
25 23 24 jca ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → 0 ..^ N − 1 ⊆ 0 … N ∧ I ∈ 0 ..^ N − 1
26 ssel2 ⊢ 0 ..^ N − 1 ⊆ 0 … N ∧ I ∈ 0 ..^ N − 1 → I ∈ 0 … N
27 elfzubelfz ⊢ I ∈ 0 … N → N ∈ 0 … N
28 25 26 27 3syl ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → N ∈ 0 … N
29 19 28 jca ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → 1 ∈ 0 … N ∧ N ∈ 0 … N
30 elfzodifsumelfzo ⊢ 1 ∈ 0 … N ∧ N ∈ 0 … N → I ∈ 0 ..^ N − 1 → I + 1 ∈ 0 ..^ N
31 29 24 30 sylc ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → I + 1 ∈ 0 ..^ N