Theorem peano2uzr

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

	Ref	Expression
Assertion	peano2uzr	|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N e. ( ZZ>= ` M ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelcn	|- ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. CC )
2		ax-1cn	|- 1 e. CC
3		npcan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
4	1 2 3	sylancl	|- ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( ( N - 1 ) + 1 ) = N )
5	4	adantl	|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
6		eluzp1m1	|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
7		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) )
8	6 7	syl	|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) )
9	5 8	eqeltrrd	|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N e. ( ZZ>= ` M ) )