let a, k be Nat; :: thesis: for n being positive Nat holds (k * ((a |^ n) + 1)) mod a = k mod a

let n be positive Nat; :: thesis: (k * ((a |^ n) + 1)) mod a = k mod a

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 (k * ((a |^ n) + 1)) mod a = k mod a by A1, Th80; :: thesis: verum

let n be positive Nat; :: thesis: (k * ((a |^ n) + 1)) mod a = k mod a

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 (k * ((a |^ n) + 1)) mod a = k mod a by A1, Th80; :: thesis: verum