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 ⊢ J ∈ ℤ ∧ K ∈ ℤ ∧ L ∈ ℤ → J ≤ K ∧ K ≤ L → J ≤ L

Proof

Step Hyp Ref Expression
1 zre ⊢ J ∈ ℤ → J ∈ ℝ
2 zre ⊢ K ∈ ℤ → K ∈ ℝ
3 zre ⊢ L ∈ ℤ → L ∈ ℝ
4 letr ⊢ J ∈ ℝ ∧ K ∈ ℝ ∧ L ∈ ℝ → J ≤ K ∧ K ≤ L → J ≤ L
5 1 2 3 4 syl3an ⊢ J ∈ ℤ ∧ K ∈ ℤ ∧ L ∈ ℤ → J ≤ K ∧ K ≤ L → J ≤ L