This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐾 < 𝑀 → ( ( 𝐽 ... 𝐾 ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )