Theorem uztric

Description: Totality of the ordering relation on integers, stated in terms of upper integers. (Contributed by NM, 6-Jul-2005) (Revised by Mario Carneiro, 25-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		zre	|- ( M e. ZZ -> M e. RR )
2		zre	|- ( N e. ZZ -> N e. RR )
3		letric	|- ( ( M e. RR /\ N e. RR ) -> ( M <_ N \/ N <_ M ) )
4	1 2 3	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N \/ N <_ M ) )
5		eluz	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
6		eluz	|- ( ( N e. ZZ /\ M e. ZZ ) -> ( M e. ( ZZ>= ` N ) <-> N <_ M ) )
7	6	ancoms	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( ZZ>= ` N ) <-> N <_ M ) )
8	5 7	orbi12d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) <-> ( M <_ N \/ N <_ M ) ) )
9	4 8	mpbird	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )