theorem Th29: :: NUMBER03:29

for a, b, m being Nat st 1 < m holds
( m divides (a |^ b) + 1 iff m divides ((a mod m) |^ b) + 1 )