fzdisj

Description: Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010)

		Ref	Expression
	Assertion	fzdisj	$⊢ K < M \to (J \dots K) \cap (M \dots N) = \emptyset$

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in ((J \dots K) \cap (M \dots N)) \leftrightarrow (x \in (J \dots K) \land x \in (M \dots N))$
2		elfzel1	$⊢ x \in (M \dots N) \to M \in ℤ$
3	2	adantl	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to M \in ℤ$
4	3	zred	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to M \in ℝ$
5		elfzel2	$⊢ x \in (J \dots K) \to K \in ℤ$
6	5	adantr	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to K \in ℤ$
7	6	zred	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to K \in ℝ$
8		elfzelz	$⊢ x \in (M \dots N) \to x \in ℤ$
9	8	zred	$⊢ x \in (M \dots N) \to x \in ℝ$
10	9	adantl	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to x \in ℝ$
11		elfzle1	$⊢ x \in (M \dots N) \to M \leq x$
12	11	adantl	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to M \leq x$
13		elfzle2	$⊢ x \in (J \dots K) \to x \leq K$
14	13	adantr	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to x \leq K$
15	4 10 7 12 14	letrd	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to M \leq K$
16	4 7 15	lensymd	$⊢ (x \in (J \dots K) \land x \in (M \dots N)) \to \neg K < M$
17	1 16	sylbi	$⊢ x \in ((J \dots K) \cap (M \dots N)) \to \neg K < M$
18	17	con2i	$⊢ K < M \to \neg x \in ((J \dots K) \cap (M \dots N))$
19	18	eq0rdv	$⊢ K < M \to (J \dots K) \cap (M \dots N) = \emptyset$

Metamath Proof Explorer