Definition df-bj-divc 36143

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

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 36142	. 2 class ∥ℂ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1540	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1540	. . . . . 6 class 𝑦
6	3, 5	cop 4634	. . . . 5 class ⟨𝑥, 𝑦⟩
7		cccbar 36091	. . . . . . 7 class ℂ̅
8	7, 7	cxp 5674	. . . . . 6 class (ℂ̅ × ℂ̅)
9		ccchat 36108	. . . . . . 7 class ℂ̂
10	9, 9	cxp 5674	. . . . . 6 class (ℂ̂ × ℂ̂)
11	8, 10	cun 3946	. . . . 5 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
12	6, 11	wcel 2106	. . . 4 wff ⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
13		vn	. . . . . . . 8 setvar 𝑛
14	13	cv 1540	. . . . . . 7 class 𝑛
15		cmulc 36121	. . . . . . 7 class ·ℂ̅
16	14, 3, 15	co 7408	. . . . . 6 class (𝑛 ·ℂ̅ 𝑥)
17	16, 5	wceq 1541	. . . . 5 wff (𝑛 ·ℂ̅ 𝑥) = 𝑦
18		czzbar 36138	. . . . . 6 class ℤ̅
19		czzhat 36140	. . . . . 6 class ℤ̂
20	18, 19	cun 3946	. . . . 5 class (ℤ̅ ∪ ℤ̂)
21	17, 13, 20	wrex 3070	. . . 4 wff ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦
22	12, 21	wa 396	. . 3 wff (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)
23	22, 2, 4	copab 5210	. 2 class {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
24	1, 23	wceq 1541	1 wff ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}

This definition is referenced by: (None)