Metamath Proof Explorer


Theorem dvdstrd

Description: The divides relation is transitive, a deduction version of dvdstr . (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses dvdstrd.1
|- ( ph -> K e. ZZ )
dvdstrd.2
|- ( ph -> M e. ZZ )
dvdstrd.3
|- ( ph -> N e. ZZ )
dvdstrd.4
|- ( ph -> K || M )
dvdstrd.5
|- ( ph -> M || N )
Assertion dvdstrd
|- ( ph -> K || N )

Proof

Step Hyp Ref Expression
1 dvdstrd.1
 |-  ( ph -> K e. ZZ )
2 dvdstrd.2
 |-  ( ph -> M e. ZZ )
3 dvdstrd.3
 |-  ( ph -> N e. ZZ )
4 dvdstrd.4
 |-  ( ph -> K || M )
5 dvdstrd.5
 |-  ( ph -> M || N )
6 dvdstr
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ M || N ) -> K || N ) )
7 1 2 3 6 syl3anc
 |-  ( ph -> ( ( K || M /\ M || N ) -> K || N ) )
8 4 5 7 mp2and
 |-  ( ph -> K || N )