Definition df-bj-divc 34577

Description: Definition of the divisibility relation (compare df-dvds 15601).

Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥_ℂ 0)) and ⊢ ((0 ∥_ℂ 𝐴) ↔ 𝐴 = 0).

(Contributed by BJ, 28-Jul-2023.)

Assertion

Ref	Expression
df-bj-divc	⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}

Distinct variable group:   𝑥,𝑛,𝑦

Detailed syntax breakdown of Definition df-bj-divc

Step	Hyp	Ref	Expression
1		cdivc 34576	. 2 class ∥ℂ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1535	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1535	. . . . . 6 class 𝑦
6	3, 5	cop 4566	. . . . 5 class ⟨𝑥, 𝑦⟩
7		cccbar 34525	. . . . . . 7 class ℂ̅
8	7, 7	cxp 5546	. . . . . 6 class (ℂ̅ × ℂ̅)
9		ccchat 34542	. . . . . . 7 class ℂ̂
10	9, 9	cxp 5546	. . . . . 6 class (ℂ̂ × ℂ̂)
11	8, 10	cun 3927	. . . . 5 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
12	6, 11	wcel 2113	. . . 4 wff ⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
13		vn	. . . . . . . 8 setvar 𝑛
14	13	cv 1535	. . . . . . 7 class 𝑛
15		cmulc 34555	. . . . . . 7 class ·ℂ̅
16	14, 3, 15	co 7149	. . . . . 6 class (𝑛 ·ℂ̅ 𝑥)
17	16, 5	wceq 1536	. . . . 5 wff (𝑛 ·ℂ̅ 𝑥) = 𝑦
18		czzbar 34572	. . . . . 6 class ℤ̅
19		czzhat 34574	. . . . . 6 class ℤ̂
20	18, 19	cun 3927	. . . . 5 class (ℤ̅ ∪ ℤ̂)
21	17, 13, 20	wrex 3138	. . . 4 wff ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦
22	12, 21	wa 398	. . 3 wff (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)
23	22, 2, 4	copab 5121	. 2 class {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
24	1, 23	wceq 1536	1 wff ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}

This definition is referenced by: (None)