Theorem fzouzdisj

Description: A half-open integer range does not overlap the upper integer range starting at the endpoint of the first range. (Contributed by Mario Carneiro, 21-Sep-2016)

	Ref	Expression
Assertion	fzouzdisj	⊢ ( ( 𝐴 ..^ 𝐵 ) ∩ ( ℤ≥ ‘ 𝐵 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 < 𝐵 )
2	1	adantr	⊢ ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝑥 < 𝐵 )
3		eluzel2	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) → 𝐵 ∈ ℤ )
4	3	adantl	⊢ ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝐵 ∈ ℤ )
5	4	zred	⊢ ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝐵 ∈ ℝ )
6		eluzelre	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) → 𝑥 ∈ ℝ )
7	6	adantl	⊢ ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝑥 ∈ ℝ )
8		eluzle	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) → 𝐵 ≤ 𝑥 )
9	8	adantl	⊢ ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝐵 ≤ 𝑥 )
10	5 7 9	lensymd	⊢ ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) → ¬ 𝑥 < 𝐵 )
11	2 10	pm2.65i	⊢ ¬ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) )
12		elin	⊢ ( 𝑥 ∈ ( ( 𝐴 ..^ 𝐵 ) ∩ ( ℤ≥ ‘ 𝐵 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
13	11 12	mtbir	⊢ ¬ 𝑥 ∈ ( ( 𝐴 ..^ 𝐵 ) ∩ ( ℤ≥ ‘ 𝐵 ) )
14	13	nel0	⊢ ( ( 𝐴 ..^ 𝐵 ) ∩ ( ℤ≥ ‘ 𝐵 ) ) = ∅