This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfzfzo

Description: Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	elfzfzo	$⊢ A \in (M ..^N) \leftrightarrow (A \in (M \dots N) \land A < N)$

Proof

Step	Hyp	Ref	Expression
1		elfzofz	$⊢ A \in (M ..^N) \to A \in (M \dots N)$
2		elfzolt2	$⊢ A \in (M ..^N) \to A < N$
3	1 2	jca	$⊢ A \in (M ..^N) \to (A \in (M \dots N) \land A < N)$
4		elfzuz	$⊢ A \in (M \dots N) \to A \in ℤ_{\geq M}$
5	4	adantr	$⊢ (A \in (M \dots N) \land A < N) \to A \in ℤ_{\geq M}$
6		elfzel2	$⊢ A \in (M \dots N) \to N \in ℤ$
7	6	adantr	$⊢ (A \in (M \dots N) \land A < N) \to N \in ℤ$
8		simpr	$⊢ (A \in (M \dots N) \land A < N) \to A < N$
9		elfzo2	$⊢ A \in (M ..^N) \leftrightarrow (A \in ℤ_{\geq M} \land N \in ℤ \land A < N)$
10	5 7 8 9	syl3anbrc	$⊢ (A \in (M \dots N) \land A < N) \to A \in (M ..^N)$
11	3 10	impbii	$⊢ A \in (M ..^N) \leftrightarrow (A \in (M \dots N) \land A < N)$