This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ M ∨ M ∈ ℤ ≥ N

Proof

Step Hyp Ref Expression
1 zre ⊢ M ∈ ℤ → M ∈ ℝ
2 zre ⊢ N ∈ ℤ → N ∈ ℝ
3 letric ⊢ M ∈ ℝ ∧ N ∈ ℝ → M ≤ N ∨ N ≤ M
4 1 2 3 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ∨ N ≤ M
5 eluz ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ M ↔ M ≤ N
6 eluz ⊢ N ∈ ℤ ∧ M ∈ ℤ → M ∈ ℤ ≥ N ↔ N ≤ M
7 6 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∈ ℤ ≥ N ↔ N ≤ M
8 5 7 orbi12d ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ M ∨ M ∈ ℤ ≥ N ↔ M ≤ N ∨ N ≤ M
9 4 8 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ M ∨ M ∈ ℤ ≥ N