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 e. ZZ /\ K e. ZZ /\ L e. ZZ ) -> ( ( J <_ K /\ K <_ L ) -> J <_ L ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( J e. ZZ -> J e. RR )
2 zre 
 |-  ( K e. ZZ -> K e. RR )
3 zre 
 |-  ( L e. ZZ -> L e. RR )
4 letr 
 |-  ( ( J e. RR /\ K e. RR /\ L e. RR ) -> ( ( J <_ K /\ K <_ L ) -> J <_ L ) )
5 1 2 3 4 syl3an 
 |-  ( ( J e. ZZ /\ K e. ZZ /\ L e. ZZ ) -> ( ( J <_ K /\ K <_ L ) -> J <_ L ) )