let m be Nat; :: thesis: for a1, b1 being Complex holds (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))
let a1, b1 be Complex; :: thesis: (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))
(((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m))) = (((((a1 |^ (m + 1)) * a1) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - ((b1 |^ (m + 1)) * b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m)))
.= ((((a1 |^ ((m + 1) + 1)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - ((b1 |^ (m + 1)) * b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m))) by NEWTON:6
.= ((((a1 |^ (m + 2)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - (b1 |^ ((m + 1) + 1))) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m))) by NEWTON:6
.= (((((a1 |^ (m + 2)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - (b1 |^ (m + 2))) + (b1 * (a1 * (a1 |^ m)))) - ((a1 * b1) * (b1 |^ m))
.= (((((a1 |^ (m + 2)) + ((b1 |^ (m + 1)) * a1)) - ((a1 |^ (m + 1)) * b1)) - (b1 |^ (m + 2))) + (b1 * (a1 |^ (m + 1)))) - (a1 * (b1 * (b1 |^ m))) by NEWTON:6
.= (((a1 |^ (m + 2)) + ((b1 |^ (m + 1)) * a1)) - (b1 |^ (m + 2))) - (a1 * (b1 |^ (m + 1))) by NEWTON:6 ;
hence (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m))) ; :: thesis: verum