r:
, s:{s':| CoPrime(r,s') }. 
x:
. ((x = 1 mod r) & (x = 0 mod s))a,b:. CoPrime(a,b) 
(x,y:. a
x+by = 1)a:. a | aa,b,c:. a | b 
a | bca,b:. a | b a | -b| Rank | Theorem | Name |
| 8 | r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s)) | [chrem_exists_aux_a] |
| cites the following: | ||
| 7 | a,b:. CoPrime(a,b) (x,y:. ax+by = 1) | [coprime_bezout_id] |
| 0 | a:. a | a | [divides_reflexivity] |
| 0 | a,b,c:. a | b a | bc | [divisor_of_mul] |
| 0 | a,b:. a | b a | -b | [divisor_of_minus] |