let p be natural number ; :: thesis:
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: card (Segm p99) = card p99 by CARD_1:def 6
.= 1 + [\(sqrt p)/] by CARD_1:def 2 ;
then A2: (sqrt p) * (card (Segm p99)) < (card (Segm p99)) * (card (Segm p99)) by INT_1:29, XREAL_1:68;
assume A3: p is prime ; :: thesis:
then p > 1 by INT_2:def 4;
then p + 1 > 1 + 1 by XREAL_1:6;
then A4: p >= 2 by NAT_1:13;
A5: p9 ^2 <> p

proof

assume p9 ^2 = p ; :: thesis:
then reconsider p99 = sqrt p as Element of NAT by SQUARE_1:def 2;
p99 ^2 = p by SQUARE_1:def 2;
then A6: p99 * p99 = p by SQUARE_1:def 1;
then A7: p99 divides p by INT_1:def 3;

per cases by A3, A7, INT_2:def 4;

suppose p99 = 1 ; :: thesis:

hence contradiction by A3, A6, INT_2:def 4; :: thesis:

end;

suppose p99 = p ; :: thesis:

then 1 = (p * p) / p by A3, A6, XCMPLX_1:60
.= p * (p / p) by XCMPLX_1:74
.= p * 1 by A3, XCMPLX_1:60 ;
hence contradiction by A3, INT_2:def 4; :: thesis:

end;

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 A8: p9 ^2 < p by A5, XXREAL_0:1;
assume A9: p mod 4 = 1 ; :: thesis:
then p <> 2 by NAT_D:24;
then p > 2 by A4, XXREAL_0:1;
then - 1 is_quadratic_residue_mod p by A3, A9, INT_5:37;
then consider s being Integer such that
A10: ((s ^2) - (- 1)) mod p = 0 by INT_5:def 2;
0 < sqrt p by A3, SQUARE_1:25;
then (sqrt p) * (sqrt p) < (card (Segm p99)) * (sqrt p) by A1, INT_1:29, XREAL_1:68;
then (sqrt p) * (sqrt p) < (card (Segm p99)) * (card (Segm p99)) by A2, 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 A11: p < card [:(Segm p99),(Segm p99):] by CARD_2:46;
for s being integer number ex x9, x99, y9, y99 being natural number 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 number ; :: thesis:
set B = Segm p9;
defpred S₁[ set , set ] means ex n1, n2, n3 being Element of NAT st
( $1 = [n1,n2] & $2 = n3 & (n1 - (s * n2)) mod p = n3 );
card (Segm p9) = card p9 by CARD_1:def 6
.= p by CARD_1:def 2 ;
then A12: card (Segm p9) in card [:(Segm p99),(Segm p99):] by A11, NAT_1:44;
A13: for x being set st x in [:(Segm p99),(Segm p99):] holds
ex y being set st
( y in Segm p9 & S₁[x,y] )

proof

let x be set ; :: thesis:
assume x in [:(Segm p99),(Segm p99):] ; :: thesis:
then consider n1, n2 being set such that
A14: ( n1 in Segm p99 & n2 in Segm p99 ) and
A15: x = [n1,n2] by ZFMISC_1:def 2;
reconsider n1 = n1, n2 = n2 as Element of NAT by A14;
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 ; :: thesis:
y < p by A3, INT_1:58;
then y in p by NAT_1:44;
hence y in Segm p9 by CARD_1:def 6; :: thesis:
thus S₁[x,y] by A15; :: thesis:

end;

consider f being Function of [:(Segm p99),(Segm p99):],(Segm p9) such that
A16: for x being set st x in [:(Segm p99),(Segm p99):] holds
S₁[x,f . x] from FUNCT_2:sch 1(A13);
Segm p9 <> {} by A3, ALGSEQ_1:1;
then consider x1, x2 being set such that
A17: x1 in [:(Segm p99),(Segm p99):] and
A18: x2 in [:(Segm p99),(Segm p99):] and
A19: x1 <> x2 and
A20: f . x1 = f . x2 by A12, FINSEQ_4:65;
consider x9, y9 being set such that
A21: ( x9 in Segm p99 & y9 in Segm p99 ) and
A22: x1 = [x9,y9] by A17, ZFMISC_1:def 2;
reconsider x9 = x9, y9 = y9 as natural number by A21;
consider x99, y99 being set such that
A23: ( x99 in Segm p99 & y99 in Segm p99 ) and
A24: x2 = [x99,y99] by A18, ZFMISC_1:def 2;
reconsider x99 = x99, y99 = y99 as natural number by A23;
take x9 ; :: thesis:
take x99 ; :: thesis:
take y9 ; :: thesis:
take y99 ; :: thesis:
thus ( x9 in Segm p99 & x99 in Segm p99 & y9 in Segm p99 & y99 in Segm p99 ) by A21, A23; :: thesis:
thus [x9,y9] <> [x99,y99] by A19, A22, A24; :: thesis:
consider n11, n12, n13 being Element of NAT such that
A25: x1 = [n11,n12] and
A26: ( f . x1 = n13 & (n11 - (s * n12)) mod p = n13 ) by A16, A17;
A27: ( n11 = x9 & n12 = y9 ) by A22, A25, ZFMISC_1:27;
consider n21, n22, n23 being Element of NAT such that
A28: x2 = [n21,n22] and
A29: ( f . x2 = n23 & (n21 - (s * n22)) mod p = n23 ) by A16, A18;
n21 = x99 by A24, A28, ZFMISC_1:27;
hence (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p by A20, A24, A26, A28, A29, A27, ZFMISC_1:27; :: thesis:

end;

then consider x9, x99, y9, y99 being natural number such that
A30: x9 in Segm p99 and
A31: x99 in Segm p99 and
A32: y9 in Segm p99 and
A33: y99 in Segm p99 and
A34: [x9,y9] <> [x99,y99] and
A35: (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p ;
set m9 = y9 - y99;
A36: 0 = ((((s ^2) + 1) mod p) * (((y9 - y99) ^2) mod p)) mod p by A10, INT_4:12
.= (((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;
A37: ((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 A35;
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_4:12;
then 0 = ((((x9 - x99) + (s * (y9 - y99))) mod p) * (((x9 - x99) - (s * (y9 - y99))) mod p)) mod p by INT_4:12
.= (((x9 - x99) ^2) - ((s * (y9 - y99)) ^2)) mod p by A37, 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 A36, INT_4:12
.= ((((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 A3, INT_1:62;
then consider i being Integer such that
A38: ((x9 - x99) ^2) + ((y9 - y99) ^2) = p * i by INT_1:def 3;
A39: p * i = (|.(x9 - x99).| ^2) + ((y9 - y99) ^2) by A38, COMPLEX1:75
.= ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) by COMPLEX1:75 ;
y9 in p99 by A32, CARD_1:def 6;
then y9 < p99 by NAT_1:44;
then A40: y9 <= p9 by NAT_1:13;
x99 in p99 by A31, CARD_1:def 6;
then x99 < p99 by NAT_1:44;
then A41: x99 <= p9 by NAT_1:13;
y99 in p99 by A33, CARD_1:def 6;
then y99 < p99 by NAT_1:44;
then A42: y99 <= p9 by NAT_1:13;
x9 in p99 by A30, CARD_1:def 6;
then x9 < p99 by NAT_1:44;
then A43: x9 <= p9 by NAT_1:13;
set m = abs (y9 - y99);
A44: ( y9 in NAT & y99 in NAT ) by ORDINAL1:def 12;
set n = abs (x9 - x99);
( x9 in NAT & x99 in NAT ) by ORDINAL1:def 12;
then reconsider x9 = x9, x99 = x99, y9 = y9, y99 = y99 as Real by A44;
abs (y9 - y99) <= p9 - 0 by A40, A42, JGRAPH_1:27;
then (abs (y9 - y99)) ^2 <= p9 ^2 by SQUARE_1:15;
then A45: (abs (y9 - y99)) ^2 < p by A8, XXREAL_0:2;
abs (x9 - x99) <= p9 - 0 by A43, A41, JGRAPH_1:27;
then (abs (x9 - x99)) ^2 <= p9 ^2 by SQUARE_1:15;
then (abs (x9 - x99)) ^2 < p by A8, XXREAL_0:2;
then ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) < p + p by A45, XREAL_1:8;
then (i * p) / p < (2 * p) / p by A3, A39, 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 A3, XCMPLX_1:60;
then i * 1 < 2 by A3, XCMPLX_1:60;
then i + 1 <= 2 by INT_1:7;
then A46: (i + 1) - 1 <= 2 - 1 by XREAL_1:9;
take abs (x9 - x99) ; :: thesis:
take abs (y9 - y99) ; :: thesis:
((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) <> 0

proof

assume A47: ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) = 0 ; :: thesis:
then (abs (y9 - y99)) ^2 = 0 ;
then (abs (y9 - y99)) * (abs (y9 - y99)) = 0 by SQUARE_1:def 1;
then abs (y9 - y99) = 0 ;
then A48: y9 - y99 = 0 by ABSVALUE:2;
(abs (x9 - x99)) ^2 = 0 by A47;
then (abs (x9 - x99)) * (abs (x9 - x99)) = 0 by SQUARE_1:def 1;
then abs (x9 - x99) = 0 ;
then x9 - x99 = 0 by ABSVALUE:2;
hence contradiction by A34, A48; :: thesis:

end;

then i > 0 by A39;
then i >= 0 + 1 by INT_1:7;
then i = 1 by A46, XXREAL_0:1;
hence p = ((abs (x9 - x99)) ^2) + ((abs (y9 - y99)) ^2) by A39; :: thesis: