mulgcddvds - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mulgcddvds		GIF version

Theorem mulgcddvds 12668

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

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

**Proof of Theorem mulgcddvds**
Step	Hyp	Ref	Expression
1		simp1 1023	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ ℤ)
2		simp2 1024	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
3		simp3 1025	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
4	2, 3	zmulcld 9608	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ)
5	1, 4	gcdcld 12541	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∈ ℕ₀)
6	5	nn0zd 9600	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ)
7		dvds0 12369	. . . . 5 ⊢ ((𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ → (𝐾 gcd (𝑀 · 𝑁)) ∥ 0)
8	6, 7	syl 14	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ 0)
9	8	adantr 276	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) = 0) → (𝐾 gcd (𝑀 · 𝑁)) ∥ 0)
10		oveq2 6026	. . . 4 ⊢ ((𝐾 gcd 𝑁) = 0 → ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)) = ((𝐾 gcd 𝑀) · 0))
11	1, 2	gcdcld 12541	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑀) ∈ ℕ₀)
12	11	nn0cnd 9457	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑀) ∈ ℂ)
13	12	mul01d 8572	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑀) · 0) = 0)
14	10, 13	sylan9eqr 2286	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) = 0) → ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)) = 0)
15	9, 14	breqtrrd 4116	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) = 0) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)))
16	6	adantr 276	. . . . 5 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ)
17	16	zcnd 9603	. . . 4 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd (𝑀 · 𝑁)) ∈ ℂ)
18	1, 3	gcdcld 12541	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∈ ℕ₀)
19	18	nn0zd 9600	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∈ ℤ)
20	19	adantr 276	. . . . 5 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd 𝑁) ∈ ℤ)
21	20	zcnd 9603	. . . 4 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd 𝑁) ∈ ℂ)
22		0zd 9491	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
23		zapne 9554	. . . . . 6 ⊢ (((𝐾 gcd 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐾 gcd 𝑁) # 0 ↔ (𝐾 gcd 𝑁) ≠ 0))
24	19, 22, 23	syl2anc 411	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑁) # 0 ↔ (𝐾 gcd 𝑁) ≠ 0))
25	24	biimpar 297	. . . 4 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd 𝑁) # 0)
26	17, 21, 25	divcanap1d 8971	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) = (𝐾 gcd (𝑀 · 𝑁)))
27		gcddvds 12536	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → ((𝐾 gcd (𝑀 · 𝑁)) ∥ 𝐾 ∧ (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · 𝑁)))
28	1, 4, 27	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd (𝑀 · 𝑁)) ∥ 𝐾 ∧ (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · 𝑁)))
29	28	simpld 112	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ 𝐾)
30	6, 1, 19, 29	dvdsmultr1d 12395	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝐾 · (𝐾 gcd 𝑁)))
31	30	adantr 276	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝐾 · (𝐾 gcd 𝑁)))
32	26, 31	eqbrtrd 4110	. . . . . 6 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ (𝐾 · (𝐾 gcd 𝑁)))
33		gcddvds 12536	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑁) ∥ 𝐾 ∧ (𝐾 gcd 𝑁) ∥ 𝑁))
34	1, 3, 33	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑁) ∥ 𝐾 ∧ (𝐾 gcd 𝑁) ∥ 𝑁))
35	34	simpld 112	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∥ 𝐾)
36	34	simprd 114	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∥ 𝑁)
37		dvdsmultr2 12396	. . . . . . . . . . . 12 ⊢ (((𝐾 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑁) ∥ 𝑁 → (𝐾 gcd 𝑁) ∥ (𝑀 · 𝑁)))
38	19, 2, 3, 37	syl3anc 1273	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑁) ∥ 𝑁 → (𝐾 gcd 𝑁) ∥ (𝑀 · 𝑁)))
39	36, 38	mpd 13	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∥ (𝑀 · 𝑁))
40		dvdsgcd 12585	. . . . . . . . . . 11 ⊢ (((𝐾 gcd 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝐾 gcd 𝑁) ∥ 𝐾 ∧ (𝐾 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝐾 gcd 𝑁) ∥ (𝐾 gcd (𝑀 · 𝑁))))
41	19, 1, 4, 40	syl3anc 1273	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐾 gcd 𝑁) ∥ 𝐾 ∧ (𝐾 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝐾 gcd 𝑁) ∥ (𝐾 gcd (𝑀 · 𝑁))))
42	35, 39, 41	mp2and 433	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∥ (𝐾 gcd (𝑀 · 𝑁)))
43	42	adantr 276	. . . . . . . 8 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd 𝑁) ∥ (𝐾 gcd (𝑀 · 𝑁)))
44		simpr 110	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd 𝑁) ≠ 0)
45		dvdsval2 12353	. . . . . . . . 9 ⊢ (((𝐾 gcd 𝑁) ∈ ℤ ∧ (𝐾 gcd 𝑁) ≠ 0 ∧ (𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ) → ((𝐾 gcd 𝑁) ∥ (𝐾 gcd (𝑀 · 𝑁)) ↔ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ))
46	20, 44, 16, 45	syl3anc 1273	. . . . . . . 8 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((𝐾 gcd 𝑁) ∥ (𝐾 gcd (𝑀 · 𝑁)) ↔ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ))
47	43, 46	mpbid 147	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ)
48	1	adantr 276	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → 𝐾 ∈ ℤ)
49		dvdsmulcr 12384	. . . . . . 7 ⊢ ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ((𝐾 gcd 𝑁) ∈ ℤ ∧ (𝐾 gcd 𝑁) ≠ 0)) → ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ (𝐾 · (𝐾 gcd 𝑁)) ↔ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝐾))
50	47, 48, 20, 44, 49	syl112anc 1277	. . . . . 6 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ (𝐾 · (𝐾 gcd 𝑁)) ↔ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝐾))
51	32, 50	mpbid 147	. . . . 5 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝐾)
52		nn0abscl 11647	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → (abs‘𝑀) ∈ ℕ₀)
53	2, 52	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘𝑀) ∈ ℕ₀)
54	53	nn0zd 9600	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘𝑀) ∈ ℤ)
55		dvdsmultr2 12396	. . . . . . . . . . . . 13 ⊢ (((𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ (abs‘𝑀) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝐾 gcd (𝑀 · 𝑁)) ∥ 𝐾 → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝐾)))
56	6, 54, 1, 55	syl3anc 1273	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd (𝑀 · 𝑁)) ∥ 𝐾 → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝐾)))
57	29, 56	mpd 13	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝐾))
58	28	simprd 114	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · 𝑁))
59		iddvds 12367	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∥ 𝑀)
60	2, 59	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ 𝑀)
61		dvdsabsb 12373	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∥ 𝑀 ↔ 𝑀 ∥ (abs‘𝑀)))
62	2, 2, 61	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑀 ↔ 𝑀 ∥ (abs‘𝑀)))
63	60, 62	mpbid 147	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (abs‘𝑀))
64		dvdsmulc 12382	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ (abs‘𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (abs‘𝑀) → (𝑀 · 𝑁) ∥ ((abs‘𝑀) · 𝑁)))
65	2, 54, 3, 64	syl3anc 1273	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (abs‘𝑀) → (𝑀 · 𝑁) ∥ ((abs‘𝑀) · 𝑁)))
66	63, 65	mpd 13	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∥ ((abs‘𝑀) · 𝑁))
67	54, 3	zmulcld 9608	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) · 𝑁) ∈ ℤ)
68		dvdstr 12391	. . . . . . . . . . . . 13 ⊢ (((𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ ∧ ((abs‘𝑀) · 𝑁) ∈ ℤ) → (((𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · 𝑁) ∧ (𝑀 · 𝑁) ∥ ((abs‘𝑀) · 𝑁)) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝑁)))
69	6, 4, 67, 68	syl3anc 1273	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · 𝑁) ∧ (𝑀 · 𝑁) ∥ ((abs‘𝑀) · 𝑁)) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝑁)))
70	58, 66, 69	mp2and 433	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝑁))
71	54, 1	zmulcld 9608	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) · 𝐾) ∈ ℤ)
72		dvdsgcd 12585	. . . . . . . . . . . 12 ⊢ (((𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ ((abs‘𝑀) · 𝐾) ∈ ℤ ∧ ((abs‘𝑀) · 𝑁) ∈ ℤ) → (((𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝐾) ∧ (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝑁)) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (((abs‘𝑀) · 𝐾) gcd ((abs‘𝑀) · 𝑁))))
73	6, 71, 67, 72	syl3anc 1273	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝐾) ∧ (𝐾 gcd (𝑀 · 𝑁)) ∥ ((abs‘𝑀) · 𝑁)) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (((abs‘𝑀) · 𝐾) gcd ((abs‘𝑀) · 𝑁))))
74	57, 70, 73	mp2and 433	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (((abs‘𝑀) · 𝐾) gcd ((abs‘𝑀) · 𝑁)))
75	18	nn0red 9456	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∈ ℝ)
76	18	nn0ge0d 9458	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝐾 gcd 𝑁))
77	75, 76	absidd 11729	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐾 gcd 𝑁)) = (𝐾 gcd 𝑁))
78	77	oveq2d 6034	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) · (abs‘(𝐾 gcd 𝑁))) = ((abs‘𝑀) · (𝐾 gcd 𝑁)))
79	2	zcnd 9603	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ)
80	18	nn0cnd 9457	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑁) ∈ ℂ)
81	79, 80	absmuld 11756	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝑀 · (𝐾 gcd 𝑁))) = ((abs‘𝑀) · (abs‘(𝐾 gcd 𝑁))))
82		mulgcd 12589	. . . . . . . . . . . 12 ⊢ (((abs‘𝑀) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((abs‘𝑀) · 𝐾) gcd ((abs‘𝑀) · 𝑁)) = ((abs‘𝑀) · (𝐾 gcd 𝑁)))
83	53, 1, 3, 82	syl3anc 1273	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((abs‘𝑀) · 𝐾) gcd ((abs‘𝑀) · 𝑁)) = ((abs‘𝑀) · (𝐾 gcd 𝑁)))
84	78, 81, 83	3eqtr4d 2274	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝑀 · (𝐾 gcd 𝑁))) = (((abs‘𝑀) · 𝐾) gcd ((abs‘𝑀) · 𝑁)))
85	74, 84	breqtrrd 4116	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (abs‘(𝑀 · (𝐾 gcd 𝑁))))
86	2, 19	zmulcld 9608	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · (𝐾 gcd 𝑁)) ∈ ℤ)
87		dvdsabsb 12373	. . . . . . . . . 10 ⊢ (((𝐾 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ (𝑀 · (𝐾 gcd 𝑁)) ∈ ℤ) → ((𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)) ↔ (𝐾 gcd (𝑀 · 𝑁)) ∥ (abs‘(𝑀 · (𝐾 gcd 𝑁)))))
88	6, 86, 87	syl2anc 411	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)) ↔ (𝐾 gcd (𝑀 · 𝑁)) ∥ (abs‘(𝑀 · (𝐾 gcd 𝑁)))))
89	85, 88	mpbird 167	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)))
90	89	adantr 276	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd (𝑀 · 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)))
91	26, 90	eqbrtrd 4110	. . . . . 6 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)))
92	2	adantr 276	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → 𝑀 ∈ ℤ)
93		dvdsmulcr 12384	. . . . . . 7 ⊢ ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 gcd 𝑁) ∈ ℤ ∧ (𝐾 gcd 𝑁) ≠ 0)) → ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)) ↔ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝑀))
94	47, 92, 20, 44, 93	syl112anc 1277	. . . . . 6 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ (𝑀 · (𝐾 gcd 𝑁)) ↔ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝑀))
95	91, 94	mpbid 147	. . . . 5 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝑀)
96		dvdsgcd 12585	. . . . . 6 ⊢ ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝐾 ∧ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝑀) → ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ (𝐾 gcd 𝑀)))
97	47, 48, 92, 96	syl3anc 1273	. . . . 5 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝐾 ∧ ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ 𝑀) → ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ (𝐾 gcd 𝑀)))
98	51, 95, 97	mp2and 433	. . . 4 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → ((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ (𝐾 gcd 𝑀))
99	11	nn0zd 9600	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd 𝑀) ∈ ℤ)
100	99	adantr 276	. . . . 5 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd 𝑀) ∈ ℤ)
101		dvdsmulc 12382	. . . . 5 ⊢ ((((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∈ ℤ ∧ (𝐾 gcd 𝑀) ∈ ℤ ∧ (𝐾 gcd 𝑁) ∈ ℤ) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ (𝐾 gcd 𝑀) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁))))
102	47, 100, 20, 101	syl3anc 1273	. . . 4 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) ∥ (𝐾 gcd 𝑀) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁))))
103	98, 102	mpd 13	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (((𝐾 gcd (𝑀 · 𝑁)) / (𝐾 gcd 𝑁)) · (𝐾 gcd 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)))
104	26, 103	eqbrtrrd 4112	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑁) ≠ 0) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)))
105		zdceq 9555	. . . 4 ⊢ (((𝐾 gcd 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → DECID (𝐾 gcd 𝑁) = 0)
106	19, 22, 105	syl2anc 411	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐾 gcd 𝑁) = 0)
107		exmiddc 843	. . . 4 ⊢ (DECID (𝐾 gcd 𝑁) = 0 → ((𝐾 gcd 𝑁) = 0 ∨ ¬ (𝐾 gcd 𝑁) = 0))
108		df-ne 2403	. . . . 5 ⊢ ((𝐾 gcd 𝑁) ≠ 0 ↔ ¬ (𝐾 gcd 𝑁) = 0)
109	108	orbi2i 769	. . . 4 ⊢ (((𝐾 gcd 𝑁) = 0 ∨ (𝐾 gcd 𝑁) ≠ 0) ↔ ((𝐾 gcd 𝑁) = 0 ∨ ¬ (𝐾 gcd 𝑁) = 0))
110	107, 109	sylibr 134	. . 3 ⊢ (DECID (𝐾 gcd 𝑁) = 0 → ((𝐾 gcd 𝑁) = 0 ∨ (𝐾 gcd 𝑁) ≠ 0))
111	106, 110	syl 14	. 2 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑁) = 0 ∨ (𝐾 gcd 𝑁) ≠ 0))
112	15, 104, 111	mpjaodan 805	1 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 715 DECID wdc 841 ∧ w3a 1004 = wceq 1397 ∈ wcel 2202 ≠ wne 2402 class class class wbr 4088 ‘cfv 5326 (class class class)co 6018 0cc0 8032 · cmul 8037 # cap 8761 / cdiv 8852 ℕ₀cn0 9402 ℤcz 9479 abscabs 11559 ∥ cdvds 12350 gcd cgcd 12526

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8123 ax-resscn 8124 ax-1cn 8125 ax-1re 8126 ax-icn 8127 ax-addcl 8128 ax-addrcl 8129 ax-mulcl 8130 ax-mulrcl 8131 ax-addcom 8132 ax-mulcom 8133 ax-addass 8134 ax-mulass 8135 ax-distr 8136 ax-i2m1 8137 ax-0lt1 8138 ax-1rid 8139 ax-0id 8140 ax-rnegex 8141 ax-precex 8142 ax-cnre 8143 ax-pre-ltirr 8144 ax-pre-ltwlin 8145 ax-pre-lttrn 8146 ax-pre-apti 8147 ax-pre-ltadd 8148 ax-pre-mulgt0 8149 ax-pre-mulext 8150 ax-arch 8151 ax-caucvg 8152

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-riota 5971 df-ov 6021 df-oprab 6022 df-mpo 6023 df-1st 6303 df-2nd 6304 df-recs 6471 df-frec 6557 df-sup 7183 df-pnf 8216 df-mnf 8217 df-xr 8218 df-ltxr 8219 df-le 8220 df-sub 8352 df-neg 8353 df-reap 8755 df-ap 8762 df-div 8853 df-inn 9144 df-2 9202 df-3 9203 df-4 9204 df-n0 9403 df-z 9480 df-uz 9756 df-q 9854 df-rp 9889 df-fz 10244 df-fzo 10378 df-fl 10531 df-mod 10586 df-seqfrec 10711 df-exp 10802 df-cj 11404 df-re 11405 df-im 11406 df-rsqrt 11560 df-abs 11561 df-dvds 12351 df-gcd 12527

This theorem is referenced by: rpmulgcd2 12669 rpmul 12672

W3C validator