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

Metamath Proof Explorer

Theorem dvdstr

Description: The divides relation is transitive. Theorem 1.1(b) in ApostolNT p. 14 (transitive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdstr 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ M || N ) -> K || N ) )

Proof

Step Hyp Ref Expression
1 3simpa 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ M e. ZZ ) )
2 3simpc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ N e. ZZ ) )
3 3simpb 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ N e. ZZ ) )
4 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
5 4 adantl 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x x. y ) e. ZZ )
6 oveq2 
 |-  ( ( x x. K ) = M -> ( y x. ( x x. K ) ) = ( y x. M ) )
7 6 adantr 
 |-  ( ( ( x x. K ) = M /\ ( y x. M ) = N ) -> ( y x. ( x x. K ) ) = ( y x. M ) )
8 eqeq2 
 |-  ( ( y x. M ) = N -> ( ( y x. ( x x. K ) ) = ( y x. M ) <-> ( y x. ( x x. K ) ) = N ) )
9 8 adantl 
 |-  ( ( ( x x. K ) = M /\ ( y x. M ) = N ) -> ( ( y x. ( x x. K ) ) = ( y x. M ) <-> ( y x. ( x x. K ) ) = N ) )
10 7 9 mpbid 
 |-  ( ( ( x x. K ) = M /\ ( y x. M ) = N ) -> ( y x. ( x x. K ) ) = N )
11 zcn 
 |-  ( x e. ZZ -> x e. CC )
12 zcn 
 |-  ( y e. ZZ -> y e. CC )
13 zcn 
 |-  ( K e. ZZ -> K e. CC )
14 mulass 
 |-  ( ( x e. CC /\ y e. CC /\ K e. CC ) -> ( ( x x. y ) x. K ) = ( x x. ( y x. K ) ) )
15 mul12 
 |-  ( ( x e. CC /\ y e. CC /\ K e. CC ) -> ( x x. ( y x. K ) ) = ( y x. ( x x. K ) ) )
16 14 15 eqtrd 
 |-  ( ( x e. CC /\ y e. CC /\ K e. CC ) -> ( ( x x. y ) x. K ) = ( y x. ( x x. K ) ) )
17 11 12 13 16 syl3an 
 |-  ( ( x e. ZZ /\ y e. ZZ /\ K e. ZZ ) -> ( ( x x. y ) x. K ) = ( y x. ( x x. K ) ) )
18 17 3comr 
 |-  ( ( K e. ZZ /\ x e. ZZ /\ y e. ZZ ) -> ( ( x x. y ) x. K ) = ( y x. ( x x. K ) ) )
19 18 3expb 
 |-  ( ( K e. ZZ /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. y ) x. K ) = ( y x. ( x x. K ) ) )
20 19 3ad2antl1 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. y ) x. K ) = ( y x. ( x x. K ) ) )
21 20 eqeq1d 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. y ) x. K ) = N <-> ( y x. ( x x. K ) ) = N ) )
22 10 21 imbitrrid 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. K ) = M /\ ( y x. M ) = N ) -> ( ( x x. y ) x. K ) = N ) )
23 1 2 3 5 22 dvds2lem 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ M || N ) -> K || N ) )