elfzo

Description: Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	elfzo	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M ..^N) \leftrightarrow (M \leq K \land K < N))$

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
2		elfz	$⊢ (K \in ℤ \land M \in ℤ \land N - 1 \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (M \leq K \land K \leq N - 1))$
3	1 2	syl3an3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (M \leq K \land K \leq N - 1))$
4		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
5	4	eleq2d	$⊢ N \in ℤ \to (K \in (M ..^N) \leftrightarrow K \in (M \dots N - 1))$
6	5	3ad2ant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M ..^N) \leftrightarrow K \in (M \dots N - 1))$
7		zltlem1	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow K \leq N - 1)$
8	7	3adant2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow K \leq N - 1)$
9	8	anbi2d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M \leq K \land K < N) \leftrightarrow (M \leq K \land K \leq N - 1))$
10	3 6 9	3bitr4d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M ..^N) \leftrightarrow (M \leq K \land K < N))$

Metamath Proof Explorer