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

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 ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐽 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → 𝐽 ≤ 𝐿 ) )