This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 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 ) ) ) )