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

Metamath Proof Explorer

Theorem peano2uzr

Description: Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006)

Ref Expression
Assertion peano2uzr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ℂ )
2 ax-1cn ⊢ 1 ∈ ℂ
3 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
4 1 2 3 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
5 4 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
6 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
7 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
8 6 7 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 5 8 eqeltrrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )