let p be natural number ; :: thesis:
0 <= sqrt p by SQUARE_1:def 4;
then reconsider p' = [\(sqrt p)/] as Element of NAT by INT_1:16, INT_1:81;
reconsider p'' = p' + 1 as Element of NAT ;
set X = Segm p'';
A1: card (Segm p'') = card p'' by CARD_1:def 12
.= 1 + [\(sqrt p)/] by CARD_1:def 5 ;
then A2: (sqrt p) * (card (Segm p'')) < (card (Segm p'')) * (card (Segm p'')) by INT_1:52, XREAL_1:70;
assume A3: p is prime ; :: thesis:
then p > 1 by INT_2:def 5;
then p + 1 > 1 + 1 by XREAL_1:8;
then A4: p >= 2 by NAT_1:13;
A5: p' ^2 <> p

proof

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

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

suppose p'' = 1 ; :: thesis:

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

end;

suppose p'' = p ; :: thesis:

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

end;

p' <= sqrt p by INT_1:def 4;
then p' ^2 <= (sqrt p) ^2 by SQUARE_1:77;
then p' ^2 <= p by SQUARE_1:def 4;
then A8: p' ^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:93;
then (sqrt p) * (sqrt p) < (card (Segm p'')) * (sqrt p) by A1, INT_1:52, XREAL_1:70;
then (sqrt p) * (sqrt p) < (card (Segm p'')) * (card (Segm p'')) by A2, XXREAL_0:2;
then sqrt (p * p) < (card (Segm p'')) * (card (Segm p'')) by SQUARE_1:97;
then sqrt (p ^2 ) < (card (Segm p'')) * (card (Segm p'')) by SQUARE_1:def 3;
then p < (card (Segm p'')) * (card (Segm p'')) by SQUARE_1:89;
then A11: p < card [:(Segm p''),(Segm p''):] by CARD_2:65;
for s being integer number ex x', x'', y', y'' being natural number st
( x' in Segm p'' & x'' in Segm p'' & y' in Segm p'' & y'' in Segm p'' & [x',y'] <> [x'',y''] & (x' - (s * y')) mod p = (x'' - (s * y'')) mod p )

proof

set A = [:(Segm p''),(Segm p''):];
reconsider p' = p as Element of NAT by ORDINAL1:def 13;
let s be integer number ; :: thesis:
set B = Segm p';
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 p') = card p' by CARD_1:def 12
.= p by CARD_1:def 5 ;
then A12: card (Segm p') in card [:(Segm p''),(Segm p''):] by A11, NAT_1:45;
A13: for x being set st x in [:(Segm p''),(Segm p''):] holds
ex y being set st
( y in Segm p' & S₁[x,y] )

proof

let x be set ; :: thesis:
assume x in [:(Segm p''),(Segm p''):] ; :: thesis:
then consider n1, n2 being set such that
A14: ( n1 in Segm p'' & n2 in Segm p'' ) 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:16, INT_1:84;
take y ; :: thesis:
y < p by A3, INT_1:85;
then y in p by NAT_1:45;
hence y in Segm p' by CARD_1:def 12; :: thesis:
thus S₁[x,y] by A15; :: thesis:

end;

consider f being Function of [:(Segm p''),(Segm p''):], Segm p' such that
A16: for x being set st x in [:(Segm p''),(Segm p''):] holds
S₁[x,f . x] from FUNCT_2:sch 1(A13);
Segm p' <> {} by A3, ALGSEQ_1:10;
then consider x1, x2 being set such that
A17: x1 in [:(Segm p''),(Segm p''):] and
A18: x2 in [:(Segm p''),(Segm p''):] and
A19: x1 <> x2 and
A20: f . x1 = f . x2 by A12, FINSEQ_4:80;
consider x', y' being set such that
A21: ( x' in Segm p'' & y' in Segm p'' ) and
A22: x1 = [x',y'] by A17, ZFMISC_1:def 2;
reconsider x' = x', y' = y' as natural number by A21;
consider x'', y'' being set such that
A23: ( x'' in Segm p'' & y'' in Segm p'' ) and
A24: x2 = [x'',y''] by A18, ZFMISC_1:def 2;
reconsider x'' = x'', y'' = y'' as natural number by A23;
take x' ; :: thesis:
take x'' ; :: thesis:
take y' ; :: thesis:
take y'' ; :: thesis:
thus ( x' in Segm p'' & x'' in Segm p'' & y' in Segm p'' & y'' in Segm p'' ) by A21, A23; :: thesis:
thus [x',y'] <> [x'',y''] 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 = x' & n12 = y' ) by A22, A25, ZFMISC_1:33;
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 = x'' by A24, A28, ZFMISC_1:33;
hence (x' - (s * y')) mod p = (x'' - (s * y'')) mod p by A20, A24, A26, A28, A29, A27, ZFMISC_1:33; :: thesis:

end;

then consider x', x'', y', y'' being natural number such that
A30: x' in Segm p'' and
A31: x'' in Segm p'' and
A32: y' in Segm p'' and
A33: y'' in Segm p'' and
A34: [x',y'] <> [x'',y''] and
A35: (x' - (s * y')) mod p = (x'' - (s * y'')) mod p ;
set m' = y' - y'';
A36: 0 = ((((s ^2 ) + 1) mod p) * (((y' - y'') ^2 ) mod p)) mod p by A10, INT_4:12
.= (((s ^2 ) + 1) * ((y' - y'') ^2 )) mod p by INT_3:15
.= (((s ^2 ) * ((y' - y'') ^2 )) + ((y' - y'') ^2 )) mod p
.= (((s * (y' - y'')) ^2 ) + ((y' - y'') ^2 )) mod p by SQUARE_1:68 ;
set n' = x' - x'';
A37: ((x' - x'') + (s * (y' - y''))) * ((x' - x'') - (s * (y' - y''))) = ((x' - x'') to_power 2) - ((s * (y' - y'')) to_power 2) by FIB_NUM3:7
.= ((x' - x'') ^2 ) - ((s * (y' - y'')) to_power 2) by POWER:53
.= ((x' - x'') ^2 ) - ((s * (y' - y'')) ^2 ) by POWER:53 ;
((x' - (s * y')) mod p) - ((x'' - (s * y'')) mod p) = 0 by A35;
then ((x' - (s * y')) - (x'' - (s * y''))) mod p = 0 mod p by INT_6:7;
then ((x' - x'') - (s * (y' - y''))) mod p = 0 by INT_4:12;
then 0 = ((((x' - x'') + (s * (y' - y''))) mod p) * (((x' - x'') - (s * (y' - y''))) mod p)) mod p by INT_4:12
.= (((x' - x'') ^2 ) - ((s * (y' - y'')) ^2 )) mod p by A37, INT_3:15 ;
then 0 = (((((x' - x'') ^2 ) - ((s * (y' - y'')) ^2 )) mod p) + ((((s * (y' - y'')) ^2 ) + ((y' - y'') ^2 )) mod p)) mod p by A36, INT_4:12
.= ((((x' - x'') ^2 ) - ((s * (y' - y'')) ^2 )) + (((s * (y' - y'')) ^2 ) + ((y' - y'') ^2 ))) mod p by INT_3:14
.= (((x' - x'') ^2 ) + ((y' - y'') ^2 )) mod p ;
then p divides ((x' - x'') ^2 ) + ((y' - y'') ^2 ) by A3, INT_1:89;
then consider i being Integer such that
A38: ((x' - x'') ^2 ) + ((y' - y'') ^2 ) = p * i by INT_1:def 9;
A39: p * i = (|.(x' - x'').| ^2 ) + ((y' - y'') ^2 ) by A38, COMPLEX1:161
.= ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) by COMPLEX1:161 ;
y' in p'' by A32, CARD_1:def 12;
then y' < p'' by NAT_1:45;
then A40: y' <= p' by NAT_1:13;
x'' in p'' by A31, CARD_1:def 12;
then x'' < p'' by NAT_1:45;
then A41: x'' <= p' by NAT_1:13;
y'' in p'' by A33, CARD_1:def 12;
then y'' < p'' by NAT_1:45;
then A42: y'' <= p' by NAT_1:13;
x' in p'' by A30, CARD_1:def 12;
then x' < p'' by NAT_1:45;
then A43: x' <= p' by NAT_1:13;
set m = abs (y' - y'');
A44: ( y' in NAT & y'' in NAT ) by ORDINAL1:def 13;
set n = abs (x' - x'');
( x' in NAT & x'' in NAT ) by ORDINAL1:def 13;
then reconsider x' = x', x'' = x'', y' = y', y'' = y'' as Real by A44;
abs (y' - y'') <= p' - 0 by A40, A42, JGRAPH_1:31;
then (abs (y' - y'')) ^2 <= p' ^2 by SQUARE_1:77;
then A45: (abs (y' - y'')) ^2 < p by A8, XXREAL_0:2;
abs (x' - x'') <= p' - 0 by A43, A41, JGRAPH_1:31;
then (abs (x' - x'')) ^2 <= p' ^2 by SQUARE_1:77;
then (abs (x' - x'')) ^2 < p by A8, XXREAL_0:2;
then ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) < p + p by A45, XREAL_1:10;
then (i * p) / p < (2 * p) / p by A3, A39, XREAL_1:76;
then (i * p) / p < 2 * (p / p) by XCMPLX_1:75;
then i * (p / p) < 2 * (p / p) by XCMPLX_1:75;
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:20;
then A46: (i + 1) - 1 <= 2 - 1 by XREAL_1:11;
take abs (x' - x'') ; :: thesis:
take abs (y' - y'') ; :: thesis:
((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) <> 0

proof

assume A47: ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) = 0 ; :: thesis:
then (abs (y' - y'')) ^2 = 0 ;
then (abs (y' - y'')) * (abs (y' - y'')) = 0 by SQUARE_1:def 3;
then abs (y' - y'') = 0 ;
then A48: y' - y'' = 0 by ABSVALUE:7;
(abs (x' - x'')) ^2 = 0 by A47;
then (abs (x' - x'')) * (abs (x' - x'')) = 0 by SQUARE_1:def 3;
then abs (x' - x'') = 0 ;
then x' - x'' = 0 by ABSVALUE:7;
hence contradiction by A34, A48; :: thesis:

end;

then i > 0 by A39;
then i >= 0 + 1 by INT_1:20;
then i = 1 by A46, XXREAL_0:1;
hence p = ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) by A39; :: thesis: