Definition df-bj-divc 38156

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

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 38155	. 2 class ∥ℂ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1569	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1569	. . . . . 6 class 𝑦
6	3, 5	cop 4590	. . . . 5 class ⟨𝑥, 𝑦⟩
7		cccbar 38104	. . . . . . 7 class ℂ̅
8	7, 7	cxp 5649	. . . . . 6 class (ℂ̅ × ℂ̅)
9		ccchat 38121	. . . . . . 7 class ℂ̂
10	9, 9	cxp 5649	. . . . . 6 class (ℂ̂ × ℂ̂)
11	8, 10	cun 3897	. . . . 5 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
12	6, 11	wcel 2145	. . . 4 wff ⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
13		vn	. . . . . . . 8 setvar 𝑛
14	13	cv 1569	. . . . . . 7 class 𝑛
15		cmulc 38134	. . . . . . 7 class ·ℂ̅
16	14, 3, 15	co 7412	. . . . . 6 class (𝑛 ·ℂ̅ 𝑥)
17	16, 5	wceq 1570	. . . . 5 wff (𝑛 ·ℂ̅ 𝑥) = 𝑦
18		czzbar 38151	. . . . . 6 class ℤ̅
19		czzhat 38153	. . . . . 6 class ℤ̂
20	18, 19	cun 3897	. . . . 5 class (ℤ̅ ∪ ℤ̂)
21	17, 13, 20	wrex 3087	. . . 4 wff ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦
22	12, 21	wa 401	. . 3 wff (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)
23	22, 2, 4	copab 5167	. 2 class {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
24	1, 23	wceq 1570	1 wff ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}

This definition is used by: (None)