Metamath Proof Explorer

Theorem ige2m2fzo

Description: Membership of an integer greater than 1 decreased by 2 in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 3-Oct-2018)

Ref Expression
Assertion ige2m2fzo ⊢ N ∈ ℤ ≥ 2 → N − 2 ∈ 0 ..^ N − 1

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ N ∈ ℤ ≥ 2 → 2 ∈ ℤ
2 1z ⊢ 1 ∈ ℤ
3 1 2 jctir ⊢ N ∈ ℤ ≥ 2 → 2 ∈ ℤ ∧ 1 ∈ ℤ
4 1lt2 ⊢ 1 < 2
5 4 jctr ⊢ N ∈ ℤ ≥ 2 → N ∈ ℤ ≥ 2 ∧ 1 < 2
6 eluzgtdifelfzo ⊢ 2 ∈ ℤ ∧ 1 ∈ ℤ → N ∈ ℤ ≥ 2 ∧ 1 < 2 → N − 2 ∈ 0 ..^ N − 1
7 3 5 6 sylc ⊢ N ∈ ℤ ≥ 2 → N − 2 ∈ 0 ..^ N − 1