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 
|- ||C = { <. x , y >. | ( <. x , y >. e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) /\ E. n e. ( ZZbar u. ZZhat ) ( n .cc x ) = y ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdivc 
 |-  ||C
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 2 cv 
 |-  y
5 3 4 cop 
 |-  <. x , y >.
6 cccbar 
 |-  CCbar
7 6 6 cxp 
 |-  ( CCbar X. CCbar )
8 ccchat 
 |-  CChat
9 8 8 cxp 
 |-  ( CChat X. CChat )
10 7 9 cun 
 |-  ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) )
11 5 10 wcel 
 |-  <. x , y >. e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) )
12 vn 
 |-  n
13 czzbar 
 |-  ZZbar
14 czzhat 
 |-  ZZhat
15 13 14 cun 
 |-  ( ZZbar u. ZZhat )
16 12 cv 
 |-  n
17 cmulc 
 |-  .cc
18 16 3 17 co 
 |-  ( n .cc x )
19 18 4 wceq 
 |-  ( n .cc x ) = y
20 19 12 15 wrex 
 |-  E. n e. ( ZZbar u. ZZhat ) ( n .cc x ) = y
21 11 20 wa 
 |-  ( <. x , y >. e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) /\ E. n e. ( ZZbar u. ZZhat ) ( n .cc x ) = y )
22 21 1 2 copab 
 |-  { <. x , y >. | ( <. x , y >. e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) /\ E. n e. ( ZZbar u. ZZhat ) ( n .cc x ) = y ) }
23 0 22 wceq 
 |-  ||C = { <. x , y >. | ( <. x , y >. e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) /\ E. n e. ( ZZbar u. ZZhat ) ( n .cc x ) = y ) }