let x, y be Integer; :: thesis: for a being non trivial Nat holds (sgn (x + y)) * (Py (a,|.(x + y).|)),(sgn (x - y)) * (Py (a,|.(x - y).|)) are_congruent_mod Px (a,|.x.|)
let a be non trivial Nat; :: thesis: (sgn (x + y)) * (Py (a,|.(x + y).|)),(sgn (x - y)) * (Py (a,|.(x - y).|)) are_congruent_mod Px (a,|.x.|)
x + y = (2 * x) + ((- x) + y) ;
then A1: (sgn (x + y)) * (Py (a,|.(x + y).|)), - ((sgn ((- x) + y)) * (Py (a,|.((- x) + y).|))) are_congruent_mod Px (a,|.x.|) by Th30;
A2: |.((- x) + y).| = |.(- ((- x) + y)).| by COMPLEX1:52;
(- x) + y = (- 1) * (x - y) ;
then ( sgn ((- x) + y) = (sgn (x - y)) * (sgn (- 1)) & sgn (- 1) = - 1 ) by ABSVALUE:18, ABSVALUE:def 2;
hence (sgn (x + y)) * (Py (a,|.(x + y).|)),(sgn (x - y)) * (Py (a,|.(x - y).|)) are_congruent_mod Px (a,|.x.|) by A2, A1; :: thesis: verum