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 \in ℕ \land M \in ℤ_{\geq N}) \to N \in (1 \dots M)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \in ℕ$
2		eluzle	$⊢ M \in ℤ_{\geq N} \to N \leq M$
3	2	adantl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \leq M$
4		eluzelz	$⊢ M \in ℤ_{\geq N} \to M \in ℤ$
5	4	adantl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to M \in ℤ$
6		fznn	$⊢ M \in ℤ \to (N \in (1 \dots M) \leftrightarrow (N \in ℕ \land N \leq M))$
7	5 6	syl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to (N \in (1 \dots M) \leftrightarrow (N \in ℕ \land N \leq M))$
8	1 3 7	mpbir2and	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \in (1 \dots M)$

Metamath Proof Explorer