let a, b be odd Nat; :: thesis: for m being even Nat holds 4 divides (a |^ m) - (b |^ m)

let m be even Nat; :: thesis: 4 divides (a |^ m) - (b |^ m)

consider n being Nat such that

L0: m = 2 * n by ABIAN:def 2;

L1: ( 4 divides a + b implies 4 divides (a |^ m) - (b |^ m) )

hence 4 divides (a |^ m) - (b |^ m) by L1, Th58; :: thesis: verum

let m be even Nat; :: thesis: 4 divides (a |^ m) - (b |^ m)

consider n being Nat such that

L0: m = 2 * n by ABIAN:def 2;

L1: ( 4 divides a + b implies 4 divides (a |^ m) - (b |^ m) )

proof

( 4 divides a - b implies 4 divides (a |^ m) - (b |^ m) )
by Th64;
assume A1:
4 divides a + b
; :: thesis: 4 divides (a |^ m) - (b |^ m)

a + b divides (a |^ m) - (b |^ m) by NEWTON01:36, L0;

hence 4 divides (a |^ m) - (b |^ m) by A1, INT_2:9; :: thesis: verum

end;a + b divides (a |^ m) - (b |^ m) by NEWTON01:36, L0;

hence 4 divides (a |^ m) - (b |^ m) by A1, INT_2:9; :: thesis: verum

hence 4 divides (a |^ m) - (b |^ m) by L1, Th58; :: thesis: verum