let a, b, c, m, l be Nat; :: thesis: for n being positive Nat holds ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = (b + c) mod a
let n be positive Nat; :: thesis: ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = (b + c) mod a
A1: ( (b * (((a |^ n) + 1) |^ m)) mod a = b mod a & (c * (((a |^ n) + 1) |^ l)) mod a = c mod a ) by Th82;
((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = ((b mod a) + (c mod a)) mod a by A1, NAT_D:66
.= (b + c) mod a by NAT_D:66 ;
hence ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = (b + c) mod a ; :: thesis: verum