let p be Nat; :: thesis: ( 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 ; :: thesis: ( 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

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: 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 )

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: ex m being Nat st p = (n ^2) + (m ^2)

take m ; :: thesis: p = (n ^2) + (m ^2)

(n ^2) + (m ^2) <> 0

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: verum

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: ( 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

proof

p9 <= sqrt p
by INT_1:def 6;
assume
p9 ^2 = p
; :: thesis: contradiction

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;

end;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
( p99 = 1 or p99 = p )
by A2, A6, INT_2:def 4;

end;

suppose
p99 = p
; :: thesis: contradiction

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: verum

end;.= p * (p / p) by XCMPLX_1:74

.= p * 1 by A2, XCMPLX_1:60 ;

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

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

then consider x9, x99, y9, y99 being Nat such that
set A = [:(Segm p99),(Segm p99):];

reconsider p9 = p as Element of NAT by ORDINAL1:def 12;

let s be Integer; :: thesis: 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 S_{1}[ 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_{1}[x,y] )

A15: for x being object st x in [:(Segm p99),(Segm p99):] holds

S_{1}[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: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )

thus [x9,y9] <> [x99,y99] by A18, A21, A23; :: thesis: (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; :: thesis: verum

end;reconsider p9 = p as Element of NAT by ORDINAL1:def 12;

let s be Integer; :: thesis: 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 S

( $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

proof

consider f being Function of [:(Segm p99),(Segm p99):],(Segm p9) such that
let x be object ; :: thesis: ( x in [:(Segm p99),(Segm p99):] implies ex y being object st

( y in Segm p9 & S_{1}[x,y] ) )

assume x in [:(Segm p99),(Segm p99):] ; :: thesis: ex y being object st

( y in Segm p9 & S_{1}[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 ; :: thesis: ( y in Segm p9 & S_{1}[x,y] )

y < p by A2, INT_1:58;

then y in Segm p by NAT_1:44;

hence y in Segm p9 ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A14; :: thesis: verum

end;( y in Segm p9 & S

assume x in [:(Segm p99),(Segm p99):] ; :: thesis: ex y being object st

( y in Segm p9 & S

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 in Segm p9 & S

y < p by A2, INT_1:58;

then y in Segm p by NAT_1:44;

hence y in Segm p9 ; :: thesis: S

thus S

A15: for x being object st x in [:(Segm p99),(Segm p99):] holds

S

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: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( [x9,y9] <> [x99,y99] & (x9 - (s * y9)) mod p = (x99 - (s * y99)) mod p )

thus [x9,y9] <> [x99,y99] by A18, A21, A23; :: thesis: (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; :: thesis: verum

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: ex m being Nat st p = (n ^2) + (m ^2)

take m ; :: thesis: p = (n ^2) + (m ^2)

(n ^2) + (m ^2) <> 0

proof

then
i > 0
by A38;
assume A45:
(n ^2) + (m ^2) = 0
; :: thesis: contradiction

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: verum

end;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: verum

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: verum