Metamath Proof Explorer

Theorem coprmdvdsb

Description: Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion coprmdvdsb 
|- ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( K || N <-> K || ( M x. N ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> K e. ZZ )
2 simp3l 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> M e. ZZ )
3 simp2 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> N e. ZZ )
4 dvdsmultr2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || N -> K || ( M x. N ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( K || N -> K || ( M x. N ) ) )
6 simp3r 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( K gcd M ) = 1 )
7 coprmdvds 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M x. N ) /\ ( K gcd M ) = 1 ) -> K || N ) )
8 1 2 3 7 syl3anc 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( ( K || ( M x. N ) /\ ( K gcd M ) = 1 ) -> K || N ) )
9 6 8 mpan2d 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( K || ( M x. N ) -> K || N ) )
10 5 9 impbid 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( K || N <-> K || ( M x. N ) ) )