let p be Nat; :: 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: (sqrt p) * (card (Segm p99)) < (card (Segm p99)) * (card (Segm p99)) by INT_1:29, XREAL_1:68;
assume A2: p is prime ; :: thesis:
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

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 A5: p99 * p99 = p by SQUARE_1:def 1;
then A6: p99 divides p by INT_1:def 3;

per cases by A2, A6, INT_2:def 4;

suppose p99 = 1 ; :: thesis:

hence contradiction by A2, A5, INT_2:def 4; :: thesis:

end;

suppose p99 = p ; :: thesis:

then 1 = (p * p) / p by A2, A5, XCMPLX_1:60
.= p * (p / p) by XCMPLX_1:74
.= p * 1 by A2, XCMPLX_1:60 ;
hence contradiction by A2, 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 A7: p9 ^2 < p by A4, XXREAL_0:1;
assume A8: p mod 4 = 1 ; :: thesis:
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; :: thesis:
set B = Segm p9;
defpred S₁[ 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 & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in [:(Segm p99),(Segm p99):] ; :: thesis:
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 ; :: thesis:
y < p by A2, INT_1:58;
then y in Segm p by NAT_1:44;
hence y in Segm p9 ; :: thesis:
thus S₁[x,y] by A14; :: thesis:

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
S₁[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 ; :: 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 A20, A22; :: thesis:
thus [x9,y9] <> [x99,y99] by A18, A21, A23; :: thesis:
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; :: thesis:

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 ; :: thesis:
take m ; :: thesis:
(n ^2) + (m ^2) <> 0

proof

assume A45: (n ^2) + (m ^2) = 0 ; :: thesis:
then m ^2 = 0 ;
then m * m = 0 by SQUARE_1:def 1;
then m = 0 ;
then A46: y9 - y99 = 0 by ABSVALUE:2;
n ^2 = 0 by A45;
then n * n = 0 by SQUARE_1:def 1;
then n = 0 ;
then x9 - x99 = 0 by ABSVALUE:2;
hence contradiction by A33, A46; :: thesis:

end;

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; :: thesis: