r,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,b:. a | b a | -ba:. a | aa,b,c:. a | b a | bc| Rank | Theorem | Name |
| 8 | r,s:. CoPrime(r,s) (x:. (x = 1 mod r) & (x = 0 mod s)) | [chrem_exists_aux] |
| cites the following: | ||
| 7 | a,b:. CoPrime(a,b) (x,y:. ax+by = 1) | [coprime_bezout_id] |
| 0 | a,b:. a | b a | -b | [divisor_of_minus] |
| 0 | a:. a | a | [divides_reflexivity] |
| 0 | a,b,c:. a | b a | bc | [divisor_of_mul] |