elfzonelfzo

Description: If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018)

		Ref	Expression
	Assertion	elfzonelfzo	$⊢ N \in ℤ \to ((K \in (M ..^R) \land \neg K \in (M ..^N)) \to K \in (N ..^R))$

Proof

Step	Hyp	Ref	Expression
1		elfzo2	$⊢ K \in (M ..^R) \leftrightarrow (K \in ℤ_{\geq M} \land R \in ℤ \land K < R)$
2		simpr	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to N \in ℤ$
3		eluzelz	$⊢ K \in ℤ_{\geq M} \to K \in ℤ$
4	3	3ad2ant1	$⊢ (K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \to K \in ℤ$
5	4	ad2antrr	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to K \in ℤ$
6		eluzelre	$⊢ K \in ℤ_{\geq M} \to K \in ℝ$
7		zre	$⊢ N \in ℤ \to N \in ℝ$
8		ltnle	$⊢ (K \in ℝ \land N \in ℝ) \to (K < N \leftrightarrow \neg N \leq K)$
9	6 7 8	syl2an	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K < N \leftrightarrow \neg N \leq K)$
10		id	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ \land K < N) \to (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$
11	10	3expa	$⊢ ((K \in ℤ_{\geq M} \land N \in ℤ) \land K < N) \to (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$
12		elfzo2	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$
13	11 12	sylibr	$⊢ ((K \in ℤ_{\geq M} \land N \in ℤ) \land K < N) \to K \in (M ..^N)$
14	13	ex	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K < N \to K \in (M ..^N))$
15	9 14	sylbird	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (\neg N \leq K \to K \in (M ..^N))$
16	15	con1d	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (\neg K \in (M ..^N) \to N \leq K)$
17	16	ex	$⊢ K \in ℤ_{\geq M} \to (N \in ℤ \to (\neg K \in (M ..^N) \to N \leq K))$
18	17	com23	$⊢ K \in ℤ_{\geq M} \to (\neg K \in (M ..^N) \to (N \in ℤ \to N \leq K))$
19	18	3ad2ant1	$⊢ (K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \to (\neg K \in (M ..^N) \to (N \in ℤ \to N \leq K))$
20	19	imp31	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to N \leq K$
21		eluz2	$⊢ K \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land K \in ℤ \land N \leq K)$
22	2 5 20 21	syl3anbrc	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to K \in ℤ_{\geq N}$
23		simpll2	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to R \in ℤ$
24		simpll3	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to K < R$
25		elfzo2	$⊢ K \in (N ..^R) \leftrightarrow (K \in ℤ_{\geq N} \land R \in ℤ \land K < R)$
26	22 23 24 25	syl3anbrc	$⊢ (((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \land N \in ℤ) \to K \in (N ..^R)$
27	26	ex	$⊢ ((K \in ℤ_{\geq M} \land R \in ℤ \land K < R) \land \neg K \in (M ..^N)) \to (N \in ℤ \to K \in (N ..^R))$
28	1 27	sylanb	$⊢ (K \in (M ..^R) \land \neg K \in (M ..^N)) \to (N \in ℤ \to K \in (N ..^R))$
29	28	com12	$⊢ N \in ℤ \to ((K \in (M ..^R) \land \neg K \in (M ..^N)) \to K \in (N ..^R))$

Metamath Proof Explorer

Theorem elfzonelfzo

Proof