r,s:
. CoPrime(r,s) 
(a,b:
. 
x:. (x = a mod r) & (x = b mod s))r,s:. CoPrime(r,s) (x:. (x = 1 mod r) & (x = 0 mod s))a,b,y:. GCD(a;b;y) GCD(b;a;y)m,a,b:. a = b (a = b mod m)| Rank | Theorem | Name |
| 9 | r,s:. CoPrime(r,s) (a,b:. x:. (x = a mod r) & (x = b mod s)) | [chrem_exists] |
| cites the following: | ||
| 8 | r,s:. CoPrime(r,s) (x:. (x = 1 mod r) & (x = 0 mod s)) | [chrem_exists_aux] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |
| 1 | m,a,b:. a = b (a = b mod m) | [eqmod_weakening] |