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 \in ℤ \land K \in ℤ \land L \in ℤ) \to ((J \leq K \land K \leq L) \to J \leq L)$

Step	Hyp	Ref	Expression
1		zre	$⊢ J \in ℤ \to J \in ℝ$
2		zre	$⊢ K \in ℤ \to K \in ℝ$
3		zre	$⊢ L \in ℤ \to L \in ℝ$
4		letr	$⊢ (J \in ℝ \land K \in ℝ \land L \in ℝ) \to ((J \leq K \land K \leq L) \to J \leq L)$
5	1 2 3 4	syl3an	$⊢ (J \in ℤ \land K \in ℤ \land L \in ℤ) \to ((J \leq K \land K \leq L) \to J \leq L)$