Theorem fzdisj

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

	Ref	Expression
Assertion	fzdisj	⊢ ( 𝐾 < 𝑀 → ( ( 𝐽 ... 𝐾 ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( ( 𝐽 ... 𝐾 ) ∩ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) )
2		elfzel1	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
3	2	adantl	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
4	3	zred	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
5		elfzel2	⊢ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) → 𝐾 ∈ ℤ )
6	5	adantr	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
7	6	zred	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
8		elfzelz	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
9	8	zred	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ )
10	9	adantl	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ ℝ )
11		elfzle1	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝑥 )
12	11	adantl	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝑥 )
13		elfzle2	⊢ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) → 𝑥 ≤ 𝐾 )
14	13	adantr	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ≤ 𝐾 )
15	4 10 7 12 14	letrd	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝐾 )
16	4 7 15	lensymd	⊢ ( ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ¬ 𝐾 < 𝑀 )
17	1 16	sylbi	⊢ ( 𝑥 ∈ ( ( 𝐽 ... 𝐾 ) ∩ ( 𝑀 ... 𝑁 ) ) → ¬ 𝐾 < 𝑀 )
18	17	con2i	⊢ ( 𝐾 < 𝑀 → ¬ 𝑥 ∈ ( ( 𝐽 ... 𝐾 ) ∩ ( 𝑀 ... 𝑁 ) ) )
19	18	eq0rdv	⊢ ( 𝐾 < 𝑀 → ( ( 𝐽 ... 𝐾 ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )