df-bj-divc

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

		Ref	Expression
	Assertion	df-bj-divc	$⊢ ∥_{ℂ} = \{⟨x, y⟩ \| (⟨x, y⟩ \in ((\overline{ℂ} \times \overline{ℂ}) \cup (\hat{ℂ} \times \hat{ℂ})) \land \exists n \in (\overline{ℤ} \cup \hat{ℤ}) n \cdot_{\overline{ℂ}} x = y)\}$

Step	Hyp	Ref	Expression
0		cdivc	$class ∥_{ℂ}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4	2	cv	$setvar y$
5	3 4	cop	$class ⟨x, y⟩$
6		cccbar	$class \overline{ℂ}$
7	6 6	cxp	$class (\overline{ℂ} \times \overline{ℂ})$
8		ccchat	$class \hat{ℂ}$
9	8 8	cxp	$class (\hat{ℂ} \times \hat{ℂ})$
10	7 9	cun	$class ((\overline{ℂ} \times \overline{ℂ}) \cup (\hat{ℂ} \times \hat{ℂ}))$
11	5 10	wcel	$wff ⟨x, y⟩ \in ((\overline{ℂ} \times \overline{ℂ}) \cup (\hat{ℂ} \times \hat{ℂ}))$
12		vn	$setvar n$
13		czzbar	$class \overline{ℤ}$
14		czzhat	$class \hat{ℤ}$
15	13 14	cun	$class (\overline{ℤ} \cup \hat{ℤ})$
16	12	cv	$setvar n$
17		cmulc	$class \cdot_{\overline{ℂ}}$
18	16 3 17	co	$class (n \cdot_{\overline{ℂ}} x)$
19	18 4	wceq	$wff n \cdot_{\overline{ℂ}} x = y$
20	19 12 15	wrex	$wff \exists n \in (\overline{ℤ} \cup \hat{ℤ}) n \cdot_{\overline{ℂ}} x = y$
21	11 20	wa	$wff (⟨x, y⟩ \in ((\overline{ℂ} \times \overline{ℂ}) \cup (\hat{ℂ} \times \hat{ℂ})) \land \exists n \in (\overline{ℤ} \cup \hat{ℤ}) n \cdot_{\overline{ℂ}} x = y)$
22	21 1 2	copab	$class \{⟨x, y⟩ \| (⟨x, y⟩ \in ((\overline{ℂ} \times \overline{ℂ}) \cup (\hat{ℂ} \times \hat{ℂ})) \land \exists n \in (\overline{ℤ} \cup \hat{ℤ}) n \cdot_{\overline{ℂ}} x = y)\}$
23	0 22	wceq	$wff ∥_{ℂ} = \{⟨x, y⟩ \| (⟨x, y⟩ \in ((\overline{ℂ} \times \overline{ℂ}) \cup (\hat{ℂ} \times \hat{ℂ})) \land \exists n \in (\overline{ℤ} \cup \hat{ℤ}) n \cdot_{\overline{ℂ}} x = y)\}$

Metamath Proof Explorer