let n be Proth Nat; :: thesis: ( n is prime iff ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n )
consider k being odd Nat, l being positive Nat such that
A1: ( 2 |^ l > k & n = (k * (2 |^ l)) + 1 ) by Def5;
set s = 2 |^ l;
A2: l + 1 >= 1 + 1 by NAT_1:14, XREAL_1:6;
2 |^ l >= l + 1 by NEWTON:85;
then ( 2 |^ l <> 0 & 2 |^ l <> 1 ) by A2, XXREAL_0:2;
then reconsider s = 2 |^ l as non trivial Nat by NAT_2:def 1;
reconsider s = s as non trivial Divisor of n - 1 by A1, INT_1:def 3, Def2;

A3: now :: thesis: ( ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n implies n is prime )

assume ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n ; :: thesis: n is prime
then consider a being Nat such that
A4: a |^ ((n - 1) / 2), - 1 are_congruent_mod n ;
A5: (a |^ ((n - 1) / 2)) * (a |^ ((n - 1) / 2)) = a |^ (((n - 1) / 2) + ((n - 1) / 2)) by NEWTON:8
.= a |^ (n - 1) ;
A6: (- 1) * (- 1) = 1 ;
A7: l >= 1 by NAT_1:14;
((2 |^ l) - 1) + 1 > k by A1;
then A8: k <= (2 |^ l) - 1 by NAT_1:13;
then k * (2 |^ l) <= ((2 |^ l) - 1) * (2 |^ l) by XREAL_1:64;
then A9: n <= (((2 |^ l) - 1) * (2 |^ l)) + 1 by A1, XREAL_1:6;
(((2 |^ l) - 1) * (2 |^ l)) + 1 = (((2 |^ l) * (2 |^ l)) - (2 |^ l)) + 1
.= ((2 |^ (l + l)) - (2 |^ l)) + 1 by NEWTON:8 ;
then A10: n < (((2 |^ (l + l)) - (2 |^ l)) + 1) + 1 by A9, NAT_1:13;
A11: s > sqrt n

proof

per cases ( l >= 2 or l < 2 ) ;

suppose l >= 2 ; :: thesis: s > sqrt n

then A12: 2 |^ l >= 2 |^ 2 by Th1;
2 |^ (1 + 1) = (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
then 2 |^ l > 2 by A12, XXREAL_0:2;
then 2 - (2 |^ l) < (2 |^ l) - (2 |^ l) by XREAL_1:9;
then (2 |^ (l + l)) + ((- (2 |^ l)) + 2) < (2 |^ (l + l)) + 0 by XREAL_1:6;
then A13: n < 2 |^ (2 * l) by A10, XXREAL_0:2;
(2 |^ l) ^2 = 2 |^ (l + l) by NEWTON:8;
then sqrt (2 |^ (2 * l)) = 2 |^ l by SQUARE_1:def 2;
hence s > sqrt n by A13, SQUARE_1:27; :: thesis: verum

end;

suppose l < 2 ; :: thesis: s > sqrt n

then l < 1 + 1 ;
then A14: l <= 1 by NAT_1:13;
then A15: l = 1 by A7, XXREAL_0:1;
then A16: s = sqrt 4 by SQUARE_1:20;
A17: n = (k * (2 |^ 1)) + 1 by A14, A1, A7, XXREAL_0:1
.= (k * 2) + 1 ;
A18: k <= 2 - 1 by A8, A15;
k >= 1 by NAT_1:14;
then k = 1 by A18, XXREAL_0:1;
hence s > sqrt n by A17, A16, SQUARE_1:27; :: thesis: verum

end;

end;

end;

now :: thesis: for q being prime Divisor of s holds ((a |^ ((n - 1) / q)) - 1) gcd n = 1

let q be prime Divisor of s; :: thesis: ((a |^ ((n - 1) / q)) - 1) gcd n = 1
A19: a |^ ((n - 1) / q), - 1 are_congruent_mod n by A4, Th8, INT_2:28, Def2;
1 * ((a |^ ((n - 1) / q)) - 1) = (a |^ ((n - 1) / q)) - 1 ;
then A20: 1 divides (a |^ ((n - 1) / q)) - 1 ;
1 * n = n ;
then A21: 1 divides n ;

now :: thesis: for m being Integer st m divides (a |^ ((n - 1) / q)) - 1 & m divides n holds
m divides 1

let m be Integer; :: thesis: ( m divides (a |^ ((n - 1) / q)) - 1 & m divides n implies m divides 1 )
assume A22: ( m divides (a |^ ((n - 1) / q)) - 1 & m divides n ) ; :: thesis: m divides 1
then A23: a |^ ((n - 1) / q),1 are_congruent_mod m ;
consider j being Integer such that
A24: m * j = n by A22;
a |^ ((n - 1) / q), - 1 are_congruent_mod m by A19, A24, INT_1:20;
then (a |^ ((n - 1) / q)) - (a |^ ((n - 1) / q)),(- 1) - 1 are_congruent_mod m by A23, INT_1:17;
then 0 + 1,(- 2) + 1 are_congruent_mod m ;
then A25: ( m = 2 or m = 1 or m = - 2 or m = - 1 ) by Th20, INT_1:14;

A26: now :: thesis: not - 2 divides n

assume - 2 divides n ; :: thesis: contradiction
then consider g being Integer such that
A27: n = (- 2) * g ;
n = 2 * (- g) by A27;
hence contradiction ; :: thesis: verum

end;

( 1 * 1 = 1 & (- 1) * (- 1) = 1 ) ;
hence m divides 1 by A26, A22, A25; :: thesis: verum

end;

hence ((a |^ ((n - 1) / q)) - 1) gcd n = 1 by A20, A21, INT_2:def 2; :: thesis: verum

end;

hence n is prime by A4, A5, INT_1:18, A6, A11, Th21; :: thesis: verum

end;

now :: thesis: ( n is prime implies ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n )

assume n is prime ; :: thesis: ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n
then reconsider m = n as prime Proth Nat ;
Z/Z* m is cyclic by INT_7:31;
then consider g being Element of (Z/Z* m) such that
A28: ord g = card (Z/Z* m) by GR_CY_1:19;
A29: ord g = m - 1 by A28, INT_7:23;
Z/Z* m = multMagma(# (Segm0 m),(multint0 m) #) by INT_7:def 4;
then reconsider g1 = g as Nat ;
A30: not g is being_of_order_0 by A28, GROUP_1:def 11;
A31: (g1 |^ (m - 1)) mod m = g |^ (m - 1) by Th17
.= 1_ (Z/Z* m) by A29, A30, GROUP_1:def 11
.= 1 by INT_7:21 ;
A32: g1 |^ (m - 1),1 are_congruent_mod m by Th10, A31;
A33: (g1 |^ ((m - 1) / 2)) |^ (1 + 1) = ((g1 |^ ((m - 1) / 2)) |^ 1) * (g1 |^ ((m - 1) / 2)) by NEWTON:6
.= (g1 |^ ((m - 1) / 2)) * (g1 |^ ((m - 1) / 2))
.= g1 |^ (((m - 1) / 2) + ((m - 1) / 2)) by NEWTON:8
.= g1 |^ (m - 1) ;

now :: thesis: not g1 |^ ((m - 1) / 2),1 are_congruent_mod n

assume A34: g1 |^ ((m - 1) / 2),1 are_congruent_mod n ; :: thesis: contradiction
A35: 1_ (Z/Z* m) = 1 by INT_7:21
.= (g1 |^ ((m - 1) / 2)) mod m by A34, INT_2:def 4, Th12
.= g |^ ((m - 1) / 2) by Th17 ;
A36: m - 1 <> 0 ;
( (m - 1) * 2 >= (m - 1) * 1 & 0 < 2 ) by XREAL_1:64;
then A37: (m - 1) / 2 <= m - 1 by XREAL_1:79;
m - 1 <= (m - 1) / 2 by A29, A30, A35, GROUP_1:def 11;
then m - 1 = (m - 1) / 2 by A37, XXREAL_0:1;
hence contradiction by A36; :: thesis: verum

end;

hence ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n by A33, A32, Th18; :: thesis: verum

end;

hence ( n is prime iff ex a being Nat st a |^ ((n - 1) / 2), - 1 are_congruent_mod n ) by A3; :: thesis: verum