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

( 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