# Metamath Proof Explorer

## 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 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge {M}}\vee {M}\in {ℤ}_{\ge {N}}\right)$

### Proof

Step Hyp Ref Expression
1 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
2 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
3 letric ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left({M}\le {N}\vee {N}\le {M}\right)$
4 1 2 3 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\le {N}\vee {N}\le {M}\right)$
5 eluz ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge {M}}↔{M}\le {N}\right)$
6 eluz ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to \left({M}\in {ℤ}_{\ge {N}}↔{N}\le {M}\right)$
7 6 ancoms ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\in {ℤ}_{\ge {N}}↔{N}\le {M}\right)$
8 5 7 orbi12d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({N}\in {ℤ}_{\ge {M}}\vee {M}\in {ℤ}_{\ge {N}}\right)↔\left({M}\le {N}\vee {N}\le {M}\right)\right)$
9 4 8 mpbird ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge {M}}\vee {M}\in {ℤ}_{\ge {N}}\right)$