let p be Nat; ( p is prime & p mod 4 = 1 implies ex n, m being Nat st p = (n ^2) + (m ^2) )
0 <= sqrt p
by SQUARE_1:def 2;
then reconsider p9 = [\(sqrt p)/] as Element of NAT by INT_1:3, INT_1:54;
reconsider p99 = p9 + 1 as Element of NAT ;
set X = Segm p99;
A1:
(sqrt p) * (card (Segm p99)) < (card (Segm p99)) * (card (Segm p99))
by INT_1:29, XREAL_1:68;
assume A2:
p is prime
; ( not p mod 4 = 1 or ex n, m being Nat st p = (n ^2) + (m ^2) )
then
p > 1
by INT_2:def 4;
then
p + 1 > 1 + 1
by XREAL_1:6;
then A3:
p >= 2
by NAT_1:13;
A4:
p9 ^2 <> p
p9 <= sqrt p
by INT_1:def 6;
then
p9 ^2 <= (sqrt p) ^2
by SQUARE_1:15;
then
p9 ^2 <= p
by SQUARE_1:def 2;
then A7:
p9 ^2 < p
by A4, XXREAL_0:1;
assume A8:
p mod 4 = 1
; ex n, m being Nat st p = (n ^2) + (m ^2)
then
p <> 2
by NAT_D:24;
then
p > 2
by A3, XXREAL_0:1;
then
- 1 is_quadratic_residue_mod p
by A2, A8, INT_5:37;
then consider s being Integer such that
A9:
((s ^2) - (- 1)) mod p = 0
by INT_5:def 2;
0 < sqrt p
by A2, SQUARE_1:25;
then
(sqrt p) * (sqrt p) < (card (Segm p99)) * (sqrt p)
by INT_1:29, XREAL_1:68;
then
(sqrt p) * (sqrt p) < (card (Segm p99)) * (card (Segm p99))
by A1, XXREAL_0:2;
then
sqrt (p * p) < (card (Segm p99)) * (card (Segm p99))
by SQUARE_1:29;
then
sqrt (p ^2) < (card (Segm p99)) * (card (Segm p99))
by SQUARE_1:def 1;
then
p < (card (Segm p99)) * (card (Segm p99))
by SQUARE_1:22;
then A10:
p < card [:(Segm p99),(Segm p99):]
by CARD_2:46;
for s being Integer ex x9, x99, y9, y99 being Nat st
( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
proof
set A =
[:(Segm p99),(Segm p99):];
reconsider p9 =
p as
Element of
NAT by ORDINAL1:def 12;
let s be
Integer;
ex x9, x99, y9, y99 being Nat st
( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
set B =
Segm p9;
defpred S1[
object ,
object ]
means ex
n1,
n2,
n3 being
Element of
NAT st
( $1
= [n1,n2] & $2
= n3 &
(n1 - (s * n2)) mod p = n3 );
A11:
card (Segm p9) in Segm (card [:(Segm p99),(Segm p99):])
by A10, NAT_1:44;
A12:
for
x being
object st
x in [:(Segm p99),(Segm p99):] holds
ex
y being
object st
(
y in Segm p9 &
S1[
x,
y] )
proof
let x be
object ;
( x in [:(Segm p99),(Segm p99):] implies ex y being object st
( y in Segm p9 & S1[x,y] ) )
assume
x in [:(Segm p99),(Segm p99):]
;
ex y being object st
( y in Segm p9 & S1[x,y] )
then consider n1,
n2 being
object such that A13:
(
n1 in Segm p99 &
n2 in Segm p99 )
and A14:
x = [n1,n2]
by ZFMISC_1:def 2;
reconsider n1 =
n1,
n2 =
n2 as
Element of
NAT by A13;
set y =
(n1 - (s * n2)) mod p;
reconsider y =
(n1 - (s * n2)) mod p as
Element of
NAT by INT_1:3, INT_1:57;
take
y
;
( y in Segm p9 & S1[x,y] )
y < p
by A2, INT_1:58;
then
y in Segm p
by NAT_1:44;
hence
y in Segm p9
;
S1[x,y]
thus
S1[
x,
y]
by A14;
verum
end;
consider f being
Function of
[:(Segm p99),(Segm p99):],
(Segm p9) such that A15:
for
x being
object st
x in [:(Segm p99),(Segm p99):] holds
S1[
x,
f . x]
from FUNCT_2:sch 1(A12);
Segm p9 <> {}
by A2;
then consider x1,
x2 being
object such that A16:
x1 in [:(Segm p99),(Segm p99):]
and A17:
x2 in [:(Segm p99),(Segm p99):]
and A18:
x1 <> x2
and A19:
f . x1 = f . x2
by A11, FINSEQ_4:65;
consider x9,
y9 being
object such that A20:
(
x9 in Segm p99 &
y9 in Segm p99 )
and A21:
x1 = [x9,y9]
by A16, ZFMISC_1:def 2;
reconsider x9 =
x9,
y9 =
y9 as
Nat by A20;
consider x99,
y99 being
object such that A22:
(
x99 in Segm p99 &
y99 in Segm p99 )
and A23:
x2 = [x99,y99]
by A17, ZFMISC_1:def 2;
reconsider x99 =
x99,
y99 =
y99 as
Nat by A22;
take
x9
;
ex x99, y9, y99 being Nat st
( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
take
x99
;
ex y9, y99 being Nat st
( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
take
y9
;
ex y99 being Nat st
( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
take
y99
;
( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 & [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
thus
(
x9 in Segm p99 &
x99 in Segm p99 &
y9 in Segm p99 &
y99 in Segm p99 )
by A20, A22;
( [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )
thus
[x9,y9] <> [x99,y99]
by A18, A21, A23;
(x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p
consider n11,
n12,
n13 being
Element of
NAT such that A24:
x1 = [n11,n12]
and A25:
(
f . x1 = n13 &
(n11 - (s * n12)) mod p = n13 )
by A15, A16;
A26:
(
n11 = x9 &
n12 = y9 )
by A21, A24, XTUPLE_0:1;
consider n21,
n22,
n23 being
Element of
NAT such that A27:
x2 = [n21,n22]
and A28:
(
f . x2 = n23 &
(n21 - (s * n22)) mod p = n23 )
by A15, A17;
n21 = x99
by A23, A27, XTUPLE_0:1;
hence
(x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p
by A19, A23, A25, A27, A28, A26, XTUPLE_0:1;
verum
end;
then consider x9, x99, y9, y99 being Nat such that
A29:
x9 in Segm p99
and
A30:
x99 in Segm p99
and
A31:
y9 in Segm p99
and
A32:
y99 in Segm p99
and
A33:
[x9,y9] <> [x99,y99]
and
A34:
(x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p
;
set m9 = y9 - y99;
A35: 0 =
((((s ^2) + 1) mod p) * (((y9 - y99) ^2) mod p)) mod p
by A9, INT_1:73
.=
(((s ^2) + 1) * ((y9 - y99) ^2)) mod p
by NAT_D:67
.=
(((s ^2) * ((y9 - y99) ^2)) + ((y9 - y99) ^2)) mod p
.=
(((s * (y9 - y99)) ^2) + ((y9 - y99) ^2)) mod p
by SQUARE_1:9
;
set n9 = x9 - x99;
A36: ((x9 - x99) + (s * (y9 - y99))) * ((x9 - x99) - (s * (y9 - y99))) =
((x9 - x99) to_power 2) - ((s * (y9 - y99)) to_power 2)
by FIB_NUM3:7
.=
((x9 - x99) ^2) - ((s * (y9 - y99)) to_power 2)
by POWER:46
.=
((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)
by POWER:46
;
((x9 - (s * y9)) mod p) - ((x99 - (s * y99)) mod p) = 0
by A34;
then
((x9 - (s * y9)) - (x99 - (s * y99))) mod p = 0 mod p
by INT_6:7;
then
((x9 - x99) - (s * (y9 - y99))) mod p = 0
by INT_1:73;
then 0 =
((((x9 - x99) + (s * (y9 - y99))) mod p) * (((x9 - x99) - (s * (y9 - y99))) mod p)) mod p
by INT_1:73
.=
(((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) mod p
by A36, NAT_D:67
;
then 0 =
(((((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) mod p) + ((((s * (y9 - y99)) ^2) + ((y9 - y99) ^2)) mod p)) mod p
by A35, INT_1:73
.=
((((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) + (((s * (y9 - y99)) ^2) + ((y9 - y99) ^2))) mod p
by NAT_D:66
.=
(((x9 - x99) ^2) + ((y9 - y99) ^2)) mod p
;
then
p divides ((x9 - x99) ^2) + ((y9 - y99) ^2)
by A2, INT_1:62;
then consider i being Integer such that
A37:
((x9 - x99) ^2) + ((y9 - y99) ^2) = p * i
by INT_1:def 3;
A38: p * i =
(|.(x9 - x99).| ^2) + ((y9 - y99) ^2)
by A37, COMPLEX1:75
.=
(|.(x9 - x99).| ^2) + (|.(y9 - y99).| ^2)
by COMPLEX1:75
;
y9 in Segm p99
by A31;
then
y9 < p99
by NAT_1:44;
then A39:
y9 <= p9
by NAT_1:13;
x99 in Segm p99
by A30;
then
x99 < p99
by NAT_1:44;
then A40:
x99 <= p9
by NAT_1:13;
y99 in Segm p99
by A32;
then
y99 < p99
by NAT_1:44;
then A41:
y99 <= p9
by NAT_1:13;
x9 in Segm p99
by A29;
then
x9 < p99
by NAT_1:44;
then A42:
x9 <= p9
by NAT_1:13;
set m = |.(y9 - y99).|;
set n = |.(x9 - x99).|;
reconsider x9 = x9, x99 = x99, y9 = y9, y99 = y99 as Real ;
|.(y9 - y99).| <= p9 - 0
by A39, A41, JGRAPH_1:27;
then
|.(y9 - y99).| ^2 <= p9 ^2
by SQUARE_1:15;
then A43:
|.(y9 - y99).| ^2 < p
by A7, XXREAL_0:2;
|.(x9 - x99).| <= p9 - 0
by A42, A40, JGRAPH_1:27;
then
|.(x9 - x99).| ^2 <= p9 ^2
by SQUARE_1:15;
then
|.(x9 - x99).| ^2 < p
by A7, XXREAL_0:2;
then
(|.(x9 - x99).| ^2) + (|.(y9 - y99).| ^2) < p + p
by A43, XREAL_1:8;
then
(i * p) / p < (2 * p) / p
by A2, A38, XREAL_1:74;
then
(i * p) / p < 2 * (p / p)
by XCMPLX_1:74;
then
i * (p / p) < 2 * (p / p)
by XCMPLX_1:74;
then
i * (p / p) < 2 * 1
by A2, XCMPLX_1:60;
then
i * 1 < 2
by A2, XCMPLX_1:60;
then
i + 1 <= 2
by INT_1:7;
then A44:
(i + 1) - 1 <= 2 - 1
by XREAL_1:9;
reconsider n = |.(x9 - x99).|, m = |.(y9 - y99).| as Nat by TARSKI:1;
take
n
; ex m being Nat st p = (n ^2) + (m ^2)
take
m
; p = (n ^2) + (m ^2)
(n ^2) + (m ^2) <> 0
then
i > 0
by A38;
then
i >= 0 + 1
by INT_1:7;
then
i = 1
by A44, XXREAL_0:1;
hence
p = (n ^2) + (m ^2)
by A38; verum