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 ... 𝑀 ) )