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 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 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 ) )