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	⊢ ( ( 𝐴 ..^ 𝐵 ) ∩ ( 𝐵 ..^ 𝐶 ) ) = ∅