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