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 ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑁 ) )

Proof

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