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 ( 𝑀 · 𝑁 ) ) ∈ ℕ₀ )
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 𝑀 ) ∈ ℕ₀ )
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 𝑁 ) ∈ ℕ₀ )
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 ‘ 𝑀 ) ∈ ℕ₀ )
49	2 48	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ 𝑀 ) ∈ ℕ₀ )
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 ‘ 𝑀 ) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 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 𝑁 ) ) )

Metamath Proof Explorer

Theorem mulgcddvds

Proof