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