let x, y be Integer; :: thesis: for a being non trivial Nat holds
( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
let a be non trivial Nat; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
set i = x;
set j = y;
set I = |.x.|;
set J = |.y.|;
set IJ = |.(x + y).|;
set A = (a ^2) -' 1;
set S = sqrt ((a ^2) -' 1);
A1: (a ^2) -' 1 = (a ^2) - 1 by NAT_1:14, XREAL_1:233;
A2: (sqrt ((a ^2) -' 1)) ^2 = (a ^2) -' 1 by SQUARE_1:def 2;
A3: 1 = ((a + (sqrt ((a ^2) -' 1))) * (a - (sqrt ((a ^2) -' 1)))) |^ |.x.| by A2, A1
.= ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|) by NEWTON:7 ;
A4: 1 = ((a + (sqrt ((a ^2) -' 1))) * (a - (sqrt ((a ^2) -' 1)))) |^ |.y.| by A2, A1
.= ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|) by NEWTON:7 ;
deffunc H1( Integer) -> Nat = Px (a,|.$1.|);
deffunc H2( Integer) -> set = (sgn $1) * (Py (a,|.$1.|));
per cases ( ( x >= 0 & y >= 0 ) or ( x < 0 & y >= 0 ) or ( x >= 0 & y < 0 ) or ( x < 0 & y < 0 ) ) ;
suppose A5: ( x >= 0 & y >= 0 ) ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then A6: ( x = |.x.| & y = |.y.| ) by ABSVALUE:def 1;
A7: H2(x) = Py (a,|.x.|) by Th23, A5;
A8: H2(y) = Py (a,|.y.|) by A5, Th23;
A9: |.(x + y).| = x + y by A5, ABSVALUE:def 1;
H2(x + y) = Py (a,|.(x + y).|) by Th23, A5;
then H1(x + y) + (H2(x + y) * (sqrt ((a ^2) -' 1))) = (a + (sqrt ((a ^2) -' 1))) |^ |.(x + y).| by Th11
.= ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) by A6, A9, NEWTON:8
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) by A7, Th11
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) by A8, Th11
.= ((H1(x) * H1(y)) + ((((a ^2) -' 1) * H2(x)) * H2(y))) + ((sqrt ((a ^2) -' 1)) * ((H1(x) * H2(y)) + (H2(x) * H1(y)))) by A2 ;
hence ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ) by PELLS_EQ:3; :: thesis: verum
end;
suppose A10: ( x < 0 & y >= 0 ) ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then A11: ( - x = |.x.| & y = |.y.| ) by ABSVALUE:def 1;
A12: H2(x) = - (Py (a,|.x.|)) by A10, Th24;
A13: H2(y) = Py (a,|.y.|) by A10, Th23;
per cases ( x + y >= 0 or x + y < 0 ) ;
suppose A14: x + y >= 0 ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then |.(x + y).| = x + y by ABSVALUE:def 1;
then A15: |.(x + y).| + |.x.| = |.y.| by A11;
H2(x + y) = Py (a,|.(x + y).|) by A14, Th23;
then H1(x + y) + (H2(x + y) * (sqrt ((a ^2) -' 1))) = ((a + (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * (((a + (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|)) by Th11, A3
.= (((a + (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|)) * ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|)
.= ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|) by A15, NEWTON:8
.= (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) * ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|) by A13, Th11
.= (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) * (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) by A12, Th11
.= ((H1(x) * H1(y)) + ((((a ^2) -' 1) * H2(x)) * H2(y))) + ((sqrt ((a ^2) -' 1)) * ((H1(x) * H2(y)) + (H2(x) * H1(y)))) by A2 ;
hence ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ) by PELLS_EQ:3; :: thesis: verum
end;
suppose A16: x + y < 0 ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then |.(x + y).| = - (x + y) by ABSVALUE:def 1;
then A17: |.(x + y).| + |.y.| = |.x.| by A11;
H2(x + y) = - (Py (a,|.(x + y).|)) by A16, Th24;
then H1(x + y) + (H2(x + y) * (sqrt ((a ^2) -' 1))) = ((a - (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * (((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|)) by Th11, A4
.= (((a - (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|)) * ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|)
.= ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) by A17, NEWTON:8
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) by A12, Th11
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) by A13, Th11
.= ((H1(x) * H1(y)) + ((((a ^2) -' 1) * H2(x)) * H2(y))) + ((sqrt ((a ^2) -' 1)) * ((H1(x) * H2(y)) + (H2(x) * H1(y)))) by A2 ;
hence ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ) by PELLS_EQ:3; :: thesis: verum
end;
end;
end;
suppose A18: ( x >= 0 & y < 0 ) ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then A19: ( x = |.x.| & - y = |.y.| ) by ABSVALUE:def 1;
A20: H2(x) = Py (a,|.x.|) by Th23, A18;
A21: H2(y) = - (Py (a,|.y.|)) by A18, Th24;
per cases ( x + y >= 0 or x + y < 0 ) ;
suppose A22: x + y >= 0 ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then |.(x + y).| = x + y by ABSVALUE:def 1;
then A23: |.(x + y).| + |.y.| = |.x.| by A19;
H2(x + y) = Py (a,|.(x + y).|) by A22, Th23;
then H1(x + y) + (H2(x + y) * (sqrt ((a ^2) -' 1))) = ((a + (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * (((a + (sqrt ((a ^2) -' 1))) |^ |.y.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|)) by A4, Th11
.= (((a + (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * ((a + (sqrt ((a ^2) -' 1))) |^ |.y.|)) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|)
.= ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|) by A23, NEWTON:8
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|) by A20, Th11
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) by A21, Th11
.= ((H1(x) * H1(y)) + ((((a ^2) -' 1) * H2(x)) * H2(y))) + ((sqrt ((a ^2) -' 1)) * ((H1(x) * H2(y)) + (H2(x) * H1(y)))) by A2 ;
hence ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ) by PELLS_EQ:3; :: thesis: verum
end;
suppose A24: x + y < 0 ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then |.(x + y).| = - (x + y) by ABSVALUE:def 1;
then A25: |.(x + y).| + |.x.| = |.y.| by A19;
H2(x + y) = - (Py (a,|.(x + y).|)) by A24, Th24;
then H1(x + y) + (H2(x + y) * (sqrt ((a ^2) -' 1))) = ((a - (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * (((a - (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|)) by Th11, A3
.= (((a - (sqrt ((a ^2) -' 1))) |^ |.(x + y).|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|)) * ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|)
.= ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|) * ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|) by A25, NEWTON:8
.= (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) * ((a + (sqrt ((a ^2) -' 1))) |^ |.x.|) by A21, Th11
.= (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) * (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) by A20, Th11
.= ((H1(x) * H1(y)) + ((((a ^2) -' 1) * H2(x)) * H2(y))) + ((sqrt ((a ^2) -' 1)) * ((H1(x) * H2(y)) + (H2(x) * H1(y)))) by A2 ;
hence ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ) by PELLS_EQ:3; :: thesis: verum
end;
end;
end;
suppose A26: ( x < 0 & y < 0 ) ; :: thesis: ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )
then A27: ( - x = |.x.| & - y = |.y.| ) by ABSVALUE:def 1;
A28: H2(x) = - (Py (a,|.x.|)) by A26, Th24;
A29: H2(y) = - (Py (a,|.y.|)) by A26, Th24;
A30: |.(x + y).| = - (x + y) by A26, ABSVALUE:def 1;
A31: |.(x + y).| = |.x.| + |.y.| by A27, A30;
H1(x + y) + (H2(x + y) * (sqrt ((a ^2) -' 1))) = H1(x + y) + ((- (Py (a,|.(x + y).|))) * (sqrt ((a ^2) -' 1))) by A26, Th24
.= (a - (sqrt ((a ^2) -' 1))) |^ |.(x + y).| by Th11
.= ((a - (sqrt ((a ^2) -' 1))) |^ |.x.|) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|) by A31, NEWTON:8
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * ((a - (sqrt ((a ^2) -' 1))) |^ |.y.|) by A28, Th11
.= (H1(x) + (H2(x) * (sqrt ((a ^2) -' 1)))) * (H1(y) + (H2(y) * (sqrt ((a ^2) -' 1)))) by A29, Th11
.= ((H1(x) * H1(y)) + ((((a ^2) -' 1) * H2(x)) * H2(y))) + ((sqrt ((a ^2) -' 1)) * ((H1(x) * H2(y)) + (H2(x) * H1(y)))) by A2 ;
hence ( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) ) by PELLS_EQ:3; :: thesis: verum
end;
end;