let m, n be Nat; for a, b being odd Nat st 2 |^ m divides (a |^ n) - (b |^ n) holds
2 |^ (m + 1) divides (a |^ (2 * n)) - (b |^ (2 * n))
let a, b be odd Nat; ( 2 |^ m divides (a |^ n) - (b |^ n) implies 2 |^ (m + 1) divides (a |^ (2 * n)) - (b |^ (2 * n)) )
A0:
( a |^ (2 * n) = (a |^ n) |^ 2 & b |^ (2 * n) = (b |^ n) |^ 2 )
by NEWTON:9;
assume A1:
2 |^ m divides (a |^ n) - (b |^ n)
; 2 |^ (m + 1) divides (a |^ (2 * n)) - (b |^ (2 * n))
A2:
2 divides (a |^ n) + (b |^ n)
by ABIAN:def 1;
(a |^ (2 * n)) - (b |^ (2 * n)) = ((a |^ n) - (b |^ n)) * ((a |^ n) + (b |^ n))
by A0, NEWTON01:1;
then
2 * (2 |^ m) divides (a |^ (2 * n)) - (b |^ (2 * n))
by A1, A2, NEWTON02:2;
hence
2 |^ (m + 1) divides (a |^ (2 * n)) - (b |^ (2 * n))
by NEWTON:6; verum