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 e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzm1	|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
2		eluzp1p1	|- ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
3		eluzelcn	|- ( N e. ( ZZ>= ` M ) -> N e. CC )
4		ax-1cn	|- 1 e. CC
5		npcan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
6	3 4 5	sylancl	|- ( N e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) = N )
7	6	eleq1d	|- ( N e. ( ZZ>= ` M ) -> ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
8	2 7	syl5ib	|- ( N e. ( ZZ>= ` M ) -> ( ( N - 1 ) e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` ( M + 1 ) ) ) )
9	8	orim2d	|- ( N e. ( ZZ>= ` M ) -> ( ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) ) )
10	1 9	mpd	|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )