Metamath Proof Explorer

Theorem elfz1uz

Description: Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022)

Ref Expression
Assertion elfz1uz ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → N ∈ 1 … M

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → N ∈ ℕ
2 eluzle ⊢ M ∈ ℤ ≥ N → N ≤ M
3 2 adantl ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → N ≤ M
4 eluzelz ⊢ M ∈ ℤ ≥ N → M ∈ ℤ
5 4 adantl ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → M ∈ ℤ
6 fznn ⊢ M ∈ ℤ → N ∈ 1 … M ↔ N ∈ ℕ ∧ N ≤ M
7 5 6 syl ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → N ∈ 1 … M ↔ N ∈ ℕ ∧ N ≤ M
8 1 3 7 mpbir2and ⊢ N ∈ ℕ ∧ M ∈ ℤ ≥ N → N ∈ 1 … M