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 ) )