let a, b be odd Integer; :: thesis: Parity (a + b) <> Parity (a - b)

per cases ( a + b is zero or a - b is zero or ( a + b <> 0 & a - b <> 0 ) ) ;

suppose B1: a + b is zero ; :: thesis: Parity (a + b) <> Parity (a - b)

then Parity (a - b) = Parity (2 * a)
.= (Parity 2) * (Parity a) by ILP ;
hence Parity (a + b) <> Parity (a - b) by B1, Def1; :: thesis: verum

end;

suppose B1: a - b is zero ; :: thesis: Parity (a + b) <> Parity (a - b)

then Parity (a + b) = Parity (2 * a)
.= (Parity 2) * (Parity a) by ILP ;
hence Parity (a + b) <> Parity (a - b) by B1, Def1; :: thesis: verum

end;

suppose B0: ( a + b <> 0 & a - b <> 0 ) ; :: thesis: Parity (a + b) <> Parity (a - b)

then B1: ( 2 |^ (2 |-count (a + b)) = Parity (a + b) & 2 |^ (2 |-count (a - b)) = Parity (a - b) ) by Def1;
2 * 2 = 2 |^ 2 by NEWTON:81;
then B2: ( 2 |^ 2 divides a + b iff not 2 |^ 2 divides a - b ) by NEWTON03:73;
not 2 is trivial ;
then ( 2 |-count (a + b) >= 2 iff 2 |-count (a - b) < 2 ) by B0, B2, NEWTON03:59;

per cases then ( 2 |-count (a + b) > 2 |-count (a - b) or 2 |-count (a + b) < 2 |-count (a - b) ) by XXREAL_0:1;

suppose 2 |-count (a + b) > 2 |-count (a - b) ; :: thesis: Parity (a + b) <> Parity (a - b)

hence Parity (a + b) <> Parity (a - b) by B1, PEPIN:66; :: thesis: verum

end;

suppose 2 |-count (a + b) < 2 |-count (a - b) ; :: thesis: Parity (a + b) <> Parity (a - b)

hence Parity (a + b) <> Parity (a - b) by B1, PEPIN:66; :: thesis: verum

end;

end;

end;

end;