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 ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑀 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ𝑁 ) ) → 𝑁 ∈ ℕ )
2 eluzle ( 𝑀 ∈ ( ℤ𝑁 ) → 𝑁𝑀 )
3 2 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ𝑁 ) ) → 𝑁𝑀 )
4 eluzelz ( 𝑀 ∈ ( ℤ𝑁 ) → 𝑀 ∈ ℤ )
5 4 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ𝑁 ) ) → 𝑀 ∈ ℤ )
6 fznn ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) ) )
7 5 6 syl ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ𝑁 ) ) → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁𝑀 ) ) )
8 1 3 7 mpbir2and ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑀 ) )