let a be Nat; :: thesis: for b, n being non zero Nat holds (a mod b) |^ n >= (a |^ n) mod b
let b, n be non zero Nat; :: thesis: (a mod b) |^ n >= (a |^ n) mod b
reconsider m = n - 1 as Nat ;
A1: (a mod b) * ((a mod b) |^ m) = (a mod b) |^ (m + 1) by NEWTON:6;
((a mod b) * ((a mod b) |^ m)) mod b <= (a mod b) * ((a mod b) |^ m) by AMB;
hence (a mod b) |^ n >= (a |^ n) mod b by A1, GR_CY_3:30; :: thesis: verum