let a, b, m be Nat; :: thesis: ( 1 < m implies ( m divides (a |^ b) + 1 iff m divides ((a mod m) |^ b) + 1 ) )
set r = a mod m;
assume A1: 1 < m ; :: thesis: ( m divides (a |^ b) + 1 iff m divides ((a mod m) |^ b) + 1 )
then A2: 1 mod m = 1 by NAT_D:24;
A3: (((- 1) mod m) + (1 mod m)) mod m = ((- 1) + 1) mod m by NAT_D:66
.= 0 ;
thus ( m divides (a |^ b) + 1 implies m divides ((a mod m) |^ b) + 1 ) :: thesis: ( m divides ((a mod m) |^ b) + 1 implies m divides (a |^ b) + 1 )

proof

assume A4: m divides (a |^ b) + 1 ; :: thesis: m divides ((a mod m) |^ b) + 1
set k = a div m;
((a |^ b) + 1) mod m = 0 by A1, A4, INT_1:62;
then A5: (((a |^ b) + 1) - 1) mod m = (0 - 1) mod m by A2, INT_6:7;
A6: a = (m * (a div m)) + (a mod m) by A1, NAT_D:2;
A7: (m * (a div m)) mod m = 0 by NAT_D:13;
for n being Nat holds (((m * (a div m)) + (a mod m)) |^ n) mod m = ((((m * (a div m)) mod m) + ((a mod m) mod m)) |^ n) mod m by Th28;
then (a |^ b) mod m = (((a mod m) mod m) |^ b) mod m by A6, A7;
then (((a mod m) |^ b) + 1) mod m = 0 by A3, A5, NAT_D:66;
hence m divides ((a mod m) |^ b) + 1 by A1, INT_1:62; :: thesis: verum

end;

assume m divides ((a mod m) |^ b) + 1 ; :: thesis: m divides (a |^ b) + 1
then (((a mod m) |^ b) + 1) mod m = 0 by A1, INT_1:62;
then A8: ((((a mod m) |^ b) + 1) - 1) mod m = (0 - 1) mod m by A2, INT_6:7;
(a |^ b) mod m = ((a mod m) |^ b) mod m by PEPIN:12;
then ((a |^ b) + 1) mod m = 0 by A3, A8, NAT_D:66;
hence m divides (a |^ b) + 1 by A1, INT_1:62; :: thesis: verum