Metamath Proof Explorer

Theorem fzpreddisj

Description: A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019)

Ref Expression
Assertion fzpreddisj ⊢ N ∈ ℤ ≥ M → M ∩ M + 1 … N = ∅

Proof

Step Hyp Ref Expression
1 incom ⊢ M ∩ M + 1 … N = M + 1 … N ∩ M
2 0lt1 ⊢ 0 < 1
3 0re ⊢ 0 ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 3 4 ltnlei ⊢ 0 < 1 ↔ ¬ 1 ≤ 0
6 2 5 mpbi ⊢ ¬ 1 ≤ 0
7 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
8 7 zred ⊢ N ∈ ℤ ≥ M → M ∈ ℝ
9 leaddle0 ⊢ M ∈ ℝ ∧ 1 ∈ ℝ → M + 1 ≤ M ↔ 1 ≤ 0
10 8 4 9 sylancl ⊢ N ∈ ℤ ≥ M → M + 1 ≤ M ↔ 1 ≤ 0
11 6 10 mtbiri ⊢ N ∈ ℤ ≥ M → ¬ M + 1 ≤ M
12 11 intnanrd ⊢ N ∈ ℤ ≥ M → ¬ M + 1 ≤ M ∧ M ≤ N
13 12 intnand ⊢ N ∈ ℤ ≥ M → ¬ M + 1 ∈ ℤ ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ M + 1 ≤ M ∧ M ≤ N
14 elfz2 ⊢ M ∈ M + 1 … N ↔ M + 1 ∈ ℤ ∧ N ∈ ℤ ∧ M ∈ ℤ ∧ M + 1 ≤ M ∧ M ≤ N
15 13 14 sylnibr ⊢ N ∈ ℤ ≥ M → ¬ M ∈ M + 1 … N
16 disjsn ⊢ M + 1 … N ∩ M = ∅ ↔ ¬ M ∈ M + 1 … N
17 15 16 sylibr ⊢ N ∈ ℤ ≥ M → M + 1 … N ∩ M = ∅
18 1 17 syl5eq ⊢ N ∈ ℤ ≥ M → M ∩ M + 1 … N = ∅