peano2uzr

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

		Ref	Expression
	Assertion	peano2uzr	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N \in ℤ_{\geq M}$

Step	Hyp	Ref	Expression
1		eluzelcn	$⊢ N \in ℤ_{\geq (M + 1)} \to N \in ℂ$
2		ax-1cn	$⊢ 1 \in ℂ$
3		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
4	1 2 3	sylancl	$⊢ N \in ℤ_{\geq (M + 1)} \to N - 1 + 1 = N$
5	4	adantl	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 + 1 = N$
6		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
7		peano2uz	$⊢ N - 1 \in ℤ_{\geq M} \to N - 1 + 1 \in ℤ_{\geq M}$
8	6 7	syl	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 + 1 \in ℤ_{\geq M}$
9	5 8	eqeltrrd	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N \in ℤ_{\geq M}$

Metamath Proof Explorer