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

per cases ( a > 1 or a = 1 or a = 0 ) by NAT_1:25;

suppose C1: a > 1 ; :: thesis: (k * (((a |^ n) + 1) |^ m)) mod a = k mod a

(((a |^ n) + 1) |^ m) mod a = ((((a |^ n) + 1) mod a) |^ m) mod a by GR_CY_3:30;
then (k * (((a |^ n) + 1) |^ m)) mod a = (k * ((((1 * ((a |^ n) + 1)) mod a) |^ m) mod a)) mod a by RADIX_2:3
.= (k * (((1 mod a) |^ m) mod a)) mod a by Th81
.= (k * ((1 |^ m) mod a)) mod a by C1, NAT_D:14
.= (k * 1) mod a by RADIX_2:3 ;
hence (k * (((a |^ n) + 1) |^ m)) mod a = k mod a ; :: thesis: verum

end;

suppose a = 1 ; :: thesis: (k * (((a |^ n) + 1) |^ m)) mod a = k mod a

then ( (k * (((a |^ n) + 1) |^ m)) mod a = 0 & k mod a = 0 ) by RADIX_2:1;
hence (k * (((a |^ n) + 1) |^ m)) mod a = k mod a ; :: thesis: verum

end;

suppose a = 0 ; :: thesis: (k * (((a |^ n) + 1) |^ m)) mod a = k mod a

hence (k * (((a |^ n) + 1) |^ m)) mod a = k mod a ; :: thesis: verum

end;

end;