Metamath Proof Explorer

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 ⊢ ∥ ℂ = x y | x y ∈ ℂ ‾ × ℂ ‾ ∪ ℂ ^ × ℂ ^ ∧ ∃ n ∈ ℤ ‾ ∪ ℤ ^ n ⋅ ℂ ‾ x = y

Detailed syntax breakdown

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 ℂ ‾
7 6 6 cxp class ℂ ‾ × ℂ ‾
8 ccchat class ℂ ^
9 8 8 cxp class ℂ ^ × ℂ ^
10 7 9 cun class ℂ ‾ × ℂ ‾ ∪ ℂ ^ × ℂ ^
11 5 10 wcel wff x y ∈ ℂ ‾ × ℂ ‾ ∪ ℂ ^ × ℂ ^
12 vn setvar n
13 czzbar class ℤ ‾
14 czzhat class ℤ ^
15 13 14 cun class ℤ ‾ ∪ ℤ ^
16 12 cv setvar n
17 cmulc class ⋅ ℂ ‾
18 16 3 17 co class n ⋅ ℂ ‾ x
19 18 4 wceq wff n ⋅ ℂ ‾ x = y
20 19 12 15 wrex wff ∃ n ∈ ℤ ‾ ∪ ℤ ^ n ⋅ ℂ ‾ x = y
21 11 20 wa wff x y ∈ ℂ ‾ × ℂ ‾ ∪ ℂ ^ × ℂ ^ ∧ ∃ n ∈ ℤ ‾ ∪ ℤ ^ n ⋅ ℂ ‾ x = y
22 21 1 2 copab class x y | x y ∈ ℂ ‾ × ℂ ‾ ∪ ℂ ^ × ℂ ^ ∧ ∃ n ∈ ℤ ‾ ∪ ℤ ^ n ⋅ ℂ ‾ x = y
23 0 22 wceq wff ∥ ℂ = x y | x y ∈ ℂ ‾ × ℂ ‾ ∪ ℂ ^ × ℂ ^ ∧ ∃ n ∈ ℤ ‾ ∪ ℤ ^ n ⋅ ℂ ‾ x = y