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 {\mathbb{Z}}_{\ge M}\to \left(N=M\vee N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		uzm1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N=M\vee N-1\in {\mathbb{Z}}_{\ge M}\right)$$
2		eluzp1p1	$$⊢N-1\in {\mathbb{Z}}_{\ge M}\to N-1+1\in {\mathbb{Z}}_{\ge \left(M+1\right)}$$
3		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\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 {\mathbb{Z}}_{\ge M}\to N-1+1=N$$
7	6	eleq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N-1+1\in {\mathbb{Z}}_{\ge \left(M+1\right)}\leftrightarrow N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)$$
8	2 7	imbitrid	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N-1\in {\mathbb{Z}}_{\ge M}\to N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)$$
9	8	orim2d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(N=M\vee N-1\in {\mathbb{Z}}_{\ge M}\right)\to \left(N=M\vee N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\right)$$
10	1 9	mpd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N=M\vee N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)$$