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	sseldi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ... 𝑁 ) )