Metamath Proof Explorer


Theorem zletr

Description: Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018)

Ref Expression
Assertion zletr ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐽𝐾𝐾𝐿 ) → 𝐽𝐿 ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
2 zre ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
3 zre ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
4 letr ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝐽𝐾𝐾𝐿 ) → 𝐽𝐿 ) )
5 1 2 3 4 syl3an ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐽𝐾𝐾𝐿 ) → 𝐽𝐿 ) )