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