Metamath Proof Explorer

Theorem prinfzo0

Description: The intersection of a half-open integer range and the pair of its outer left borders is empty. (Contributed by AV, 9-Jan-2021)

Ref Expression
Assertion prinfzo0 ⊢ M ∈ ℤ → M N ∩ M + 1 ..^ N = ∅

Proof

Step Hyp Ref Expression
1 elfz3 ⊢ M ∈ ℤ → M ∈ M … M
2 fznuz ⊢ M ∈ M … M → ¬ M ∈ ℤ ≥ M + 1
3 1 2 syl ⊢ M ∈ ℤ → ¬ M ∈ ℤ ≥ M + 1
4 3 3mix1d ⊢ M ∈ ℤ → ¬ M ∈ ℤ ≥ M + 1 ∨ ¬ N ∈ ℤ ∨ ¬ M < N
5 3ianor ⊢ ¬ M ∈ ℤ ≥ M + 1 ∧ N ∈ ℤ ∧ M < N ↔ ¬ M ∈ ℤ ≥ M + 1 ∨ ¬ N ∈ ℤ ∨ ¬ M < N
6 elfzo2 ⊢ M ∈ M + 1 ..^ N ↔ M ∈ ℤ ≥ M + 1 ∧ N ∈ ℤ ∧ M < N
7 5 6 xchnxbir ⊢ ¬ M ∈ M + 1 ..^ N ↔ ¬ M ∈ ℤ ≥ M + 1 ∨ ¬ N ∈ ℤ ∨ ¬ M < N
8 4 7 sylibr ⊢ M ∈ ℤ → ¬ M ∈ M + 1 ..^ N
9 incom ⊢ M ∩ M + 1 ..^ N = M + 1 ..^ N ∩ M
10 9 eqeq1i ⊢ M ∩ M + 1 ..^ N = ∅ ↔ M + 1 ..^ N ∩ M = ∅
11 disjsn ⊢ M + 1 ..^ N ∩ M = ∅ ↔ ¬ M ∈ M + 1 ..^ N
12 10 11 bitri ⊢ M ∩ M + 1 ..^ N = ∅ ↔ ¬ M ∈ M + 1 ..^ N
13 8 12 sylibr ⊢ M ∈ ℤ → M ∩ M + 1 ..^ N = ∅
14 fzonel ⊢ ¬ N ∈ M + 1 ..^ N
15 14 a1i ⊢ M ∈ ℤ → ¬ N ∈ M + 1 ..^ N
16 incom ⊢ N ∩ M + 1 ..^ N = M + 1 ..^ N ∩ N
17 16 eqeq1i ⊢ N ∩ M + 1 ..^ N = ∅ ↔ M + 1 ..^ N ∩ N = ∅
18 disjsn ⊢ M + 1 ..^ N ∩ N = ∅ ↔ ¬ N ∈ M + 1 ..^ N
19 17 18 bitri ⊢ N ∩ M + 1 ..^ N = ∅ ↔ ¬ N ∈ M + 1 ..^ N
20 15 19 sylibr ⊢ M ∈ ℤ → N ∩ M + 1 ..^ N = ∅
21 df-pr ⊢ M N = M ∪ N
22 21 ineq1i ⊢ M N ∩ M + 1 ..^ N = M ∪ N ∩ M + 1 ..^ N
23 22 eqeq1i ⊢ M N ∩ M + 1 ..^ N = ∅ ↔ M ∪ N ∩ M + 1 ..^ N = ∅
24 undisj1 ⊢ M ∩ M + 1 ..^ N = ∅ ∧ N ∩ M + 1 ..^ N = ∅ ↔ M ∪ N ∩ M + 1 ..^ N = ∅
25 23 24 bitr4i ⊢ M N ∩ M + 1 ..^ N = ∅ ↔ M ∩ M + 1 ..^ N = ∅ ∧ N ∩ M + 1 ..^ N = ∅
26 13 20 25 sylanbrc ⊢ M ∈ ℤ → M N ∩ M + 1 ..^ N = ∅