Definition df-bj-divc

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

Since 0 is absorbing, |- ( A e. ( CCbar u. CChat ) -> ( A ||C 0 ) ) and |- ( ( 0 ||C A ) <-> A = 0 ) .

(Contributed by BJ, 28-Jul-2023)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdivc	⊢ ∥ℂ
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	2	cv	⊢ 𝑦
5	3 4	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
6		cccbar	⊢ ℂ̅
7	6 6	cxp	⊢ ( ℂ̅ × ℂ̅ )
8		ccchat	⊢ ℂ̂
9	8 8	cxp	⊢ ( ℂ̂ × ℂ̂ )
10	7 9	cun	⊢ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) )
11	5 10	wcel	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) )
12		vn	⊢ 𝑛
13		czzbar	⊢ ℤ̅
14		czzhat	⊢ ℤ̂
15	13 14	cun	⊢ ( ℤ̅ ∪ ℤ̂ )
16	12	cv	⊢ 𝑛
17		cmulc	⊢ ·ℂ̅
18	16 3 17	co	⊢ ( 𝑛 ·ℂ̅ 𝑥 )
19	18 4	wceq	⊢ ( 𝑛 ·ℂ̅ 𝑥 ) = 𝑦
20	19 12 15	wrex	⊢ ∃ 𝑛 ∈ ( ℤ̅ ∪ ℤ̂ ) ( 𝑛 ·ℂ̅ 𝑥 ) = 𝑦
21	11 20	wa	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) ) ∧ ∃ 𝑛 ∈ ( ℤ̅ ∪ ℤ̂ ) ( 𝑛 ·ℂ̅ 𝑥 ) = 𝑦 )
22	21 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) ) ∧ ∃ 𝑛 ∈ ( ℤ̅ ∪ ℤ̂ ) ( 𝑛 ·ℂ̅ 𝑥 ) = 𝑦 ) }
23	0 22	wceq	⊢ ∥ℂ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) ) ∧ ∃ 𝑛 ∈ ( ℤ̅ ∪ ℤ̂ ) ( 𝑛 ·ℂ̅ 𝑥 ) = 𝑦 ) }