m,a,a',b,b':
. (a = a' mod m) 
(b = b' mod m) ((a
b) = (a'b') mod m)a,b,c:. a | b a | bca,b1,b2:. a | b1 a | b2 a | b1+b2| Theorem | Name |
| m,a,a',b,b':. (a = a' mod m) (b = b' mod m) ((ab) = (a'b') mod m) | [multiply_functionality_wrt_eqmod] |
| cites the following: | |
| a,b,c:. a | b a | bc | [divisor_of_mul] |
| a,b1,b2:. a | b1 a | b2 a | b1+b2 | [divisor_of_sum] |