A1: (a |^ b) / a is integer by NEWTON02:6, NEWTON05:1;
(a |^ b) div a = [\((a |^ b) / a)/] by INT_1:def 9;
then ( a = 0 or ((a |^ b) div a) * a = a |^ b ) by A1, XCMPLX_1:87;
then ( a = 0 or (a |^ b) mod a = (a |^ b) - (a |^ b) ) by INT_1:def 10;
hence (a |^ b) mod a is zero ; :: thesis: verum