dvdsmulgcd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvdsmulgcd		Structured version Visualization version GIF version

Theorem dvdsmulgcd 16620

Description: A divisibility equivalent for odmulg 19632. (Contributed by Stefan O'Rear, 6-Sep-2015.)

**Assertion**
Ref	Expression
dvdsmulgcd	⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))

Proof of Theorem dvdsmulgcd Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 780	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐶 ∈ ℤ)
2		dvdszrcl 16321	. . . . . 6 ⊢ (𝐴 ∥ (𝐵 · 𝐶) → (𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ))
3	2	adantl 486	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → (𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ))
4	3	simpld 499	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐴 ∈ ℤ)
5		bezout 16607	. . . 4 ⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)))
6	1, 4, 5	syl2anc 595	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)))
7	4	adantr 485	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∈ ℤ)
8		simplll 786	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐵 ∈ ℤ)
9		simpllr 787	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐶 ∈ ℤ)
10		simprl 782	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℤ)
11	9, 10	zmulcld 12712	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐶 · 𝑥) ∈ ℤ)
12	8, 11	zmulcld 12712	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐶 · 𝑥)) ∈ ℤ)
13		simprr 784	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℤ)
14	7, 13	zmulcld 12712	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 · 𝑦) ∈ ℤ)
15	8, 14	zmulcld 12712	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐴 · 𝑦)) ∈ ℤ)
16	8, 9	zmulcld 12712	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · 𝐶) ∈ ℤ)
17		simplr 780	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · 𝐶))
18	7, 16, 10, 17	dvdsmultr1d 16361	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ ((𝐵 · 𝐶) · 𝑥))
19	8	zcnd 12707	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐵 ∈ ℂ)
20	9	zcnd 12707	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐶 ∈ ℂ)
21	10	zcnd 12707	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℂ)
22	19, 20, 21	mulassd 11238	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐵 · 𝐶) · 𝑥) = (𝐵 · (𝐶 · 𝑥)))
23	18, 22	breqtrd 5136	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · (𝐶 · 𝑥)))
24	8, 13	zmulcld 12712	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℤ)
25		dvdsmul1 16341	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 · 𝑦) ∈ ℤ) → 𝐴 ∥ (𝐴 · (𝐵 · 𝑦)))
26	7, 24, 25	syl2anc 595	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐴 · (𝐵 · 𝑦)))
27	7	zcnd 12707	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∈ ℂ)
28	13	zcnd 12707	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℂ)
29	19, 27, 28	mul12d 11425	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐴 · 𝑦)) = (𝐴 · (𝐵 · 𝑦)))
30	26, 29	breqtrrd 5138	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · (𝐴 · 𝑦)))
31	7, 12, 15, 23, 30	dvds2addd 16356	. . . . . 6 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦))))
32	11	zcnd 12707	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐶 · 𝑥) ∈ ℂ)
33	14	zcnd 12707	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 · 𝑦) ∈ ℂ)
34	19, 32, 33	adddid 11239	. . . . . 6 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))) = ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦))))
35	31, 34	breqtrrd 5138	. . . . 5 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))))
36		oveq2 7420	. . . . . 6 ⊢ ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → (𝐵 · (𝐶 gcd 𝐴)) = (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))))
37	36	breq2d 5120	. . . . 5 ⊢ ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → (𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) ↔ 𝐴 ∥ (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦)))))
38	35, 37	syl5ibrcom 250	. . . 4 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))
39	38	rexlimdvva 3221	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))
40	6, 39	mpd 16	. 2 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))
41		dvdszrcl 16321	. . . . 5 ⊢ (𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) → (𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ))
42	41	adantl 486	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐴 ∈ ℤ ∧ (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ))
43	42	simpld 499	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∈ ℤ)
44	42	simprd 500	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · (𝐶 gcd 𝐴)) ∈ ℤ)
45		zmulcl 12649	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ)
46	45	adantr 485	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · 𝐶) ∈ ℤ)
47		simpr 489	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))
48		simplr 780	. . . . . 6 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐶 ∈ ℤ)
49		gcddvds 16567	. . . . . 6 ⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐶 gcd 𝐴) ∥ 𝐶 ∧ (𝐶 gcd 𝐴) ∥ 𝐴))
50	48, 43, 49	syl2anc 595	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → ((𝐶 gcd 𝐴) ∥ 𝐶 ∧ (𝐶 gcd 𝐴) ∥ 𝐴))
51	50	simpld 499	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∥ 𝐶)
52	48, 43	gcdcld 16572	. . . . . 6 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∈ ℕ₀)
53	52	nn0zd 12622	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∈ ℤ)
54		simpll 778	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐵 ∈ ℤ)
55		dvdscmul 16346	. . . . 5 ⊢ (((𝐶 gcd 𝐴) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐶 gcd 𝐴) ∥ 𝐶 → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶)))
56	53, 48, 54, 55	syl3anc 1397	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → ((𝐶 gcd 𝐴) ∥ 𝐶 → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶)))
57	51, 56	mpd 16	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶))
58	43, 44, 46, 47, 57	dvdstrd 16359	. 2 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∥ (𝐵 · 𝐶))
59	40, 58	impbida 812	1 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1569 ∈ wcel 2142 ∃wrex 3088 class class class wbr 5108 (class class class)co 7412 + caddc 11109 · cmul 11111 ℤcz 12597 ∥ cdvds 16316 gcd cgcd 16558

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-sup 9400 df-inf 9401 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-n0 12511 df-z 12598 df-uz 12869 df-rp 13023 df-fl 13832 df-mod 13910 df-seq 14045 df-exp 14105 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-dvds 16317 df-gcd 16559

This theorem is used by: coprmdvds 16717 odmulg 19632 fpprwpprb 48533

W3C validator