let n be Nat; :: thesis: for c1 being Complex holds ((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) = c1 |^ (n + 1)
let c1 be Complex; :: thesis: ((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) = c1 |^ (n + 1)
set k = ((c1 |^ n) / 2) + (c1 / 2);
set l = ((c1 |^ n) / 2) - (c1 / 2);
((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) = ((((c1 |^ n) / 2) + (c1 / 2)) * (((c1 |^ n) / 2) + (c1 / 2))) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) by NEWTON:81
.= ((((c1 |^ n) / 2) + (c1 / 2)) * (((c1 |^ n) / 2) + (c1 / 2))) - ((((c1 |^ n) / 2) - (c1 / 2)) * (((c1 |^ n) / 2) - (c1 / 2))) by NEWTON:81
.= c1 * (c1 |^ n)
.= c1 |^ (n + 1) by NEWTON:6 ;
hence ((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) = c1 |^ (n + 1) ; :: thesis: verum