let a, b be odd Nat; :: thesis: for m being even Nat holds 2 |-count ((a |^ m) + (b |^ m)) = 1
let m be even Nat; :: thesis: 2 |-count ((a |^ m) + (b |^ m)) = 1
A1: 4 = 2 * 2
.= 2 |^ 2 by NEWTON:81 ;
4 divides (a |^ m) - (b |^ m) by NEWTON02:65;
then A2: not 2 |^ (1 + 1) divides (a |^ m) + (b |^ m) by A1, NEWTON02:58;
(a |^ m) + (b |^ m) is even ;
then 2 |^ 1 divides (a |^ m) + (b |^ m) ;
hence 2 |-count ((a |^ m) + (b |^ m)) = 1 by A2, NAT_3:def 7; :: thesis: verum