theorem Th74: :: NUMBER15:74
for n being positive Integer holds
( ( n <= 7 or n in {9,10,12,15} ) iff for x, y being positive Integer holds not (3 * x) + (5 * y) = n )