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 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N})$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ M \in ℤ \to M \in ℝ$
2		zre	$⊢ N \in ℤ \to N \in ℝ$
3		letric	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \lor N \leq M)$
4	1 2 3	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M \leq N \lor N \leq M)$
5		eluz	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
6		eluz	$⊢ (N \in ℤ \land M \in ℤ) \to (M \in ℤ_{\geq N} \leftrightarrow N \leq M)$
7	6	ancoms	$⊢ (M \in ℤ \land N \in ℤ) \to (M \in ℤ_{\geq N} \leftrightarrow N \leq M)$
8	5 7	orbi12d	$⊢ (M \in ℤ \land N \in ℤ) \to ((N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N}) \leftrightarrow (M \leq N \lor N \leq M))$
9	4 8	mpbird	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N})$