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 𝑁 ) ) )