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 gcddvds ⊢ ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) ) )
20 17 18 19 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) ) )
21 20 simpld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) )
22 12 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑀 ) ∥ 𝑀 )
23 17 18 gcdcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 )
24 23 nn0zd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℤ )
25 dvdstr ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ) )
26 24 17 2 25 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ) )
27 21 22 26 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 )
28 20 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) )
29 15 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd 𝑁 ) ∥ 𝑁 )
30 dvdstr ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 ) )
31 24 18 3 30 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑁 ) ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 ) )
32 28 29 31 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 )
33 dvdsgcd ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 gcd 𝑁 ) ) )
34 24 2 3 33 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 𝑁 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 gcd 𝑁 ) ) )
35 27 32 34 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 gcd 𝑁 ) )
36 simpr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 gcd 𝑁 ) = 1 )
37 35 36 breqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 1 )
38 dvds1 ⊢ ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 1 ↔ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 ) )
39 23 38 syl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) ∥ 1 ↔ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 ) )
40 37 39 mpbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 )
41 coprmdvds2 ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑀 ) gcd ( 𝐾 gcd 𝑁 ) ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ) )
42 17 18 1 40 41 syl31anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ) )
43 13 16 42 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 )
44 dvdscmul ⊢ ( ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ) )
45 18 3 17 44 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ) )
46 dvdsmulc ⊢ ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝑀 → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
47 17 2 3 46 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝑀 → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
48 17 18 zmulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ )
49 17 3 zmulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∈ ℤ )
50 dvdstr ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∧ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
51 48 49 4 50 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∧ ( ( 𝐾 gcd 𝑀 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
52 45 47 51 syl2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
53 29 22 52 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) )
54 dvdsgcd ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) )
55 48 1 4 54 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) )
56 43 53 55 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) )
57 dvdseq ⊢ ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℕ0 ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∈ ℕ0 ) ∧ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∧ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
58 5 8 10 56 57 syl22anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )