let a1, b1 be Complex; :: thesis: ((a1 |^ 2) + (a1 * b1)) + (b1 |^ 2) = ((3 * ((a1 + b1) |^ 2)) + ((a1 - b1) |^ 2)) / 4
A1: (a1 + b1) |^ 2 = (a1 + b1) * (a1 + b1) by NEWTON:81
.= ((a1 * a1) + ((2 * a1) * b1)) + (b1 * b1)
.= ((a1 |^ 2) + ((2 * a1) * b1)) + (b1 * b1) by NEWTON:81
.= ((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2) by NEWTON:81 ;
(a1 - b1) |^ 2 = (a1 - b1) * (a1 - b1) by NEWTON:81
.= ((a1 * a1) - ((2 * a1) * b1)) + (b1 * b1)
.= ((a1 |^ 2) - ((2 * a1) * b1)) + (b1 * b1) by NEWTON:81
.= ((a1 |^ 2) - ((2 * a1) * b1)) + (b1 |^ 2) by NEWTON:81 ;
hence ((a1 |^ 2) + (a1 * b1)) + (b1 |^ 2) = ((3 * ((a1 + b1) |^ 2)) + ((a1 - b1) |^ 2)) / 4 by A1; :: thesis: verum