let p be odd prime Nat; for x1, x2, x3, x4, h being Nat st 1 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) holds
ex y1, y2, y3, y4 being Integer ex r being Nat st
( 0 < r & r < h & r * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) )
let x1, x2, x3, x4, h be Nat; ( 1 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) implies ex y1, y2, y3, y4 being Integer ex r being Nat st
( 0 < r & r < h & r * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) ) )
assume that
A1:
1 < h
and
A2:
h < p
and
A3:
h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
; ex y1, y2, y3, y4 being Integer ex r being Nat st
( 0 < r & r < h & r * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) )
set h1 = h;
consider y1 being Integer such that
A4:
x1 mod h = y1 mod h
and
A5:
- h < 2 * y1
and
A6:
2 * y1 <= h
and
A7:
(x1 ^2) mod h = (y1 ^2) mod h
by A1, Them2;
consider y2 being Integer such that
A8:
x2 mod h = y2 mod h
and
A9:
- h < 2 * y2
and
A10:
2 * y2 <= h
and
A11:
(x2 ^2) mod h = (y2 ^2) mod h
by A1, Them2;
consider y3 being Integer such that
A12:
x3 mod h = y3 mod h
and
A13:
- h < 2 * y3
and
A14:
2 * y3 <= h
and
A15:
(x3 ^2) mod h = (y3 ^2) mod h
by A1, Them2;
consider y4 being Integer such that
A16:
x4 mod h = y4 mod h
and
A17:
- h < 2 * y4
and
A18:
2 * y4 <= h
and
A19:
(x4 ^2) mod h = (y4 ^2) mod h
by A1, Them2;
A20: ((x1 ^2) + (x2 ^2)) mod h =
(((x1 ^2) mod h) + ((x2 ^2) mod h)) mod h
by NAT_D:66
.=
((y1 ^2) + (y2 ^2)) mod h
by NAT_D:66, A11, A7
;
A21: ((x3 ^2) + (x4 ^2)) mod h =
(((x3 ^2) mod h) + ((x4 ^2) mod h)) mod h
by NAT_D:66
.=
((y3 ^2) + (y4 ^2)) mod h
by NAT_D:66, A19, A15
;
0 =
(((x1 ^2) + (x2 ^2)) + ((x3 ^2) + (x4 ^2))) mod h
by A3, NAT_D:13
.=
((((x1 ^2) + (x2 ^2)) mod h) + (((x3 ^2) + (x4 ^2)) mod h)) mod h
by NAT_D:66
.=
(((y1 ^2) + (y2 ^2)) + ((y3 ^2) + (y4 ^2))) mod h
by NAT_D:66, A21, A20
.=
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) mod h
;
then A22:
0 = ((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) - ((((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h) * h)
by A1, INT_1:def 10;
set r = ((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h;
set z1 = (((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4);
set z2 = (((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3);
set z3 = (((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2);
set z4 = (((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1);
A25: (((((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2) + (((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2)) + (((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2)) + (((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^2) =
((((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)) * ((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2))
.=
(h * p) * ((((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h) * h)
by A22, A3
.=
(p * (h ^2)) * (((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h)
;
A26: (x1 ^2) mod h =
((x1 mod h) * (x1 mod h)) mod h
by NAT_D:67
.=
(x1 * y1) mod h
by NAT_D:67, A4
;
A27: (x2 ^2) mod h =
((x2 mod h) * (x2 mod h)) mod h
by NAT_D:67
.=
(x2 * y2) mod h
by NAT_D:67, A8
;
A28: (x3 ^2) mod h =
((x3 mod h) * (x3 mod h)) mod h
by NAT_D:67
.=
(x3 * y3) mod h
by NAT_D:67, A12
;
A29: (x4 ^2) mod h =
((x4 mod h) * (x4 mod h)) mod h
by NAT_D:67
.=
(x4 * y4) mod h
by NAT_D:67, A16
;
A30: ((x1 * y1) + (x2 * y2)) mod h =
(((x1 * y1) mod h) + ((x2 * y2) mod h)) mod h
by NAT_D:66
.=
((x1 ^2) + (x2 ^2)) mod h
by NAT_D:66, A27, A26
;
A31: ((x3 * y3) + (x4 * y4)) mod h =
(((x3 * y3) mod h) + ((x4 * y4) mod h)) mod h
by NAT_D:66
.=
((x3 ^2) + (x4 ^2)) mod h
by NAT_D:66, A29, A28
;
A32: ((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) mod h =
(((x1 * y1) + (x2 * y2)) + ((x3 * y3) + (x4 * y4))) mod h
.=
((((x1 * y1) + (x2 * y2)) mod h) + (((x3 * y3) + (x4 * y4)) mod h)) mod h
by NAT_D:66
.=
(((x1 ^2) + (x2 ^2)) + ((x3 ^2) + (x4 ^2))) mod h
by NAT_D:66, A31, A30
.=
0
by NAT_D:13, A3
;
A33: (x1 * y2) mod h =
((x1 mod h) * (y2 mod h)) mod h
by NAT_D:67
.=
(x1 * x2) mod h
by NAT_D:67, A8
;
A34: (x2 * y1) mod h =
((x2 mod h) * (y1 mod h)) mod h
by NAT_D:67
.=
(x2 * x1) mod h
by NAT_D:67, A4
;
A35: (x3 * y4) mod h =
((x3 mod h) * (y4 mod h)) mod h
by NAT_D:67
.=
(x3 * x4) mod h
by NAT_D:67, A16
;
A36: (x4 * y3) mod h =
((x4 mod h) * (y3 mod h)) mod h
by NAT_D:67
.=
(x4 * x3) mod h
by NAT_D:67, A12
;
A37: ((- (x1 * y2)) + (x2 * y1)) mod h =
((x2 * y1) - (x1 * y2)) mod h
.=
(((x2 * y1) mod h) - ((x1 * y2) mod h)) mod h
by INT_6:7
.=
0
by NAT_D:26, A33, A34
;
A38: ((- (x3 * y4)) + (x4 * y3)) mod h =
((x4 * y3) - (x3 * y4)) mod h
.=
(((x4 * x3) mod h) - ((x3 * x4) mod h)) mod h
by A35, A36, INT_6:7
.=
0
by NAT_D:26
;
A39: ((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) mod h =
(((- (x1 * y2)) + (x2 * y1)) + ((- (x3 * y4)) + (x4 * y3))) mod h
.=
((((- (x1 * y2)) + (x2 * y1)) mod h) + (((- (x3 * y4)) + (x4 * y3)) mod h)) mod h
by NAT_D:66
.=
0
by NAT_D:26, A38, A37
;
A40: (x1 * y3) mod h =
((x1 mod h) * (y3 mod h)) mod h
by NAT_D:67
.=
(x1 * x3) mod h
by NAT_D:67, A12
;
A41: (x2 * y4) mod h =
((x2 mod h) * (y4 mod h)) mod h
by NAT_D:67
.=
(x2 * x4) mod h
by NAT_D:67, A16
;
A42: (x3 * y1) mod h =
((x3 mod h) * (y1 mod h)) mod h
by NAT_D:67
.=
(x3 * x1) mod h
by NAT_D:67, A4
;
A43: (x4 * y2) mod h =
((x4 mod h) * (y2 mod h)) mod h
by NAT_D:67
.=
(x4 * x2) mod h
by NAT_D:67, A8
;
A44: ((x1 * y3) - (x3 * y1)) mod h =
(((x1 * y3) mod h) - ((x3 * y1) mod h)) mod h
by INT_6:7
.=
0
by NAT_D:26, A42, A40
;
A45: ((x4 * y2) - (x2 * y4)) mod h =
(((x4 * y2) mod h) - ((x2 * y4) mod h)) mod h
by INT_6:7
.=
0
by NAT_D:26, A41, A43
;
A46: ((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) mod h =
(((x1 * y3) - (x3 * y1)) + ((x4 * y2) - (x2 * y4))) mod h
.=
((((x1 * y3) - (x3 * y1)) mod h) + (((x4 * y2) - (x2 * y4)) mod h)) mod h
by NAT_D:66
.=
0
by NAT_D:26, A45, A44
;
A47: (x1 * y4) mod h =
((x1 mod h) * (y4 mod h)) mod h
by NAT_D:67
.=
(x1 * x4) mod h
by NAT_D:67, A16
;
A48: (x2 * y3) mod h =
((x2 mod h) * (y3 mod h)) mod h
by NAT_D:67
.=
(x2 * x3) mod h
by NAT_D:67, A12
;
A49: (x3 * y2) mod h =
((x3 mod h) * (y2 mod h)) mod h
by NAT_D:67
.=
(x3 * x2) mod h
by NAT_D:67, A8
;
A50: (x4 * y1) mod h =
((x4 mod h) * (y1 mod h)) mod h
by NAT_D:67
.=
(x4 * x1) mod h
by NAT_D:67, A4
;
A51: ((x1 * y4) - (x4 * y1)) mod h =
(((x1 * y4) mod h) - ((x4 * y1) mod h)) mod h
by INT_6:7
.=
0
by NAT_D:26, A50, A47
;
A52: ((x2 * y3) - (x3 * y2)) mod h =
(((x2 * y3) mod h) - ((x3 * y2) mod h)) mod h
by INT_6:7
.=
0
by NAT_D:26, A49, A48
;
A53: ((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) mod h =
(((x1 * y4) - (x4 * y1)) + ((x2 * y3) - (x3 * y2))) mod h
.=
((((x1 * y4) - (x4 * y1)) mod h) + (((x2 * y3) - (x3 * y2)) mod h)) mod h
by NAT_D:66
.=
0
by NAT_D:26, A52, A51
;
h divides (((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)
by A1, A32, INT_1:62;
then consider t1 being Integer such that
A55:
(((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4) = h * t1
by INT_1:def 3;
h divides (((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)
by A1, A39, INT_1:62;
then consider t2 being Integer such that
A57:
(((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3) = h * t2
by INT_1:def 3;
h divides (((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)
by A1, A46, INT_1:62;
then consider t3 being Integer such that
A59:
(((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2) = h * t3
by INT_1:def 3;
h divides (((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)
by A1, A53, INT_1:62;
then consider t4 being Integer such that
A61:
(((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1) = h * t4
by INT_1:def 3;
A62: ((h ^2) * p) * (((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h) =
((((h * t1) ^2) + ((h * t2) ^2)) + ((h * t3) ^2)) + ((h * t4) ^2)
by A61, A59, A57, A55, A25
.=
(h ^2) * ((((t1 ^2) + (t2 ^2)) + (t3 ^2)) + (t4 ^2))
;
((h ^2) ") * (h ^2) = 1
by A1, XCMPLX_0:def 7;
then A64: p * (((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h) =
((((h ^2) ") * (h ^2)) * p) * (((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h)
.=
((h ^2) ") * (((h ^2) * p) * (((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h))
.=
((h ^2) ") * ((h ^2) * ((((t1 ^2) + (t2 ^2)) + (t3 ^2)) + (t4 ^2)))
by A62
.=
(((h ^2) ") * (h ^2)) * ((((t1 ^2) + (t2 ^2)) + (t3 ^2)) + (t4 ^2))
.=
1 * ((((t1 ^2) + (t2 ^2)) + (t3 ^2)) + (t4 ^2))
by A1, XCMPLX_0:def 7
.=
(((t1 ^2) + (t2 ^2)) + (t3 ^2)) + (t4 ^2)
;
A65:
(2 * y1) ^2 <= h ^2
by A5, A6, SQUARE_1:49;
A66:
(2 * y2) ^2 <= h ^2
by A9, A10, SQUARE_1:49;
A67:
(2 * y3) ^2 <= h ^2
by A13, A14, SQUARE_1:49;
A68:
(2 * y4) ^2 <= h ^2
by A17, A18, SQUARE_1:49;
A69:
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h <= h
A76:
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h <> h
proof
assume A77:
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h = h
;
contradiction
per cases
( ((((2 * y1) ^2) + ((2 * y2) ^2)) + ((2 * y3) ^2)) + ((2 * y4) ^2) < 4 * (h ^2) or ( (2 * y1) ^2 = h ^2 & (2 * y2) ^2 = h ^2 & (2 * y3) ^2 = h ^2 & (2 * y4) ^2 = h ^2 ) )
by A65, A66, A67, A68, lem8;
suppose that A79:
(2 * y1) ^2 = h ^2
and A80:
(2 * y2) ^2 = h ^2
and A81:
(2 * y3) ^2 = h ^2
and A82:
(2 * y4) ^2 = h ^2
;
contradictionreconsider h =
h as
Integer ;
reconsider h1 =
h as
Real ;
A83:
h is
even
by A79;
consider m1 being
Nat such that A84:
2
* x1 = ((2 * m1) + 1) * h
by A1, A4, A5, A79, lem9;
consider m2 being
Nat such that A85:
2
* x2 = ((2 * m2) + 1) * h
by A1, A8, A9, A80, lem9;
consider m3 being
Nat such that A86:
2
* x3 = ((2 * m3) + 1) * h
by A1, A12, A13, A81, lem9;
consider m4 being
Nat such that A87:
2
* x4 = ((2 * m4) + 1) * h
by A1, A16, A17, A82, lem9;
p * h1 =
(((((((2 * m1) + 1) * h1) / 2) ^2) + (((((2 * m2) + 1) * h1) / 2) ^2)) + (((((2 * m3) + 1) * h1) / 2) ^2)) + (((((2 * m4) + 1) * h1) / 2) ^2)
by A84, A85, A86, A87, A3
.=
((((((((((m1 ^2) + m1) + (m2 ^2)) + m2) + (m3 ^2)) + m3) + (m4 ^2)) + m4) + 1) * h1) * h1
;
then
(p * h1) * (h1 ") = (((((((((((m1 ^2) + m1) + (m2 ^2)) + m2) + (m3 ^2)) + m3) + (m4 ^2)) + m4) + 1) * h1) * h1) * (h1 ")
;
then A88:
p * (h1 * (h1 ")) = ((((((((((m1 ^2) + m1) + (m2 ^2)) + m2) + (m3 ^2)) + m3) + (m4 ^2)) + m4) + 1) * h1) * (h1 * (h1 "))
;
h1 * (h1 ") = 1
by A1, XCMPLX_0:def 7;
hence
contradiction
by A83, A88;
verum end;
end;
reconsider x1 = x1 as Integer ;
A90:
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h <> 0
proof
assume
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h = 0
;
contradiction
then A92:
(
y1 = 0 &
y2 = 0 &
y3 = 0 &
y4 = 0 )
by A22;
then consider m1 being
Integer such that A93:
x1 = h * m1
by A1, A4, lem10;
consider m2 being
Integer such that A94:
x2 = h * m2
by A1, A8, A92, lem10;
consider m3 being
Integer such that A95:
x3 = h * m3
by A1, A12, A92, lem10;
consider m4 being
Integer such that A96:
x4 = h * m4
by A1, A16, A92, lem10;
(h * p) * (h ") = ((((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * h) * h) * (h ")
by A93, A94, A95, A96, A3;
then A99:
(h * (h ")) * p = (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * h) * (h * (h "))
;
A100:
h * (h ") = 1
by A1, XCMPLX_0:def 7;
reconsider p =
p as
Integer ;
A101:
h divides p
by A99, A100, INT_1:def 3;
reconsider p =
p as
odd prime Nat ;
end;
((((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2)) div h < h
by A69, A76, XXREAL_0:1;
hence
ex y1, y2, y3, y4 being Integer ex r being Nat st
( 0 < r & r < h & r * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) )
by A90, A64; verum