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

Metamath Proof Explorer

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