let a, b be odd Integer; :: thesis: for m being odd Nat holds 2 |-count ((a |^ m) + (b |^ m)) = 2 |-count (a + b)
let m be odd Nat; :: thesis: 2 |-count ((a |^ m) + (b |^ m)) = 2 |-count (a + b)
reconsider c = - b as odd Integer ;
reconsider n = (m - 1) / 2 as Nat ;
2 |-count ((a |^ m) + ((- c) |^ m)) = 2 |-count ((a |^ ((2 * n) + 1)) + (- (c |^ ((2 * n) + 1)))) by POWER:2
.= 2 |-count ((a |^ ((2 * n) + 1)) - (c |^ ((2 * n) + 1)))
.= 2 |-count (a - (- b)) by Odd ;
hence 2 |-count ((a |^ m) + (b |^ m)) = 2 |-count (a + b) ; :: thesis: verum