fzolb

Description: The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with M < N . This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate M e. ( ZZ>=N ) . (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	fzolb	$⊢ M \in (M ..^N) \leftrightarrow (M \in ℤ \land N \in ℤ \land M < N)$

Proof

Step	Hyp	Ref	Expression
1		elfzo2	$⊢ M \in (M ..^N) \leftrightarrow (M \in ℤ_{\geq M} \land N \in ℤ \land M < N)$
2		eluzel2	$⊢ M \in ℤ_{\geq M} \to M \in ℤ$
3		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
4	2 3	impbii	$⊢ M \in ℤ_{\geq M} \leftrightarrow M \in ℤ$
5	4	3anbi1i	$⊢ (M \in ℤ_{\geq M} \land N \in ℤ \land M < N) \leftrightarrow (M \in ℤ \land N \in ℤ \land M < N)$
6	1 5	bitri	$⊢ M \in (M ..^N) \leftrightarrow (M \in ℤ \land N \in ℤ \land M < N)$

Metamath Proof Explorer

Theorem fzolb

Proof