let m be Nat; :: thesis: for t being Integer
for a1, b1 being Complex st (a1 |^ m) - (b1 |^ m) = (a1 - b1) * t holds
(a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2
let t be Integer; :: thesis: for a1, b1 being Complex st (a1 |^ m) - (b1 |^ m) = (a1 - b1) * t holds
(a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2
let a1, b1 be Complex; :: thesis: ( (a1 |^ m) - (b1 |^ m) = (a1 - b1) * t implies (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2 )
assume (a1 |^ m) - (b1 |^ m) = (a1 - b1) * t ; :: thesis: (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2
then (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 - b1) * t))) / 2 by Th13;
hence (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((a1 - b1) * (((t * (a1 + b1)) + (a1 |^ m)) + (b1 |^ m))) / 2 ; :: thesis: verum