let i be Nat; :: thesis: not 3 divides (ArProg (2,3)) . i
assume 3 divides (ArProg (2,3)) . i ; :: thesis: contradiction
then A1: 3 divides 2 + (3 * i) by ArDefNth;
3 divides 3 * i ;
then 3 divides (2 + (3 * i)) - (3 * i) by A1, PREPOWER:94;
hence contradiction by INT_2:28; :: thesis: verum