let a, b be odd Integer; :: thesis: for n being Nat holds 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b)
let n be Nat; :: thesis: 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b)

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b)

hence 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b) ; :: thesis: verum

end;

suppose A0: a <> b ; :: thesis: 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b)

then reconsider c = a - b as non zero Integer ;
defpred S₁[ Nat] means 2 |-count ((a |^ ((2 * $1) + 1)) - (b |^ ((2 * $1) + 1))) = 2 |-count (a - b);
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]
reconsider d = (a |^ ((2 * k) + 1)) - (b |^ ((2 * k) + 1)) as non zero Integer by A0, POW2;
B1: ( 2 |^ (2 |-count c) divides c & 2 |^ (2 |-count d) divides d ) by Def6;
reconsider x = d / (2 |^ (2 |-count d)) as odd Integer ;
consider y being Integer such that
B3: c = (2 |^ (2 |-count c)) * y by B1;
B5: (a |^ (((2 * k) + 1) + 2)) - (b |^ (((2 * k) + 1) + 2)) = ((a |^ ((2 * k) + 1)) * ((a |^ 2) - (b |^ 2))) + ((b |^ 2) * ((a |^ ((2 * k) + 1)) - (b |^ ((2 * k) + 1)))) by RI2
.= ((a |^ ((2 * k) + 1)) * ((a |^ 2) - (b |^ 2))) + ((b |^ 2) * ((2 |^ (2 |-count (a - b))) * x)) by B0, XCMPLX_1:87
.= ((a |^ ((2 * k) + 1)) * ((a + b) * ((2 |^ (2 |-count (a - b))) * y))) + (((b |^ 2) * (2 |^ (2 |-count (a - b)))) * x) by B3, NEWTON01:1
.= ((((a |^ ((2 * k) + 1)) * (a + b)) * y) + ((b |^ 2) * x)) * (2 |^ (2 |-count (a - b))) ;
B6: not 2 is trivial ;
2 |-count ((a |^ (((2 * k) + 1) + 2)) - (b |^ (((2 * k) + 1) + 2))) = (2 |-count ((((a |^ ((2 * k) + 1)) * (a + b)) * y) + ((b |^ 2) * x))) + (2 |-count (2 |^ (2 |-count (a - b)))) by B5, NAT328, INT_2:28
.= 2 |-count c by B6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A1, A2);
hence 2 |-count ((a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1))) = 2 |-count (a - b) ; :: thesis: verum

end;

end;