let a be non trivial Nat; :: thesis: for x, y being Integer holds Px (a,|.((2 * x) + y).|), - (Px (a,|.y.|)) are_congruent_mod Px (a,|.x.|)
let x, y be Integer; :: thesis: Px (a,|.((2 * x) + y).|), - (Px (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 Px (a,|.((2 * x) + y).|) = ((Px (a,|.x.|)) * (Px (a,|.(x + y).|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn (x + y))) * (Py (a,|.(x + y).|))) by HILB10_1:22;
then (Px (a,|.x.|)) * (Px (a,|.(x + y).|)) = (Px (a,|.((2 * x) + y).|)) - ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn (x + y))) * (Py (a,|.(x + y).|))) ;
then A1: Px (a,|.((2 * x) + y).|),(((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn (x + y))) * (Py (a,|.(x + y).|)) are_congruent_mod Px (a,|.x.|) by INT_1:def 5;
(sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) by HILB10_1:22;
then (Px (a,|.x.|)) * ((sgn y) * (Py (a,|.y.|))) = ((sgn (x + y)) * (Py (a,|.(x + y).|))) - (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ;
then (sgn (x + y)) * (Py (a,|.(x + y).|)),((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by INT_1:def 5;
then A2: ((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * ((sgn (x + y)) * (Py (a,|.(x + y).|))),((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) are_congruent_mod Px (a,|.x.|) by INT_4:11;
A3: ((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) = (((a ^2) -' 1) * ((Py (a,|.x.|)) * (Py (a,|.x.|)))) * (Px (a,|.y.|))

proof

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: ((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) = (((a ^2) -' 1) * ((Py (a,|.x.|)) * (Py (a,|.x.|)))) * (Px (a,|.y.|))

then ( sgn x = 0 & Py (a,|.x.|) = 0 ) by ABSVALUE:def 2, HILB10_1:3;
hence ((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) = (((a ^2) -' 1) * ((Py (a,|.x.|)) * (Py (a,|.x.|)))) * (Px (a,|.y.|)) ; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: ((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) = (((a ^2) -' 1) * ((Py (a,|.x.|)) * (Py (a,|.x.|)))) * (Px (a,|.y.|))

then A4: ( (sgn x) * (sgn x) = sgn (x * x) & x * x > 0 ) by ABSVALUE:18;
((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) = (((((a ^2) -' 1) * ((sgn x) * (sgn x))) * (Py (a,|.x.|))) * (Py (a,|.x.|))) * (Px (a,|.y.|))
.= (((((a ^2) -' 1) * 1) * (Py (a,|.x.|))) * (Py (a,|.x.|))) * (Px (a,|.y.|)) by A4, ABSVALUE:def 2
.= ((((a ^2) -' 1) * 1) * ((Py (a,|.x.|)) * (Py (a,|.x.|)))) * (Px (a,|.y.|)) ;
hence ((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) = (((a ^2) -' 1) * ((Py (a,|.x.|)) * (Py (a,|.x.|)))) * (Px (a,|.y.|)) ; :: thesis: verum

end;

end;

end;

A5: (Py (a,|.x.|)) ^2 = (Py (a,|.x.|)) * (Py (a,|.x.|)) by SQUARE_1:def 1;
A6: (Px (a,|.x.|)) ^2 = (Px (a,|.x.|)) * (Px (a,|.x.|)) by SQUARE_1:def 1;
((Px (a,|.x.|)) ^2) - (((a ^2) -' 1) * ((Py (a,|.x.|)) ^2)) = 1 by HILB10_1:7;
then A7: Px (a,|.((2 * x) + y).|),(((Px (a,|.x.|)) ^2) - 1) * (Px (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by A5, A3, A2, A1, INT_1:15;
(Px (a,|.x.|)) * ((Px (a,|.x.|)) * (Px (a,|.y.|))) = ((((Px (a,|.x.|)) ^2) - 1) * (Px (a,|.y.|))) - (- (Px (a,|.y.|))) by A6;
then (((Px (a,|.x.|)) ^2) - 1) * (Px (a,|.y.|)), - (Px (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by INT_1:def 5;
hence Px (a,|.((2 * x) + y).|), - (Px (a,|.y.|)) are_congruent_mod Px (a,|.x.|) by A7, INT_1:15; :: thesis: verum