# Metamath Proof Explorer

## Theorem uzm1

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

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

### Proof

Step Hyp Ref Expression
1 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
2 1 a1d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(¬{N}={M}\to {M}\in ℤ\right)$
3 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
4 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
5 3 4 syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}-1\in ℤ$
6 5 a1d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(¬{N}={M}\to {N}-1\in ℤ\right)$
7 df-ne ${⊢}{N}\ne {M}↔¬{N}={M}$
8 eluzle ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\le {N}$
9 1 zred ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℝ$
10 eluzelre ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℝ$
11 9 10 ltlend ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}<{N}↔\left({M}\le {N}\wedge {N}\ne {M}\right)\right)$
12 11 biimprd ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(\left({M}\le {N}\wedge {N}\ne {M}\right)\to {M}<{N}\right)$
13 8 12 mpand ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}\ne {M}\to {M}<{N}\right)$
14 7 13 syl5bir ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(¬{N}={M}\to {M}<{N}\right)$
15 zltlem1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{M}\le {N}-1\right)$
16 1 3 15 syl2anc ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}<{N}↔{M}\le {N}-1\right)$
17 14 16 sylibd ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(¬{N}={M}\to {M}\le {N}-1\right)$
18 2 6 17 3jcad ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(¬{N}={M}\to \left({M}\in ℤ\wedge {N}-1\in ℤ\wedge {M}\le {N}-1\right)\right)$
19 eluz2 ${⊢}{N}-1\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}-1\in ℤ\wedge {M}\le {N}-1\right)$
20 18 19 syl6ibr ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(¬{N}={M}\to {N}-1\in {ℤ}_{\ge {M}}\right)$
21 20 orrd ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}={M}\vee {N}-1\in {ℤ}_{\ge {M}}\right)$