# Metamath Proof Explorer

## Theorem fzp1elp1

Description: Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fzp1elp1 ${⊢}{K}\in \left({M}\dots {N}\right)\to {K}+1\in \left({M}\dots {N}+1\right)$

### Proof

Step Hyp Ref Expression
1 elfzuz ${⊢}{K}\in \left({M}\dots {N}\right)\to {K}\in {ℤ}_{\ge {M}}$
2 peano2uz ${⊢}{K}\in {ℤ}_{\ge {M}}\to {K}+1\in {ℤ}_{\ge {M}}$
3 1 2 syl ${⊢}{K}\in \left({M}\dots {N}\right)\to {K}+1\in {ℤ}_{\ge {M}}$
4 elfzuz3 ${⊢}{K}\in \left({M}\dots {N}\right)\to {N}\in {ℤ}_{\ge {K}}$
5 eluzp1p1 ${⊢}{N}\in {ℤ}_{\ge {K}}\to {N}+1\in {ℤ}_{\ge \left({K}+1\right)}$
6 4 5 syl ${⊢}{K}\in \left({M}\dots {N}\right)\to {N}+1\in {ℤ}_{\ge \left({K}+1\right)}$
7 elfzuzb ${⊢}{K}+1\in \left({M}\dots {N}+1\right)↔\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}+1\in {ℤ}_{\ge \left({K}+1\right)}\right)$
8 3 6 7 sylanbrc ${⊢}{K}\in \left({M}\dots {N}\right)\to {K}+1\in \left({M}\dots {N}+1\right)$