k:
, i:{2..k
}, j:
. i
j = k 
2 
j < k & i<ka,b:. ab>0 
a>0 & b>0 
a<0 & b<0i,j:{2...}. i<ij & j<ij| Rank | Theorem | Name |
| 4 | k:, i:{2..k}, j:. ij = k 2 j < k & i<k | [factors_smaller2] |
| cites the following: | ||
| 3 | a,b:. ab>0 a>0 & b>0 a<0 & b<0 | [pos_mul_arg_bounds] |
| 3 | i,j:{2...}. i<ij & j<ij | [factors_smaller] |