Definition df-bj-divc 35365

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

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 35364	. 2 class ∥ℂ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1538	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1538	. . . . . 6 class 𝑦
6	3, 5	cop 4564	. . . . 5 class ⟨𝑥, 𝑦⟩
7		cccbar 35313	. . . . . . 7 class ℂ̅
8	7, 7	cxp 5578	. . . . . 6 class (ℂ̅ × ℂ̅)
9		ccchat 35330	. . . . . . 7 class ℂ̂
10	9, 9	cxp 5578	. . . . . 6 class (ℂ̂ × ℂ̂)
11	8, 10	cun 3881	. . . . 5 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
12	6, 11	wcel 2108	. . . 4 wff ⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
13		vn	. . . . . . . 8 setvar 𝑛
14	13	cv 1538	. . . . . . 7 class 𝑛
15		cmulc 35343	. . . . . . 7 class ·ℂ̅
16	14, 3, 15	co 7255	. . . . . 6 class (𝑛 ·ℂ̅ 𝑥)
17	16, 5	wceq 1539	. . . . 5 wff (𝑛 ·ℂ̅ 𝑥) = 𝑦
18		czzbar 35360	. . . . . 6 class ℤ̅
19		czzhat 35362	. . . . . 6 class ℤ̂
20	18, 19	cun 3881	. . . . 5 class (ℤ̅ ∪ ℤ̂)
21	17, 13, 20	wrex 3064	. . . 4 wff ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦
22	12, 21	wa 395	. . 3 wff (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)
23	22, 2, 4	copab 5132	. 2 class {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
24	1, 23	wceq 1539	1 wff ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}

This definition is referenced by: (None)