let x, y be Integer; 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; ( 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 )
;
( 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;
verum end; suppose A10:
(
x < 0 &
y >= 0 )
;
( 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
;
( 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;
verum end; suppose A16:
x + y < 0
;
( 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;
verum end; end; suppose A18:
(
x >= 0 &
y < 0 )
;
( 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
;
( 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;
verum end; suppose A24:
x + y < 0
;
( 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;
verum end; end; suppose A26:
(
x < 0 &
y < 0 )
;
( 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;
verum end;