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

Metamath Proof Explorer

Theorem fzodif2

Description: Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021)

Ref Expression
Assertion fzodif2 ⊢ N ∈ ℤ ≥ M → M ..^ N + 1 ∖ N = M ..^ N

Proof

Step Hyp Ref Expression
1 fzosplitsn ⊢ N ∈ ℤ ≥ M → M ..^ N + 1 = M ..^ N ∪ N
2 1 difeq1d ⊢ N ∈ ℤ ≥ M → M ..^ N + 1 ∖ N = M ..^ N ∪ N ∖ N
3 difun2 ⊢ M ..^ N ∪ N ∖ N = M ..^ N ∖ N
4 2 3 eqtrdi ⊢ N ∈ ℤ ≥ M → M ..^ N + 1 ∖ N = M ..^ N ∖ N
5 fzonel ⊢ ¬ N ∈ M ..^ N
6 disjsn ⊢ M ..^ N ∩ N = ∅ ↔ ¬ N ∈ M ..^ N
7 5 6 mpbir ⊢ M ..^ N ∩ N = ∅
8 disjdif2 ⊢ M ..^ N ∩ N = ∅ → M ..^ N ∖ N = M ..^ N
9 7 8 mp1i ⊢ N ∈ ℤ ≥ M → M ..^ N ∖ N = M ..^ N
10 4 9 eqtrd ⊢ N ∈ ℤ ≥ M → M ..^ N + 1 ∖ N = M ..^ N