let m be non zero even Nat; :: thesis: for a, b being odd Nat st a <> b holds
2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count ((a |^ m) - (b |^ m))) + 1
let a, b be odd Nat; :: thesis: ( a <> b implies 2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count ((a |^ m) - (b |^ m))) + 1 )
assume A0: a <> b ; :: thesis: 2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count ((a |^ m) - (b |^ m))) + 1
reconsider c = (a |^ m) + (b |^ m) as non zero Nat ;
reconsider d = (a |^ m) - (b |^ m) as non zero Integer by A0, POW1;
( a |^ (2 * m) = (a |^ m) |^ 2 & b |^ (2 * m) = (b |^ m) |^ 2 ) by NEWTON:9;
then (a |^ (2 * m)) - (b |^ (2 * m)) = ((a |^ m) - (b |^ m)) * ((a |^ m) + (b |^ m)) by NEWTON01:1;
then 2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count c) + (2 |-count d) by NAT328, INT_2:28
.= (2 |-count ((a |^ m) - (b |^ m))) + 1 by SC1 ;
hence 2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count ((a |^ m) - (b |^ m))) + 1 ; :: thesis: verum