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

Metamath Proof Explorer

Theorem mulgcddvds

Description: One half of rpmulgcd2 , which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion mulgcddvds ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
2 simp2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
3 simp3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
4 2 3 zmulcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
5 1 4 gcdcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℕ0 )
6 5 nn0zd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ )
7 dvds0 ⊢ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 0 )
8 6 7 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 0 )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) = 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 0 )
10 oveq2 ⊢ ( ( 𝐾 gcd 𝑁 ) = 0 → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) = ( ( 𝐾 gcd 𝑀 ) · 0 ) )
11 1 2 gcdcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑀 ) ∈ ℕ0 )
12 11 nn0cnd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑀 ) ∈ ℂ )
13 12 mul01d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) · 0 ) = 0 )
14 10 13 sylan9eqr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) = 0 ) → ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) = 0 )
15 9 14 breqtrrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) = 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
16 6 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ )
17 16 zcnd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℂ )
18 1 3 gcdcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∈ ℕ0 )
19 18 nn0zd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∈ ℤ )
20 19 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd 𝑁 ) ∈ ℤ )
21 20 zcnd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd 𝑁 ) ∈ ℂ )
22 simpr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd 𝑁 ) ≠ 0 )
23 17 21 22 divcan1d ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) = ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) )
24 gcddvds ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 𝐾 ∧ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
25 1 4 24 syl2anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 𝐾 ∧ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
26 25 simpld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 𝐾 )
27 6 1 19 26 dvdsmultr1d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝐾 · ( 𝐾 gcd 𝑁 ) ) )
28 27 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝐾 · ( 𝐾 gcd 𝑁 ) ) )
29 23 28 eqbrtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 · ( 𝐾 gcd 𝑁 ) ) )
30 gcddvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ) )
31 1 3 30 syl2anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ 𝑁 ) )
32 31 simpld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∥ 𝐾 )
33 31 simprd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∥ 𝑁 )
34 dvdsmultr2 ⊢ ( ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 → ( 𝐾 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
35 19 2 3 34 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ 𝑁 → ( 𝐾 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
36 33 35 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) )
37 dvdsgcd ⊢ ( ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝐾 gcd 𝑁 ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) )
38 19 1 4 37 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑁 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝐾 gcd 𝑁 ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ) )
39 32 36 38 mp2and ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) )
40 39 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd 𝑁 ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) )
41 dvdsval2 ⊢ ( ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ∧ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ↔ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ) )
42 20 22 16 41 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( 𝐾 gcd 𝑁 ) ∥ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ↔ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ) )
43 40 42 mpbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ )
44 1 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → 𝐾 ∈ ℤ )
45 dvdsmulcr ⊢ ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) ) → ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 · ( 𝐾 gcd 𝑁 ) ) ↔ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ) )
46 43 44 20 22 45 syl112anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 · ( 𝐾 gcd 𝑁 ) ) ↔ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ) )
47 29 46 mpbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 )
48 nn0abscl ⊢ ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) ∈ ℕ0 )
49 2 48 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ 𝑀 ) ∈ ℕ0 )
50 49 nn0zd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ 𝑀 ) ∈ ℤ )
51 dvdsmultr2 ⊢ ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ ∧ ( abs ‘ 𝑀 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 𝐾 → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝐾 ) ) )
52 6 50 1 51 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ 𝐾 → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝐾 ) ) )
53 26 52 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝐾 ) )
54 50 3 zmulcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · 𝑁 ) ∈ ℤ )
55 25 simprd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · 𝑁 ) )
56 iddvds ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∥ 𝑀 )
57 2 56 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ 𝑀 )
58 dvdsabsb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ∥ 𝑀 ↔ 𝑀 ∥ ( abs ‘ 𝑀 ) ) )
59 2 2 58 syl2anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑀 ↔ 𝑀 ∥ ( abs ‘ 𝑀 ) ) )
60 57 59 mpbid ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( abs ‘ 𝑀 ) )
61 dvdsmulc ⊢ ( ( 𝑀 ∈ ℤ ∧ ( abs ‘ 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( abs ‘ 𝑀 ) → ( 𝑀 · 𝑁 ) ∥ ( ( abs ‘ 𝑀 ) · 𝑁 ) ) )
62 2 50 3 61 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( abs ‘ 𝑀 ) → ( 𝑀 · 𝑁 ) ∥ ( ( abs ‘ 𝑀 ) · 𝑁 ) ) )
63 60 62 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∥ ( ( abs ‘ 𝑀 ) · 𝑁 ) )
64 6 4 54 55 63 dvdstrd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝑁 ) )
65 50 1 zmulcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · 𝐾 ) ∈ ℤ )
66 dvdsgcd ⊢ ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ ∧ ( ( abs ‘ 𝑀 ) · 𝐾 ) ∈ ℤ ∧ ( ( abs ‘ 𝑀 ) · 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝐾 ) ∧ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝑁 ) ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( ( abs ‘ 𝑀 ) · 𝐾 ) gcd ( ( abs ‘ 𝑀 ) · 𝑁 ) ) ) )
67 6 65 54 66 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝐾 ) ∧ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( abs ‘ 𝑀 ) · 𝑁 ) ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( ( abs ‘ 𝑀 ) · 𝐾 ) gcd ( ( abs ‘ 𝑀 ) · 𝑁 ) ) ) )
68 53 64 67 mp2and ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( ( abs ‘ 𝑀 ) · 𝐾 ) gcd ( ( abs ‘ 𝑀 ) · 𝑁 ) ) )
69 18 nn0red ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∈ ℝ )
70 18 nn0ge0d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 0 ≤ ( 𝐾 gcd 𝑁 ) )
71 69 70 absidd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐾 gcd 𝑁 ) ) = ( 𝐾 gcd 𝑁 ) )
72 71 oveq2d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · ( abs ‘ ( 𝐾 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
73 2 zcnd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℂ )
74 18 nn0cnd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑁 ) ∈ ℂ )
75 73 74 absmuld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝑀 ) · ( abs ‘ ( 𝐾 gcd 𝑁 ) ) ) )
76 mulgcd ⊢ ( ( ( abs ‘ 𝑀 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) · 𝐾 ) gcd ( ( abs ‘ 𝑀 ) · 𝑁 ) ) = ( ( abs ‘ 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
77 49 1 3 76 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) · 𝐾 ) gcd ( ( abs ‘ 𝑀 ) · 𝑁 ) ) = ( ( abs ‘ 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
78 72 75 77 3eqtr4d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ) = ( ( ( abs ‘ 𝑀 ) · 𝐾 ) gcd ( ( abs ‘ 𝑀 ) · 𝑁 ) ) )
79 68 78 breqtrrd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( abs ‘ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ) )
80 2 19 zmulcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ )
81 dvdsabsb ⊢ ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∈ ℤ ∧ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ↔ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( abs ‘ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ) ) )
82 6 80 81 syl2anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ↔ ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( abs ‘ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ) ) )
83 79 82 mpbird ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) )
84 83 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) )
85 23 84 eqbrtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) )
86 2 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → 𝑀 ∈ ℤ )
87 dvdsmulcr ⊢ ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐾 gcd 𝑁 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) ) → ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ↔ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ) )
88 43 86 20 22 87 syl112anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝑀 · ( 𝐾 gcd 𝑁 ) ) ↔ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ) )
89 85 88 mpbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 )
90 dvdsgcd ⊢ ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ∧ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ) )
91 43 44 86 90 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝐾 ∧ ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ 𝑀 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) ) )
92 47 89 91 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) )
93 11 nn0zd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑀 ) ∈ ℤ )
94 93 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd 𝑀 ) ∈ ℤ )
95 dvdsmulc ⊢ ( ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ ( 𝐾 gcd 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ) )
96 43 94 20 95 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) ∥ ( 𝐾 gcd 𝑀 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) ) )
97 92 96 mpd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( ( ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) / ( 𝐾 gcd 𝑁 ) ) · ( 𝐾 gcd 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
98 23 97 eqbrtrrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑁 ) ≠ 0 ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )
99 15 98 pm2.61dane ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd ( 𝑀 · 𝑁 ) ) ∥ ( ( 𝐾 gcd 𝑀 ) · ( 𝐾 gcd 𝑁 ) ) )