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 
|- ( ( 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 ) )