let p be natural number ; :: thesis:
assume A1: p is prime ; :: thesis:
assume A2: p mod 4 = 1 ; :: thesis:
A3: 0 <= sqrt p by SQUARE_1:def 4;
reconsider p' = [\(sqrt p)/] as Element of NAT by A3, INT_1:16, INT_1:81;
reconsider p'' = p' + 1 as Element of NAT ;
set X = Segm p'';
A4: card (Segm p'') = card p'' by CARD_1:def 12
.= 1 + [\(sqrt p)/] by CARD_1:def 5 ;
A5: (sqrt p) * (card (Segm p'')) < (card (Segm p'')) * (card (Segm p'')) by A4, INT_1:52, XREAL_1:70;
0 < sqrt p by A1, SQUARE_1:93;
then (sqrt p) * (sqrt p) < (card (Segm p'')) * (sqrt p) by A4, INT_1:52, XREAL_1:70;
then (sqrt p) * (sqrt p) < (card (Segm p'')) * (card (Segm p'')) by A5, 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 A6: p < card [:(Segm p''),(Segm p''):] by CARD_2:65;
A7: 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

let s be integer number ; :: thesis:
reconsider p' = p as Element of NAT by ORDINAL1:def 13;
set A = [:(Segm p''),(Segm p''):];
set B = Segm p';
card (Segm p') = card p' by CARD_1:def 12
.= p by CARD_1:def 5 ;
then A8: card (Segm p') in card [:(Segm p''),(Segm p''):] by A6, NAT_1:45;
A9: Segm p' <> {} by A1, ALGSEQ_1:10;
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 );
A10: 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
A11: ( n1 in Segm p'' & n2 in Segm p'' & x = [n1,n2] ) by ZFMISC_1:def 2;
reconsider n1 = n1, n2 = n2 as Element of NAT by A11;
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 A1, 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 A11; :: thesis:

end;

consider f being Function of [:(Segm p''),(Segm p''):],(Segm p') such that
A12: for x being set st x in [:(Segm p''),(Segm p''):] holds
S₁[x,f . x] from FUNCT_2:sch 1(A10);
consider x1, x2 being set such that
A13: ( x1 in [:(Segm p''),(Segm p''):] & x2 in [:(Segm p''),(Segm p''):] & x1 <> x2 & f . x1 = f . x2 ) by A8, A9, FINSEQ_4:80;
consider x', y' being set such that
A14: ( x' in Segm p'' & y' in Segm p'' & x1 = [x',y'] ) by A13, ZFMISC_1:def 2;
reconsider x' = x', y' = y' as natural number by A14;
consider x'', y'' being set such that
A15: ( x'' in Segm p'' & y'' in Segm p'' & x2 = [x'',y''] ) by A13, ZFMISC_1:def 2;
reconsider x'' = x'', y'' = y'' as natural number by A15;
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 A14, A15; :: thesis:
thus [x',y'] <> [x'',y''] by A13, A14, A15; :: thesis:
consider n11, n12, n13 being Element of NAT such that
A16: ( x1 = [n11,n12] & f . x1 = n13 & (n11 - (s * n12)) mod p = n13 ) by A12, A13;
consider n21, n22, n23 being Element of NAT such that
A17: ( x2 = [n21,n22] & f . x2 = n23 & (n21 - (s * n22)) mod p = n23 ) by A12, A13;
A18: ( n11 = x' & n12 = y' ) by A14, A16, ZFMISC_1:33;
( n21 = x'' & n22 = y'' ) by A15, A17, ZFMISC_1:33;
hence (x' - (s * y')) mod p = (x'' - (s * y'')) mod p by A18, A16, A17, A13; :: thesis:

end;

A19: p <> 2 by NAT_D:24, A2;
p > 1 by A1, INT_2:def 5;
then p + 1 > 1 + 1 by XREAL_1:8;
then p >= 2 by NAT_1:13;
then p > 2 by A19, XXREAL_0:1;
then - 1 is_quadratic_residue_mod p by A1, A2, INT_5:37;
then consider s being Integer such that
A20: ((s ^2 ) - (- 1)) mod p = 0 by INT_5:def 2;
consider x', x'', y', y'' being natural number such that
A21: ( 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 ) by A7;
((x' - (s * y')) mod p) - ((x'' - (s * y'')) mod p) = 0 by A21;
then ((x' - (s * y')) - (x'' - (s * y''))) mod p = 0 mod p by INT_6:7;
then A22: ((x' - x'') - (s * (y' - y''))) mod p = 0 by INT_4:12;
set n' = x' - x'';
set m' = y' - y'';
A23: ((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 ;
A24: 0 = ((((x' - x'') + (s * (y' - y''))) mod p) * (((x' - x'') - (s * (y' - y''))) mod p)) mod p by A22, INT_4:12
.= (((x' - x'') ^2 ) - ((s * (y' - y'')) ^2 )) mod p by A23, INT_3:15 ;
0 = ((((s ^2 ) + 1) mod p) * (((y' - y'') ^2 ) mod p)) mod p by A20, 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 ;
then 0 = (((((x' - x'') ^2 ) - ((s * (y' - y'')) ^2 )) mod p) + ((((s * (y' - y'')) ^2 ) + ((y' - y'') ^2 )) mod p)) mod p by A24, 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 A1, INT_1:89;
then consider i being Integer such that
A25: ((x' - x'') ^2 ) + ((y' - y'') ^2 ) = p * i by INT_1:def 9;
A26: p * i = (|.(x' - x'').| ^2 ) + ((y' - y'') ^2 ) by A25, COMPLEX1:161
.= ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) by COMPLEX1:161 ;
( x' in p'' & x'' in p'' & y' in p'' & y'' in p'' ) by A21, CARD_1:def 12;
then ( x' < p'' & x'' < p'' & y' < p'' & y'' < p'' ) by NAT_1:45;
then A27: ( x' <= p' & x'' <= p' & y' <= p' & y'' <= p' ) by NAT_1:13;
( x' in NAT & x'' in NAT & y' in NAT & y'' in NAT ) by ORDINAL1:def 13;
then reconsider x' = x', x'' = x'', y' = y', y'' = y'' as Real ;
0 is Element of NAT by ORDINAL1:def 13;
then A28: ( abs (x' - x'') <= p' - 0 & abs (y' - y'') <= p' - 0 ) by A27, JGRAPH_1:31;
set n = abs (x' - x'');
set m = abs (y' - y'');
A29: ( (abs (x' - x'')) ^2 <= p' ^2 & (abs (y' - y'')) ^2 <= p' ^2 ) by A28, SQUARE_1:77;
p' <= sqrt p by INT_1:def 4;
then p' ^2 <= (sqrt p) ^2 by SQUARE_1:77;
then A30: p' ^2 <= p by SQUARE_1:def 4;
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 A31: p'' * p'' = p by SQUARE_1:def 3;
then A32: p'' divides p by INT_1:def 9;

per cases by A32, A1, INT_2:def 5;

suppose p'' = 1 ; :: thesis:

hence contradiction by A31, A1, INT_2:def 5; :: thesis:

end;

suppose p'' = p ; :: thesis:

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

end;

then p' ^2 < p by A30, XXREAL_0:1;
then ( (abs (x' - x'')) ^2 < p & (abs (y' - y'')) ^2 < p ) by A29, XXREAL_0:2;
then ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) < p + p by XREAL_1:10;
then (i * p) / p < (2 * p) / p by A26, A1, 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 A1, XCMPLX_1:60;
then i * 1 < 2 by A1, XCMPLX_1:60;
then i + 1 <= 2 by INT_1:20;
then A33: (i + 1) - 1 <= 2 - 1 by XREAL_1:11;
((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) <> 0

proof

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

end;

then i > 0 by A26;
then i >= 0 + 1 by INT_1:20;
then A34: i = 1 by A33, XXREAL_0:1;
take abs (x' - x'') ; :: thesis:
take abs (y' - y'') ; :: thesis:
thus p = ((abs (x' - x'')) ^2 ) + ((abs (y' - y'')) ^2 ) by A26, A34; :: thesis: