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

Metamath Proof Explorer

Theorem fzodisj

Description: Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fzodisj ( ( 𝐴 ..^ 𝐵 ) ∩ ( 𝐵 ..^ 𝐶 ) ) = ∅

Proof

Step Hyp Ref Expression
1 disj1 ⊢ ( ( ( 𝐴 ..^ 𝐵 ) ∩ ( 𝐵 ..^ 𝐶 ) ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) ) )
2 elfzolt2 ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 < 𝐵 )
3 elfzoelz ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ∈ ℤ )
4 3 zred ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ∈ ℝ )
5 elfzoel2 ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℤ )
6 5 zred ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℝ )
7 4 6 ltnled ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝑥 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑥 ) )
8 2 7 mpbid ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝐵 ≤ 𝑥 )
9 elfzole1 ⊢ ( 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 ≤ 𝑥 )
10 8 9 nsyl ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) )
11 1 10 mpgbir ⊢ ( ( 𝐴 ..^ 𝐵 ) ∩ ( 𝐵 ..^ 𝐶 ) ) = ∅