Theorem elfzm12

Description: Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012)

	Ref	Expression
Assertion	elfzm12	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3	2	lem1d	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ≤ 𝑁 )
4		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
5		eluz	⊢ ( ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑁 − 1 ) ≤ 𝑁 ) )
6	4 5	mpancom	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑁 − 1 ) ≤ 𝑁 ) )
7	3 6	mpbird	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
8		fzss2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
9	1 7 8	3syl	⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
10	9	sseld	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) ) )