Metamath Proof Explorer

Theorem fzopred

Description: Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 . (Contributed by AV, 14-Jul-2020)

Ref Expression
Assertion fzopred ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → M ..^ N = M ∪ M + 1 ..^ N

Proof

Step Hyp Ref Expression
1 fzolb ⊢ M ∈ M ..^ N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N
2 fzofzp1 ⊢ M ∈ M ..^ N → M + 1 ∈ M … N
3 1 2 sylbir ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → M + 1 ∈ M … N
4 fzosplit ⊢ M + 1 ∈ M … N → M ..^ N = M ..^ M + 1 ∪ M + 1 ..^ N
5 3 4 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → M ..^ N = M ..^ M + 1 ∪ M + 1 ..^ N
6 fzosn ⊢ M ∈ ℤ → M ..^ M + 1 = M
7 6 3ad2ant1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → M ..^ M + 1 = M
8 7 uneq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → M ..^ M + 1 ∪ M + 1 ..^ N = M ∪ M + 1 ..^ N
9 5 8 eqtrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N → M ..^ N = M ∪ M + 1 ..^ N