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 16617

Description: A divisibility equivalent for odmulg 19629. (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 16318	. . . . . 6 ⊢ (𝐴 ∥ (𝐵 · 𝐶) → (𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ))
3	2	adantl 486	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → (𝐴 ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ))
4	3	simpld 499	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐴 ∈ ℤ)
5		bezout 16604	. . . 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 12709	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐶 · 𝑥) ∈ ℤ)
12	8, 11	zmulcld 12709	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐶 · 𝑥)) ∈ ℤ)
13		simprr 784	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℤ)
14	7, 13	zmulcld 12709	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 · 𝑦) ∈ ℤ)
15	8, 14	zmulcld 12709	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐴 · 𝑦)) ∈ ℤ)
16	8, 9	zmulcld 12709	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · 𝐶) ∈ ℤ)
17		simplr 780	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · 𝐶))
18	7, 16, 10, 17	dvdsmultr1d 16358	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ ((𝐵 · 𝐶) · 𝑥))
19	8	zcnd 12704	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐵 ∈ ℂ)
20	9	zcnd 12704	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐶 ∈ ℂ)
21	10	zcnd 12704	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℂ)
22	19, 20, 21	mulassd 11235	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐵 · 𝐶) · 𝑥) = (𝐵 · (𝐶 · 𝑥)))
23	18, 22	breqtrd 5142	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · (𝐶 · 𝑥)))
24	8, 13	zmulcld 12709	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℤ)
25		dvdsmul1 16338	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ (𝐵 · 𝑦) ∈ ℤ) → 𝐴 ∥ (𝐴 · (𝐵 · 𝑦)))
26	7, 24, 25	syl2anc 595	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐴 · (𝐵 · 𝑦)))
27	7	zcnd 12704	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∈ ℂ)
28	13	zcnd 12704	. . . . . . . . 9 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℂ)
29	19, 27, 28	mul12d 11422	. . . . . . . 8 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · (𝐴 · 𝑦)) = (𝐴 · (𝐵 · 𝑦)))
30	26, 29	breqtrrd 5144	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · (𝐴 · 𝑦)))
31	7, 12, 15, 23, 30	dvds2addd 16353	. . . . . 6 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦))))
32	11	zcnd 12704	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐶 · 𝑥) ∈ ℂ)
33	14	zcnd 12704	. . . . . . 7 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐴 · 𝑦) ∈ ℂ)
34	19, 32, 33	adddid 11236	. . . . . 6 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))) = ((𝐵 · (𝐶 · 𝑥)) + (𝐵 · (𝐴 · 𝑦))))
35	31, 34	breqtrrd 5144	. . . . 5 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝐴 ∥ (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))))
36		oveq2 7422	. . . . . 6 ⊢ ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → (𝐵 · (𝐶 gcd 𝐴)) = (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦))))
37	36	breq2d 5126	. . . . 5 ⊢ ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → (𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)) ↔ 𝐴 ∥ (𝐵 · ((𝐶 · 𝑥) + (𝐴 · 𝑦)))))
38	35, 37	syl5ibrcom 250	. . . 4 ⊢ ((((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))
39	38	rexlimdvva 3229	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐶 gcd 𝐴) = ((𝐶 · 𝑥) + (𝐴 · 𝑦)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))
40	6, 39	mpd 16	. 2 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · 𝐶)) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))
41		dvdszrcl 16318	. . . . 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 12646	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ)
46	45	adantr 485	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · 𝐶) ∈ ℤ)
47		simpr 489	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))
48		simplr 780	. . . . . 6 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐶 ∈ ℤ)
49		gcddvds 16564	. . . . . 6 ⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐶 gcd 𝐴) ∥ 𝐶 ∧ (𝐶 gcd 𝐴) ∥ 𝐴))
50	48, 43, 49	syl2anc 595	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → ((𝐶 gcd 𝐴) ∥ 𝐶 ∧ (𝐶 gcd 𝐴) ∥ 𝐴))
51	50	simpld 499	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∥ 𝐶)
52	48, 43	gcdcld 16569	. . . . . 6 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∈ ℕ₀)
53	52	nn0zd 12619	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐶 gcd 𝐴) ∈ ℤ)
54		simpll 778	. . . . 5 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐵 ∈ ℤ)
55		dvdscmul 16343	. . . . 5 ⊢ (((𝐶 gcd 𝐴) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐶 gcd 𝐴) ∥ 𝐶 → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶)))
56	53, 48, 54, 55	syl3anc 1396	. . . 4 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → ((𝐶 gcd 𝐴) ∥ 𝐶 → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶)))
57	51, 56	mpd 16	. . 3 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → (𝐵 · (𝐶 gcd 𝐴)) ∥ (𝐵 · 𝐶))
58	43, 44, 46, 47, 57	dvdstrd 16356	. 2 ⊢ (((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))) → 𝐴 ∥ (𝐵 · 𝐶))
59	40, 58	impbida 812	1 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1568 ∈ wcel 2150 ∃wrex 3096 class class class wbr 5114 (class class class)co 7414 + caddc 11106 · cmul 11108 ℤcz 12594 ∥ cdvds 16313 gcd cgcd 16555

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2152 ax-9 2160 ax-10 2183 ax-11 2199 ax-12 2220 ax-ext 2742 ax-sep 5262 ax-nul 5274 ax-pow 5340 ax-pr 5408 ax-un 7736 ax-cnex 11159 ax-resscn 11160 ax-1cn 11161 ax-icn 11162 ax-addcl 11163 ax-addrcl 11164 ax-mulcl 11165 ax-mulrcl 11166 ax-mulcom 11167 ax-addass 11168 ax-mulass 11169 ax-distr 11170 ax-i2m1 11171 ax-1ne0 11172 ax-1rid 11173 ax-rnegex 11174 ax-rrecex 11175 ax-cnre 11176 ax-pre-lttri 11177 ax-pre-lttrn 11178 ax-pre-ltadd 11179 ax-pre-mulgt0 11180 ax-pre-sup 11181

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2099 df-mo 2574 df-eu 2604 df-clab 2749 df-cleq 2762 df-clel 2845 df-nfc 2919 df-ne 2966 df-nel 3072 df-ral 3087 df-rex 3097 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3464 df-sbc 3753 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5560 df-eprel 5565 df-po 5573 df-so 5574 df-fr 5618 df-we 5620 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7866 df-2nd 7990 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-er 8697 df-en 8947 df-dom 8948 df-sdom 8949 df-sup 9405 df-inf 9406 df-pnf 11248 df-mnf 11249 df-xr 11250 df-ltxr 11251 df-le 11252 df-sub 11446 df-neg 11447 df-div 11875 df-nn 12237 df-2 12306 df-3 12307 df-n0 12508 df-z 12595 df-uz 12866 df-rp 13020 df-fl 13828 df-mod 13906 df-seq 14041 df-exp 14101 df-cj 15153 df-re 15154 df-im 15155 df-sqrt 15289 df-abs 15290 df-dvds 16314 df-gcd 16556

This theorem is referenced by: coprmdvds 16714 odmulg 19629 fpprwpprb 48454

W3C validator