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

Metamath Proof Explorer

Theorem rpmulgcd2

Description: If M is relatively prime to N , then the GCD of K with M x. N is the product of the GCDs with M and N respectively. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion rpmulgcd2 ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝐾 ∈ ℤ )
2 simpl2 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀 ∈ ℤ )
3 simpl3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℤ )
4 2 3 zmulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
5 1 4 gcdcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℕ0 )
6 1 2 gcdcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑀 ) ∈ ℕ0 )
7 1 3 gcdcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑁 ) ∈ ℕ0 )
8 6 7 nn0mulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 )
9 mulgcddvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
10 9 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
11 gcddvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) )
12 1 2 11 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) )
13 12 simpld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑀 ) ∥ 𝐾 )
14 gcddvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ) )
15 1 3 14 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ) )
16 15 simpld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑁 ) ∥ 𝐾 )
17 6 nn0zd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑀 ) ∈ ℤ )
18 7 nn0zd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑁 ) ∈ ℤ )
19 17 18 gcdcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 )
20 19 nn0zd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℤ )
21 gcddvds ⊢ ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) ) )
22 17 18 21 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) ) )
23 22 simpld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) )
24 12 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑀 ) ∥ 𝑀 )
25 20 17 2 23 24 dvdstrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 )
26 22 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) )
27 15 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑁 ) ∥ 𝑁 )
28 20 18 3 26 27 dvdstrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 )
29 dvdsgcd ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 gcd 𝑁 ) ) )
30 20 2 3 29 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 gcd 𝑁 ) ) )
31 25 28 30 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 gcd 𝑁 ) )
32 simpr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 gcd 𝑁 ) = 1 )
33 31 32 breqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 1 )
34 dvds1 ⊢ ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 1 ↔ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 ) )
35 19 34 syl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 1 ↔ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 ) )
36 33 35 mpbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 )
37 coprmdvds2 ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ) )
38 17 18 1 36 37 syl31anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ) )
39 13 16 38 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 )
40 dvdscmul ⊢ ( ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ) )
41 18 3 17 40 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ) )
42 dvdsmulc ⊢ ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝑀 → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
43 17 2 3 42 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝑀 → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
44 17 18 zmulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ )
45 17 3 zmulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∈ ℤ )
46 dvdstr ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∧ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
47 44 45 4 46 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∧ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
48 41 43 47 syl2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
49 27 24 48 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) )
50 dvdsgcd ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) )
51 44 1 4 50 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) )
52 39 49 51 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) )
53 dvdseq ⊢ ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℕ0 ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 ) ∧ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
54 5 8 10 52 53 syl22anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )