Metamath Proof Explorer

Theorem nelfzo

Description: An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		df-nel	$⊢ K \notin (M ..^N) \leftrightarrow \neg K \in (M ..^N)$
2		ianor	$⊢ \neg (M \leq K \land K < N) \leftrightarrow (\neg M \leq K \lor \neg K < N)$
3	2	a1i	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\neg (M \leq K \land K < N) \leftrightarrow (\neg M \leq K \lor \neg K < N))$
4		elfzo	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M ..^N) \leftrightarrow (M \leq K \land K < N))$
5	4	notbid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\neg K \in (M ..^N) \leftrightarrow \neg (M \leq K \land K < N))$
6		zre	$⊢ K \in ℤ \to K \in ℝ$
7		zre	$⊢ M \in ℤ \to M \in ℝ$
8	6 7	anim12i	$⊢ (K \in ℤ \land M \in ℤ) \to (K \in ℝ \land M \in ℝ)$
9	8	3adant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℝ \land M \in ℝ)$
10		ltnle	$⊢ (K \in ℝ \land M \in ℝ) \to (K < M \leftrightarrow \neg M \leq K)$
11	9 10	syl	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K < M \leftrightarrow \neg M \leq K)$
12		zre	$⊢ N \in ℤ \to N \in ℝ$
13	6 12	anim12ci	$⊢ (K \in ℤ \land N \in ℤ) \to (N \in ℝ \land K \in ℝ)$
14	13	3adant2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (N \in ℝ \land K \in ℝ)$
15		lenlt	$⊢ (N \in ℝ \land K \in ℝ) \to (N \leq K \leftrightarrow \neg K < N)$
16	14 15	syl	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (N \leq K \leftrightarrow \neg K < N)$
17	11 16	orbi12d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K < M \lor N \leq K) \leftrightarrow (\neg M \leq K \lor \neg K < N))$
18	3 5 17	3bitr4d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\neg K \in (M ..^N) \leftrightarrow (K < M \lor N \leq K))$
19	1 18	bitrid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \notin (M ..^N) \leftrightarrow (K < M \lor N \leq K))$