let n be Nat; :: thesis: for a1, b1, c1 being Complex st (a1 + b1) |^ (n + 1) = ((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1) holds
(a1 + b1) |^ (n + 2) = ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1))))
let a1, b1, c1 be Complex; :: thesis: ( (a1 + b1) |^ (n + 1) = ((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1) implies (a1 + b1) |^ (n + 2) = ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1)))) )
assume (a1 + b1) |^ (n + 1) = ((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1) ; :: thesis: (a1 + b1) |^ (n + 2) = ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1))))
then (a1 + b1) |^ ((n + 1) + 1) = (a1 + b1) * (((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1)) by NEWTON:6
.= ((((a1 * (a1 |^ (n + 1))) + (b1 * (a1 |^ (n + 1)))) + (a1 * (b1 |^ (n + 1)))) + (b1 * (b1 |^ (n + 1)))) + ((((a1 + b1) * a1) * b1) * c1)
.= ((((a1 |^ ((n + 1) + 1)) + (b1 * (a1 |^ (n + 1)))) + (a1 * (b1 |^ (n + 1)))) + (b1 * (b1 |^ (n + 1)))) + ((a1 * b1) * (c1 * (a1 + b1))) by NEWTON:6
.= ((((a1 |^ (n + 2)) + (b1 * (a1 * (a1 |^ n)))) + (a1 * (b1 |^ (n + 1)))) + (b1 * (b1 |^ (n + 1)))) + (((a1 * b1) * c1) * (a1 + b1)) by NEWTON:6
.= ((((a1 |^ (n + 2)) + ((b1 * a1) * (a1 |^ n))) + (a1 * (b1 * (b1 |^ n)))) + (b1 * (b1 |^ (n + 1)))) + (((a1 * b1) * c1) * (a1 + b1)) by NEWTON:6
.= ((((a1 |^ (n + 2)) + ((b1 * a1) * (a1 |^ n))) + ((a1 * b1) * (b1 |^ n))) + (b1 |^ ((n + 1) + 1))) + ((a1 * b1) * ((c1 * a1) + (c1 * b1))) by NEWTON:6
.= ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1)))) ;
hence (a1 + b1) |^ (n + 2) = ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1)))) ; :: thesis: verum