Theorem uzp1

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

	Ref	Expression
Assertion	uzp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzm1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
2		eluzp1p1	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
3		eluzelcn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℂ )
4		ax-1cn	⊢ 1 ∈ ℂ
5		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
6	3 4 5	sylancl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7	6	eleq1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
8	2 7	imbitrid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
9	8	orim2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
10	1 9	mpd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )