let a, k, m, n be Nat; ( a divides (m |^ k) + 1 implies a divides (((a * n) + m) |^ k) + 1 )
assume A1:
a divides (m |^ k) + 1
; a divides (((a * n) + m) |^ k) + 1
then A2:
a <> 0
;
then A3:
((m |^ k) + 1) mod a = 0
by A1, INT_1:62;
((a * n) + m) mod a = m mod a
by NAT_D:21;
then
(((a * n) + m) |^ k) mod a = (m |^ k) mod a
by INT_4:8;
then 0 =
(((((a * n) + m) |^ k) mod a) + (1 mod a)) mod a
by A3, NAT_D:66
.=
((((a * n) + m) |^ k) + 1) mod a
by NAT_D:66
;
hence
a divides (((a * n) + m) |^ k) + 1
by A2, INT_1:62; verum