let p be odd prime Nat; ex x1, x2, x3, x4, h being Nat st
( 0 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
consider s being Integer such that
A1:
2 * s = p + 1
by ABIAN:11;
s > 0
by A1;
then
s in NAT
by INT_1:3;
then reconsider s = s as Nat ;
set f = LAG4SQf s;
set g = LAG4SQg s;
A5: dom (LAG4SQf s) =
Seg (len (LAG4SQf s))
by FINSEQ_1:def 3
.=
Seg s
by Def2
;
A6: dom (LAG4SQg s) =
Seg (len (LAG4SQg s))
by FINSEQ_1:def 3
.=
Seg s
by Def3
;
A7:
LAG4SQf s is one-to-one
by lem1;
A8:
LAG4SQg s is one-to-one
by lem2;
A9:
rng (LAG4SQf s) misses rng (LAG4SQg s)
A19:
card (rng ((LAG4SQg s) ^ (LAG4SQf s))) = p + 1
A23:
rng ((LAG4SQg s) ^ (LAG4SQf s)) = (rng (LAG4SQg s)) \/ (rng (LAG4SQf s))
by FINSEQ_1:31;
A24:
dom (MODMAP_ p) = INT
by FUNCT_2:def 1;
A25:
card (dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) = p + 1
by A19, A24, RELAT_1:62;
A26:
card (rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) <= card (Segm p)
by NAT_1:43;
set s1 = card (rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))));
set t1 = card (dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))));
card (rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) < card (dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))))
by A25, A26, NAT_1:13;
then A28:
card (rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) in { i where i is Nat : i < card (dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) }
;
A29:
dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) <> {}
by A25;
set A = dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))));
set B = rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))));
defpred S1[ object , object ] means ex m1 being Element of INT st
( $1 in dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) & $2 = m1 & ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) . $1 = m1 );
A30:
card (rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) in card (dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))))
by A28, AXIOMS:4;
A31:
for x being object st x in dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) holds
ex y being object st
( y in rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) & S1[x,y] )
consider h being Function of (dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))),(rng ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))) such that
A38:
for x being object st x in dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) holds
S1[x,h . x]
from FUNCT_2:sch 1(A31);
consider m1, m2 being object such that
A39:
m1 in dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))
and
A40:
m2 in dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s))))
and
A41:
m1 <> m2
and
A42:
h . m1 = h . m2
by A29, A30, RELAT_1:42, FINSEQ_4:65;
A43:
S1[m1,h . m1]
by A38, A39;
A44:
S1[m2,h . m2]
by A38, A40;
reconsider m1 = m1, m2 = m2 as Element of INT by A39, A40;
A46: ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) . m1 =
(MODMAP_ p) . m1
by A39, FUNCT_1:47
.=
m1 mod p
by Def1
;
A47: ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) . m2 =
(MODMAP_ p) . m2
by A40, FUNCT_1:47
.=
m2 mod p
by Def1
;
A49: dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) =
(dom (MODMAP_ p)) /\ (rng ((LAG4SQg s) ^ (LAG4SQf s)))
by RELAT_1:61
.=
rng ((LAG4SQg s) ^ (LAG4SQf s))
by A24, XBOOLE_1:28
;
A50:
( m1 in rng (LAG4SQf s) implies m2 in rng (LAG4SQg s) )
proof
assume A51:
m1 in rng (LAG4SQf s)
;
m2 in rng (LAG4SQg s)
assume
not
m2 in rng (LAG4SQg s)
;
contradiction
then
m2 in rng (LAG4SQf s)
by A23, A40, A49, XBOOLE_0:def 3;
hence
contradiction
by A1, A41, A47, A44, A42, A43, A46, A51, lem4;
verum
end;
A54:
( m1 in rng (LAG4SQg s) implies m2 in rng (LAG4SQf s) )
proof
assume A55:
m1 in rng (LAG4SQg s)
;
m2 in rng (LAG4SQf s)
assume
not
m2 in rng (LAG4SQf s)
;
contradiction
then
m2 in rng (LAG4SQg s)
by A23, A40, A49, XBOOLE_0:def 3;
hence
contradiction
by A1, A41, A47, A44, A42, A43, A46, A55, lem5;
verum
end;
A58: dom ((MODMAP_ p) | (rng ((LAG4SQg s) ^ (LAG4SQf s)))) =
(dom (MODMAP_ p)) /\ (rng ((LAG4SQg s) ^ (LAG4SQf s)))
by RELAT_1:61
.=
rng ((LAG4SQg s) ^ (LAG4SQf s))
by A24, XBOOLE_1:28
;
ex x1, x2, x3, x4, h being Nat st
( h > 0 & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
proof
A60:
p * (p ") = 1
by XCMPLX_0:def 7;
per cases
( m1 in rng (LAG4SQf s) or m1 in rng (LAG4SQg s) )
by A23, A39, A58, XBOOLE_0:def 3;
suppose A61:
m1 in rng (LAG4SQf s)
;
ex x1, x2, x3, x4, h being Nat st
( h > 0 & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )then consider x0 being
object such that A62:
x0 in dom (LAG4SQf s)
and A63:
m1 = (LAG4SQf s) . x0
by FUNCT_1:def 3;
reconsider x0 =
x0 as
Nat by A62;
A64:
m1 = (x0 - 1) ^2
by Def2, A62, A63;
consider y0 being
object such that A65:
y0 in dom (LAG4SQg s)
and A66:
m2 = (LAG4SQg s) . y0
by A50, A61, FUNCT_1:def 3;
reconsider y0 =
y0 as
Nat by A65;
A67:
m2 = (- 1) - ((y0 - 1) ^2)
by Def3, A65, A66;
(m1 - m2) mod p =
((m1 mod p) - (m2 mod p)) mod p
by INT_6:7
.=
0
by A47, A44, A42, A43, A46, NAT_D:26
;
then A69:
(m1 - m2) - (((m1 - m2) div p) * p) = 0
by INT_1:def 10;
A70:
(m1 - m2) div p > 0
by A64, A67, A69;
consider x9 being
Nat such that A71:
x0 = x9
and A72:
1
<= x9
and A73:
x9 <= s
by A5, A62;
A74:
1
- 1
<= x9 - 1
by A72, XREAL_1:9;
consider y9 being
Nat such that A75:
y0 = y9
and A76:
1
<= y9
and A77:
y9 <= s
by A6, A65;
A78:
1
- 1
<= y9 - 1
by A76, XREAL_1:9;
x9 - 1
<= s - 1
by A73, XREAL_1:9;
then A80:
(x9 - 1) ^2 <= (s - 1) ^2
by A74, XREAL_1:66;
y9 - 1
<= s - 1
by A77, XREAL_1:9;
then
(y9 - 1) ^2 <= (s - 1) ^2
by A78, XREAL_1:66;
then
((x9 - 1) ^2) + ((y9 - 1) ^2) <= ((s - 1) ^2) + ((s - 1) ^2)
by A80, XREAL_1:7;
then A84:
(((x0 - 1) ^2) + ((y0 - 1) ^2)) + 1
<= (((s - 1) ^2) + ((s - 1) ^2)) + 1
by A71, A75, XREAL_1:7;
A85:
p ^2 = ((2 * s) - 1) ^2
by A1;
(2 * s) - 2
> 3
- 2
by A1, XREAL_1:9, lem3a;
then A86:
(s + 1) * ((2 * s) - 2) > 0
;
A87:
((p ^2) - ((((s - 1) ^2) + ((s - 1) ^2)) + 1)) + ((((s - 1) ^2) + ((s - 1) ^2)) + 1) > 0 + ((((s - 1) ^2) + ((s - 1) ^2)) + 1)
by A85, A86, XREAL_1:6;
A89:
x0 - 1
in NAT
by A71, A74, INT_1:3;
A90:
y0 - 1
in NAT
by A75, A78, INT_1:3;
set h =
(m1 - m2) div p;
(m1 - m2) div p in NAT
by A70, INT_1:3;
then reconsider h =
(m1 - m2) div p as
Nat ;
A92:
h > 0
by A69, A64, A67;
consider x1,
x2,
x3,
x4 being
Nat such that A93:
x1 = x0 - 1
and A94:
x2 = y0 - 1
and A95:
x3 = 1
and A96:
x4 = 0
by A89, A90;
A97:
(((x0 - 1) ^2) + ((y0 - 1) ^2)) + 1
= (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
by A96, A95, A94, A93;
h * p < p * p
by A69, A64, A67, A84, A87, XXREAL_0:2;
then
(h * p) * (p ") < (p * p) * (p ")
by XREAL_1:68;
then
h * (p * (p ")) < p * (p * (p "))
;
hence
ex
x1,
x2,
x3,
x4,
h being
Nat st
(
h > 0 &
h < p &
h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
by A92, A69, A64, A67, A97, A60;
verum end; suppose A101:
m1 in rng (LAG4SQg s)
;
ex x1, x2, x3, x4, h being Nat st
( h > 0 & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )consider x0 being
object such that A102:
x0 in dom (LAG4SQf s)
and A103:
m2 = (LAG4SQf s) . x0
by A54, A101, FUNCT_1:def 3;
reconsider x0 =
x0 as
Nat by A102;
consider y0 being
object such that A104:
y0 in dom (LAG4SQg s)
and A105:
m1 = (LAG4SQg s) . y0
by A101, FUNCT_1:def 3;
reconsider y0 =
y0 as
Nat by A104;
A106:
m1 = (- 1) - ((y0 - 1) ^2)
by A104, A105, Def3;
(m2 - m1) mod p =
((m2 mod p) - (m1 mod p)) mod p
by INT_6:7
.=
0
by A47, A44, A42, A43, A46, NAT_D:26
;
then
(m2 - m1) - (((m2 - m1) div p) * p) = 0
by INT_1:def 10;
then A109:
((x0 - 1) ^2) - ((- 1) - ((y0 - 1) ^2)) = ((m2 - m1) div p) * p
by A102, A103, A106, Def2;
A110:
(m2 - m1) div p >= 0
by A109;
consider x9 being
Nat such that A111:
x0 = x9
and A112:
1
<= x9
and A113:
x9 <= s
by A102, A5;
A114:
1
- 1
<= x9 - 1
by A112, XREAL_1:9;
consider y9 being
Nat such that A115:
y0 = y9
and A116:
1
<= y9
and A117:
y9 <= s
by A6, A104;
A118:
1
- 1
<= y9 - 1
by A116, XREAL_1:9;
x9 - 1
<= s - 1
by A113, XREAL_1:9;
then A120:
(x9 - 1) ^2 <= (s - 1) ^2
by A114, XREAL_1:66;
y9 - 1
<= s - 1
by A117, XREAL_1:9;
then
(y9 - 1) ^2 <= (s - 1) ^2
by A118, XREAL_1:66;
then
((x9 - 1) ^2) + ((y9 - 1) ^2) <= ((s - 1) ^2) + ((s - 1) ^2)
by A120, XREAL_1:7;
then A124:
(((x0 - 1) ^2) + ((y0 - 1) ^2)) + 1
<= (((s - 1) ^2) + ((s - 1) ^2)) + 1
by A111, A115, XREAL_1:7;
A125:
p ^2 = ((2 * s) - 1) ^2
by A1;
(2 * s) - 2
> 3
- 2
by A1, XREAL_1:9, lem3a;
then
(s + 1) * ((2 * s) - 2) > 0
;
then A127:
((p ^2) - ((((s - 1) ^2) + ((s - 1) ^2)) + 1)) + ((((s - 1) ^2) + ((s - 1) ^2)) + 1) > 0 + ((((s - 1) ^2) + ((s - 1) ^2)) + 1)
by A125, XREAL_1:6;
set h =
(m2 - m1) div p;
(m2 - m1) div p in NAT
by A110, INT_1:3;
then reconsider h =
(m2 - m1) div p as
Nat ;
A129:
x0 - 1
in NAT
by A114, A111, INT_1:3;
A130:
y0 - 1
in NAT
by INT_1:3, A115, A118;
A132:
h > 0
by A109;
consider x1,
x2,
x3,
x4 being
Nat such that A133:
(
x1 = x0 - 1 &
x2 = y0 - 1 &
x3 = 1 &
x4 = 0 )
by A129, A130;
A134:
(((x0 - 1) ^2) + ((y0 - 1) ^2)) + 1
= (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
by A133;
h * p < p * p
by A109, A124, A127, XXREAL_0:2;
then
(h * p) * (p ") < (p * p) * (p ")
by XREAL_1:68;
then
h * (p * (p ")) < p * (p * (p "))
;
hence
ex
x1,
x2,
x3,
x4,
h being
Nat st
(
h > 0 &
h < p &
h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
by A60, A109, A132, A134;
verum end;
end;
hence
ex x1, x2, x3, x4, h being Nat st
( 0 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
; verum