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 |^ (2 * m)) - (b |^ (2 * m)) as non zero Integer by A0, POW1;
reconsider d = (a |^ m) - (b |^ m) as non zero Integer by A0, POW1;
A1: not 2 is trivial ;
( 2 |^ (2 |-count d) divides d & not 2 |^ ((2 |-count d) + 1) divides d ) by Def6;
then 2 |^ ((2 |-count d) + 1) divides c by Even;
hence 2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) >= (2 |-count ((a |^ m) - (b |^ m))) + 1 by A1, Count1; :: thesis: verum