let a, b be odd Integer; ( |.a.| <> |.b.| implies ( 2 |-count ((a - b) |^ 2) <> 2 |-count ((a + b) |^ 2) & 2 |-count ((a - b) |^ 2) <> (2 |-count (a |^ 2)) - (b |^ 2) ) )
assume A1:
|.a.| <> |.b.|
; ( 2 |-count ((a - b) |^ 2) <> 2 |-count ((a + b) |^ 2) & 2 |-count ((a - b) |^ 2) <> (2 |-count (a |^ 2)) - (b |^ 2) )
A1a:
a - b <> a - a
by A1;
reconsider c = a - b as non zero Integer by A1;
reconsider d = a + b as non zero Integer by A1, ABS1;
A2: 2 |-count ((a - b) |^ 2) =
2 |-count (c |^ 2)
.=
2 * (2 |-count (a - b))
by NAT332, INT_2:28
;
A3: 2 |-count ((a + b) |^ 2) =
2 |-count (d |^ 2)
.=
2 * (2 |-count (a + b))
by NAT332, INT_2:28
;
2 * 2 = 2 |^ 2
by NEWTON:81;
then A6:
( ( 2 |^ 2 divides a - b & not 2 |^ 2 divides a + b ) or ( 2 |^ 2 divides a + b & not 2 |^ 2 divides a - b ) )
by NEWTON0258;
( a + b <> 0 & not 2 is trivial )
by A1, ABS1;
hence
( 2 |-count ((a - b) |^ 2) <> 2 |-count ((a + b) |^ 2) & 2 |-count ((a - b) |^ 2) <> (2 |-count (a |^ 2)) - (b |^ 2) )
by A2, A3, A6, A1a, DIC; verum