B2: 2 |^ 2 = 2 * 2 by NEWTON:81;
A1: 4 divides (a |^ (2 * n)) - (b |^ (2 * n)) by Th65;
A2: 4 divides ((a |^ (2 * n)) - (b |^ (2 * n))) * (((a |^ 1) - (b |^ 1)) / 2) by Th65, INT_2:2;
consider l being Nat such that
A3: ( l = ((a |^ (2 * n)) + (b |^ (2 * n))) / 2 & l is odd ) by A1, Th58, Lm63;
A4: (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) = ((((a |^ (2 * n)) + (b |^ (2 * n))) * ((a |^ 1) + (b |^ 1))) + (((a |^ (2 * n)) - (b |^ (2 * n))) * ((a |^ 1) - (b |^ 1)))) / 2 by NEWTON01:8
.= ((((a |^ (2 * n)) + (b |^ (2 * n))) * ((a |^ 1) + (b |^ 1))) / 2) + ((((a |^ (2 * n)) - (b |^ (2 * n))) * ((a |^ 1) - (b |^ 1))) / 2) ;
assume 4 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) ; :: thesis: 4 divides a + b
then 2 |^ 2 divides (((a |^ (2 * n)) + (b |^ (2 * n))) / 2) * ((a |^ 1) + (b |^ 1)) by B2, A2, A4, INT_2:1;
hence 4 divides a + b by B2, A3, Th67; :: thesis: verum