let a be Integer; :: thesis: for b being non zero Nat
for k, l being Nat holds a mod (b |^ (k + l)) = (a mod (b |^ k)) + (((a div (b |^ k)) mod (b |^ l)) * (b |^ k))
let b be non zero Nat; :: thesis: for k, l being Nat holds a mod (b |^ (k + l)) = (a mod (b |^ k)) + (((a div (b |^ k)) mod (b |^ l)) * (b |^ k))
let k, l be Nat; :: thesis: a mod (b |^ (k + l)) = (a mod (b |^ k)) + (((a div (b |^ k)) mod (b |^ l)) * (b |^ k))
b |^ (k + l) = (b |^ k) * (b |^ l) by NEWTON:8;
hence a mod (b |^ (k + l)) = (a mod (b |^ k)) + (((a div (b |^ k)) mod (b |^ l)) * (b |^ k)) by ABC; :: thesis: verum