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

Metamath Proof Explorer

Theorem mulgcd

Description: Distribute multiplication by a nonnegative integer over gcd. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Mario Carneiro, 30-May-2014)

Ref Expression
Assertion mulgcd ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
2 simp1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℕ )
3 2 nnzd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
4 simp2 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
5 3 4 zmulcld ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
6 simp3 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
7 3 6 zmulcld ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
8 5 7 gcdcld ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∈ ℕ0 )
9 2 nnnn0d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℕ0 )
10 gcdcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
11 10 3adant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
12 9 11 nn0mulcld ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∈ ℕ0 )
13 8 nn0cnd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∈ ℂ )
14 2 nncnd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℂ )
15 2 nnne0d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ≠ 0 )
16 13 14 15 divcan2d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) = ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) )
17 gcddvds ⊢ ( ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) ∧ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) ) )
18 5 7 17 syl2anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) ∧ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) ) )
19 18 simpld ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) )
20 16 19 eqbrtrd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · 𝑀 ) )
21 dvdsmul1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝐾 ∥ ( 𝐾 · 𝑀 ) )
22 3 4 21 syl2anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∥ ( 𝐾 · 𝑀 ) )
23 dvdsmul1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∥ ( 𝐾 · 𝑁 ) )
24 3 6 23 syl2anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∥ ( 𝐾 · 𝑁 ) )
25 dvdsgcd ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝐾 · 𝑀 ) ∧ 𝐾 ∥ ( 𝐾 · 𝑁 ) ) → 𝐾 ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ) )
26 3 5 7 25 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝐾 · 𝑀 ) ∧ 𝐾 ∥ ( 𝐾 · 𝑁 ) ) → 𝐾 ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ) )
27 22 24 26 mp2and ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) )
28 8 nn0zd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∈ ℤ )
29 dvdsval2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ∧ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∈ ℤ ) → ( 𝐾 ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ↔ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ ) )
30 3 15 28 29 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ↔ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ ) )
31 27 30 mpbid ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ )
32 dvdscmulr ⊢ ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · 𝑀 ) ↔ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑀 ) )
33 31 4 3 15 32 syl112anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · 𝑀 ) ↔ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑀 ) )
34 20 33 mpbid ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑀 )
35 18 simprd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) )
36 16 35 eqbrtrd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · 𝑁 ) )
37 dvdscmulr ⊢ ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · 𝑁 ) ↔ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑁 ) )
38 31 6 3 15 37 syl112anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · 𝑁 ) ↔ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑁 ) )
39 36 38 mpbid ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑁 )
40 dvdsgcd ⊢ ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑀 ∧ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑁 ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ ( 𝑀 gcd 𝑁 ) ) )
41 31 4 6 40 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑀 ∧ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ 𝑁 ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ ( 𝑀 gcd 𝑁 ) ) )
42 34 39 41 mp2and ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ ( 𝑀 gcd 𝑁 ) )
43 11 nn0zd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℤ )
44 dvdscmul ⊢ ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∈ ℤ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ ( 𝑀 gcd 𝑁 ) → ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )
45 31 43 3 44 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ∥ ( 𝑀 gcd 𝑁 ) → ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )
46 42 45 mpd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) / 𝐾 ) ) ∥ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )
47 16 46 eqbrtrrd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )
48 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
49 48 3adant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
50 49 simpld ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑀 )
51 dvdscmul ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) ) )
52 43 4 3 51 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) ) )
53 50 52 mpd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) )
54 49 simprd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∥ 𝑁 )
55 dvdscmul ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) ) )
56 43 6 3 55 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) ) )
57 54 56 mpd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) )
58 12 nn0zd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∈ ℤ )
59 dvdsgcd ⊢ ( ( ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) → ( ( ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) ∧ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ) )
60 58 5 7 59 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑀 ) ∧ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( 𝐾 · 𝑁 ) ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ) )
61 53 57 60 mp2and ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) )
62 dvdseq ⊢ ( ( ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∈ ℕ0 ∧ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∈ ℕ0 ) ∧ ( ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ∥ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∧ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) ) ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )
63 8 12 47 61 62 syl22anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )
64 63 3expib ⊢ ( 𝐾 ∈ ℕ → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )
65 gcd0val ⊢ ( 0 gcd 0 ) = 0
66 10 3adant1 ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
67 66 nn0cnd ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℂ )
68 67 mul02d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 · ( 𝑀 gcd 𝑁 ) ) = 0 )
69 65 68 eqtr4id ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 gcd 0 ) = ( 0 · ( 𝑀 gcd 𝑁 ) ) )
70 simp1 ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 = 0 )
71 70 oveq1d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑀 ) = ( 0 · 𝑀 ) )
72 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
73 72 3ad2ant2 ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℂ )
74 73 mul02d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 · 𝑀 ) = 0 )
75 71 74 eqtrd ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑀 ) = 0 )
76 70 oveq1d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) = ( 0 · 𝑁 ) )
77 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
78 77 3ad2ant3 ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
79 78 mul02d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 · 𝑁 ) = 0 )
80 76 79 eqtrd ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) = 0 )
81 75 80 oveq12d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 0 gcd 0 ) )
82 70 oveq1d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) = ( 0 · ( 𝑀 gcd 𝑁 ) ) )
83 69 81 82 3eqtr4d ⊢ ( ( 𝐾 = 0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )
84 83 3expib ⊢ ( 𝐾 = 0 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )
85 64 84 jaoi ⊢ ( ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )
86 1 85 sylbi ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )
87 86 3impib ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) )