let a, b be Nat; :: thesis: ( a is odd & b is odd implies 8 divides (a |^ 2) - (b |^ 2) )

assume A0: ( a is odd & b is odd ) ; :: thesis: 8 divides (a |^ 2) - (b |^ 2)

then consider k being Nat such that

A1: a = (2 * k) + 1 by ABIAN:9;

consider n being Nat such that

A1a: b = (2 * n) + 1 by A0, ABIAN:9;

( ( k is even or k + 1 is even ) & ( n is even or n + 1 is even ) ) ;

then (k * (k + 1)) - (n * (n + 1)) is even ;

then A2: 2 * 4 divides 4 * ((k * (k + 1)) - (n * (n + 1))) by INT_6:8;

(a |^ 2) - (b |^ 2) = (((2 * k) + 1) |^ 2) - (((4 * n) * (n + 1)) + 1) by A1, A1a, Th62

.= (((4 * k) * (k + 1)) + 1) - (((4 * n) * (n + 1)) + 1) by Th62

.= 4 * ((k * (k + 1)) - (n * (n + 1))) ;

hence 8 divides (a |^ 2) - (b |^ 2) by A2; :: thesis: verum

assume A0: ( a is odd & b is odd ) ; :: thesis: 8 divides (a |^ 2) - (b |^ 2)

then consider k being Nat such that

A1: a = (2 * k) + 1 by ABIAN:9;

consider n being Nat such that

A1a: b = (2 * n) + 1 by A0, ABIAN:9;

( ( k is even or k + 1 is even ) & ( n is even or n + 1 is even ) ) ;

then (k * (k + 1)) - (n * (n + 1)) is even ;

then A2: 2 * 4 divides 4 * ((k * (k + 1)) - (n * (n + 1))) by INT_6:8;

(a |^ 2) - (b |^ 2) = (((2 * k) + 1) |^ 2) - (((4 * n) * (n + 1)) + 1) by A1, A1a, Th62

.= (((4 * k) * (k + 1)) + 1) - (((4 * n) * (n + 1)) + 1) by Th62

.= 4 * ((k * (k + 1)) - (n * (n + 1))) ;

hence 8 divides (a |^ 2) - (b |^ 2) by A2; :: thesis: verum