# Metamath Proof Explorer

## Theorem fzpred

Description: Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

Ref Expression
Assertion fzpred ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)=\left\{{M}\right\}\cup \left({M}+1\dots {N}\right)$

### Proof

Step Hyp Ref Expression
1 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
2 uzid ${⊢}{M}\in ℤ\to {M}\in {ℤ}_{\ge {M}}$
3 peano2uz ${⊢}{M}\in {ℤ}_{\ge {M}}\to {M}+1\in {ℤ}_{\ge {M}}$
4 1 2 3 3syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}+1\in {ℤ}_{\ge {M}}$
5 fzsplit2 ${⊢}\left({M}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {M}}\right)\to \left({M}\dots {N}\right)=\left({M}\dots {M}\right)\cup \left({M}+1\dots {N}\right)$
6 4 5 mpancom ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)=\left({M}\dots {M}\right)\cup \left({M}+1\dots {N}\right)$
7 fzsn ${⊢}{M}\in ℤ\to \left({M}\dots {M}\right)=\left\{{M}\right\}$
8 1 7 syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {M}\right)=\left\{{M}\right\}$
9 8 uneq1d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {M}\right)\cup \left({M}+1\dots {N}\right)=\left\{{M}\right\}\cup \left({M}+1\dots {N}\right)$
10 6 9 eqtrd ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)=\left\{{M}\right\}\cup \left({M}+1\dots {N}\right)$