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

Metamath Proof Explorer

Theorem rpmulgcd

Description: If K and M are relatively prime, then the GCD of K and M x. N is the GCD of K and N . (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rpmulgcd ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd 𝑁 ) )

Proof

Step Hyp Ref Expression
1 gcdmultiple ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 gcd ( 𝐾 · 𝑁 ) ) = 𝐾 )
2 1 3adant2 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 gcd ( 𝐾 · 𝑁 ) ) = 𝐾 )
3 2 oveq1d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 gcd ( 𝐾 · 𝑁 ) ) gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) )
4 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
5 4 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℤ )
6 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
7 zmulcl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
8 4 6 7 syl2an ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
9 8 3adant2 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
10 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
11 zmulcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
12 10 6 11 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
13 12 3adant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
14 gcdass ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( 𝐾 gcd ( 𝐾 · 𝑁 ) ) gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) ) )
15 5 9 13 14 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 gcd ( 𝐾 · 𝑁 ) ) gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) ) )
16 3 15 eqtr3d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) ) )
17 16 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) ) )
18 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
19 mulgcdr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) )
20 4 10 18 19 syl3an ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) )
21 oveq1 ⊢ ( ( 𝐾 gcd 𝑀 ) = 1 → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) = ( 1 · 𝑁 ) )
22 20 21 sylan9eq ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) = ( 1 · 𝑁 ) )
23 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
24 23 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
25 24 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → 𝑁 ∈ ℂ )
26 25 mullidd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 1 · 𝑁 ) = 𝑁 )
27 22 26 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) = 𝑁 )
28 27 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 gcd ( ( 𝐾 · 𝑁 ) gcd ( 𝑀 · 𝑁 ) ) ) = ( 𝐾 gcd 𝑁 ) )
29 17 28 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( 𝐾 gcd 𝑁 ) )