let a, b be Nat; :: thesis: ( b |^ 2 = a * (a - b) implies ( 3 divides a & 3 divides b ) )
assume b |^ 2 = a * (a - b) ; :: thesis: ( 3 divides a & 3 divides b )
then 0 = ((b |^ 2) - (a * a)) + (a * b)
.= ((b |^ 2) - (a |^ 2)) + (a * b) by NEWTON:81
.= ((b - a) * (b + a)) + (a * b) by NEWTON01:1 ;
then 3 divides ((b - a) * (b + a)) + (a * b) by INT_2:12;
hence ( 3 divides a & 3 divides b ) by Th51; :: thesis: verum