let n be Nat; :: thesis: 3 divides Triangle (3 * n)
A0: (2 * 1) + 1 is odd ;
a1: n * ((3 * n) + 1) is even

proof

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: n * ((3 * n) + 1) is even

hence n * ((3 * n) + 1) is even ; :: thesis: verum

end;

suppose n is odd ; :: thesis: n * ((3 * n) + 1) is even

hence n * ((3 * n) + 1) is even by A0; :: thesis: verum

end;

end;

end;

Triangle (3 * n) = ((3 * n) * ((3 * n) + 1)) / 2 by NUMPOLY1:19;
then Triangle (3 * n) = 3 * ((n * ((3 * n) + 1)) / 2) ;
hence 3 divides Triangle (3 * n) by a1; :: thesis: verum