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	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑀 ) = 1 ∧ ( 𝐾 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		mulgcddvds	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
2		oveq12	⊢ ( ( ( 𝐾 gcd 𝑀 ) = 1 ∧ ( 𝐾 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) = ( 1 · 1 ) )
3		1t1e1	⊢ ( 1 · 1 ) = 1
4	2 3	eqtrdi	⊢ ( ( ( 𝐾 gcd 𝑀 ) = 1 ∧ ( 𝐾 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) = 1 )
5	4	breq2d	⊢ ( ( ( 𝐾 gcd 𝑀 ) = 1 ∧ ( 𝐾 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ↔ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 1 ) )
6	1 5	syl5ibcom	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑀 ) = 1 ∧ ( 𝐾 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 1 ) )
7		simp1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
8		zmulcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
9	8	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
10	7 9	gcdcld	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℕ0 )
11		dvds1	⊢ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℕ0 → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 1 ↔ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
12	10 11	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 1 ↔ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
13	6 12	sylibd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑀 ) = 1 ∧ ( 𝐾 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = 1 ) )