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

Metamath Proof Explorer

Theorem rpmul

Description: If K is relatively prime to M and to N , it is also relatively prime to their product. (Contributed by Mario Carneiro, 24-Feb-2014) (Proof shortened by Mario Carneiro, 2-Jul-2015)

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

Proof

Step Hyp Ref Expression
1 mulgcddvds 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )
2 oveq12 
 |-  ( ( ( K gcd M ) = 1 /\ ( K gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) = ( 1 x. 1 ) )
3 1t1e1 
 |-  ( 1 x. 1 ) = 1
4 2 3 eqtrdi 
 |-  ( ( ( K gcd M ) = 1 /\ ( K gcd N ) = 1 ) -> ( ( K gcd M ) x. ( K gcd N ) ) = 1 )
5 4 breq2d 
 |-  ( ( ( K gcd M ) = 1 /\ ( K gcd N ) = 1 ) -> ( ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) <-> ( K gcd ( M x. N ) ) || 1 ) )
6 1 5 syl5ibcom 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K gcd M ) = 1 /\ ( K gcd N ) = 1 ) -> ( K gcd ( M x. N ) ) || 1 ) )
7 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
8 zmulcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
9 8 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
10 7 9 gcdcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) e. NN0 )
11 dvds1 
 |-  ( ( K gcd ( M x. N ) ) e. NN0 -> ( ( K gcd ( M x. N ) ) || 1 <-> ( K gcd ( M x. N ) ) = 1 ) )
12 10 11 syl 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd ( M x. N ) ) || 1 <-> ( K gcd ( M x. N ) ) = 1 ) )
13 6 12 sylibd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K gcd M ) = 1 /\ ( K gcd N ) = 1 ) -> ( K gcd ( M x. N ) ) = 1 ) )