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