# Metamath Proof Explorer

## Theorem uzp1

Description: Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009)

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

### Proof

Step Hyp Ref Expression
1 uzm1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}={M}\vee {N}-1\in {ℤ}_{\ge {M}}\right)$
2 eluzp1p1 ${⊢}{N}-1\in {ℤ}_{\ge {M}}\to {N}-1+1\in {ℤ}_{\ge \left({M}+1\right)}$
3 eluzelcn ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℂ$
4 ax-1cn ${⊢}1\in ℂ$
5 npcan ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\to {N}-1+1={N}$
6 3 4 5 sylancl ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}-1+1={N}$
7 6 eleq1d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}-1+1\in {ℤ}_{\ge \left({M}+1\right)}↔{N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
8 2 7 syl5ib ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}-1\in {ℤ}_{\ge {M}}\to {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
9 8 orim2d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(\left({N}={M}\vee {N}-1\in {ℤ}_{\ge {M}}\right)\to \left({N}={M}\vee {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\right)$
10 1 9 mpd ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}={M}\vee {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$