let b, c, m, l be Nat; :: thesis: for a, n being positive Nat holds
( a divides (b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l)) iff a divides b + c )
let a, n be positive Nat; :: thesis: ( a divides (b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l)) iff a divides b + c )
( ((b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l))) mod a = 0 iff (b + c) mod a = 0 ) by Th83;
hence ( a divides (b * (((a |^ n) + 1) |^ m)) + (c * (((a |^ n) + 1) |^ l)) iff a divides b + c ) by PEPIN:6; :: thesis: verum