let x, y be Integer; :: thesis: for a being non trivial Nat holds (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)), - ((sgn y) * (Py (a,|.y.|))) are_congruent_mod Px (a,|.x.|)
let a be non trivial Nat; :: thesis: (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)), - ((sgn y) * (Py (a,|.y.|))) are_congruent_mod Px (a,|.x.|)
set i = x;
set j = y;
set A = (a ^2) -' 1;
(2 * x) + y = x + (x + y) ;
then (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)) = (((Px (a,|.x.|)) * (sgn (x + y))) * (Py (a,|.(x + y).|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.(x + y).|))) by Th25;
then ((sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|))) - (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.(x + y).|))) = (Px (a,|.x.|)) * ((sgn (x + y)) * (Py (a,|.(x + y).|))) ;
then A1: (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)),((sgn x) * (Py (a,|.x.|))) * (Px (a,|.(x + y).|)) are_congruent_mod Px (a,|.x.|) by INT_1:def 5;
A2: ((sgn x) * (Py (a,|.x.|))) * ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) = ((((((sgn x) * (sgn x)) * (Py (a,|.x.|))) * ((a ^2) -' 1)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))
.= ((((Py (a,|.x.|)) * ((a ^2) -' 1)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|)) by Lm6 ;
A3: ((Px (a,|.x.|)) ^2) - (((a ^2) -' 1) * ((Py (a,|.x.|)) ^2)) = 1 by Th10;
Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) by Th25;
then (Px (a,|.(x + y).|)) - ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) = (Px (a,|.x.|)) * (Px (a,|.y.|)) ;
then Px (a,|.(x + y).|),(((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by INT_1:def 5;
then ((sgn x) * (Py (a,|.x.|))) * (Px (a,|.(x + y).|)),((((Py (a,|.x.|)) * ((a ^2) -' 1)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by A2, INT_4:11;
then A4: (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)),((((Px (a,|.x.|)) ^2) - 1) * (sgn y)) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by A3, A1, INT_1:15;
(((((Px (a,|.x.|)) ^2) - 1) * (sgn y)) * (Py (a,|.y.|))) - (- ((sgn y) * (Py (a,|.y.|)))) = (Px (a,|.x.|)) * (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) ;
then ((((Px (a,|.x.|)) ^2) - 1) * (sgn y)) * (Py (a,|.y.|)), - ((sgn y) * (Py (a,|.y.|))) are_congruent_mod Px (a,|.x.|) by INT_1:def 5;
hence (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)), - ((sgn y) * (Py (a,|.y.|))) are_congruent_mod Px (a,|.x.|) by A4, INT_1:15; :: thesis: verum