Metamath Proof Explorer

Theorem elfzm12

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

Ref Expression
Assertion elfzm12 ⊢ N ∈ ℕ → M ∈ 1 … N − 1 → M ∈ 1 … N

Proof

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