let a, k be Nat; :: thesis: for n being positive Nat holds
( a divides k * ((a |^ n) + 1) iff a divides k )
let n be positive Nat; :: thesis: ( a divides k * ((a |^ n) + 1) iff a divides k )
consider k being Nat such that
A1: n = 1 + k by NAT_1:10, NAT_1:14;
a |^ (1 + k) = a * (a |^ k) by NEWTON:6;
hence ( a divides k * ((a |^ n) + 1) iff a divides k ) by A1, Th77; :: thesis: verum