This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ige2m1fz

Description: Membership in a 0-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 18-Jun-2018) (Proof shortened by Alexander van der Vekens, 15-Sep-2018)

Ref Expression
Assertion ige2m1fz ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
2 fzss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
3 1 2 ax-mp ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
4 2z ⊢ 2 ∈ ℤ
5 4 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 2 ∈ ℤ )
6 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
7 6 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
8 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 2 ≤ 𝑁 )
9 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
10 5 7 8 9 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
11 ige2m1fz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ( 1 ... 𝑁 ) )
12 10 11 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 1 ... 𝑁 ) )
13 3 12 sselid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ... 𝑁 ) )