let a be Integer; :: thesis: for b being non zero Integer
for n being non zero Nat holds (a mod (b |^ n)) mod b = a mod b
let b be non zero Integer; :: thesis: for n being non zero Nat holds (a mod (b |^ n)) mod b = a mod b
let n be non zero Nat; :: thesis: (a mod (b |^ n)) mod b = a mod b
reconsider m = n - 1 as Nat ;
a mod (b |^ n) = a mod (b |^ (m + 1))
.= a mod (b * (b |^ m)) by NEWTON:6 ;
hence (a mod (b |^ n)) mod b = a mod b by CMI; :: thesis: verum