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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ_≥ ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3		letric	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ∨ 𝑁 ≤ 𝑀 ) )
4	1 2 3	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ∨ 𝑁 ≤ 𝑀 ) )
5		eluz	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
6		eluz	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ∈ ( ℤ_≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑀 ) )
7	6	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( ℤ_≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑀 ) )
8	5 7	orbi12d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ_≥ ‘ 𝑁 ) ) ↔ ( 𝑀 ≤ 𝑁 ∨ 𝑁 ≤ 𝑀 ) ) )
9	4 8	mpbird	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ_≥ ‘ 𝑁 ) ) )