let n be Nat; :: thesis: ( n + 2 is prime implies for l being Nat st l in Seg n & l <> 1 holds
ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume A1: n + 2 is prime ; :: thesis: for l being Nat st l in Seg n & l <> 1 holds
ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
then A2: 1 < n9 + 2 by INT_2:def 4;
let l be Nat; :: thesis: ( l in Seg n & l <> 1 implies ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
reconsider l9 = l as Element of NAT by ORDINAL1:def 12;
assume A3: l in Seg n ; :: thesis: ( not l <> 1 or ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
then A4: l9 <> 0 by FINSEQ_1:1;
assume A5: l <> 1 ; :: thesis: ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
A6: l <= n by A3, FINSEQ_1:1;
then A7: l < n + 1 by NAT_1:13;
A8: 1 + n < 2 + n by XREAL_1:6;
then l9 < n9 + 2 by A7, XXREAL_0:2;
then consider k being Nat such that
A9: (k * l9) mod (n9 + 2) = 1 and
A10: k < n9 + 2 by A1, A2, A4, IDEA_1:1;
take k ; :: thesis: ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
k <> 0 by A9, NAT_D:26;
then A11: k >= 0 + 1 by NAT_1:13;
A12: 1 <= l by A3, FINSEQ_1:1;
then A13: 1 - 1 <= l - 1 by XREAL_1:9;
A14: l < n + 2 by A7, A8, XXREAL_0:2;
then A15: n + 2 > 1 by A12, XXREAL_0:2;
A16: l + 1 < (n + 1) + 1 by A7, XREAL_1:6;
A17: k <> n + 1

proof

assume k = n + 1 ; :: thesis: contradiction
then ((n + 1) * l) mod (n + 2) = 1 mod (n + 2) by A9, A15, NAT_D:14
.= (((n + 2) * l) + 1) mod (n + 2) by NAT_D:21 ;
then 0 = ((((n + 2) * l) + 1) - ((n + 1) * l)) mod (n + 2) by INT_4:22
.= l + 1 by A16, NAT_D:24 ;
hence contradiction ; :: thesis: verum

end;

k < (n + 1) + 1 by A10;
then k <= n + 1 by NAT_1:13;
then k < n + 1 by A17, XXREAL_0:1;
then k <= n by NAT_1:13;
hence k in Seg n by A11; :: thesis: ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
l - 1 < (n + 2) - 1 by A14, XREAL_1:9;
then l - 1 < n + 2 by A8, XXREAL_0:2;
then A18: l -' 1 < n + 2 by XREAL_0:def 2;
thus A19: k <> 1 :: thesis: ( k <> l & (l * k) mod (n + 2) = 1 )

proof

assume k = 1 ; :: thesis: contradiction
then (1 * l) mod (n + 2) = 1 mod (n + 2) by A9, A10, NAT_D:14;
then 0 = (l - 1) mod (n + 2) by INT_4:22
.= (l -' 1) mod (n + 2) by A13, XREAL_0:def 2
.= l -' 1 by A18, NAT_D:24
.= l - 1 by A13, XREAL_0:def 2 ;
hence contradiction by A5; :: thesis: verum

end;

thus k <> l :: thesis: (l * k) mod (n + 2) = 1

proof

assume A20: k = l ; :: thesis: contradiction
then (l * l) mod (n + 2) = 1 mod (n + 2) by A9, A15, NAT_D:14;
then 0 = ((l * l) - 1) mod (n + 2) by INT_4:22;
then A21: n + 2 divides (l + 1) * (l - 1) by INT_1:62;

per cases ( n + 2 divides l + 1 or n + 2 divides l - 1 ) by A1, A21, INT_5:7;

suppose n + 2 divides l + 1 ; :: thesis: contradiction

then n + 2 <= l + 1 by NAT_D:7;
then (n + 2) - 1 <= (l + 1) - 1 by XREAL_1:9;
hence contradiction by A7; :: thesis: verum

end;

suppose n + 2 divides l - 1 ; :: thesis: contradiction

then A22: n + 2 divides l -' 1 by A13, XREAL_0:def 2;

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

suppose l = 1 ; :: thesis: contradiction

hence contradiction by A19, A20; :: thesis: verum

end;

suppose l <> 1 ; :: thesis: contradiction

then l > 1 by A12, XXREAL_0:1;
then l - 1 > 1 - 1 by XREAL_1:9;
then l -' 1 > 0 by XREAL_0:def 2;
then n + 2 <= l -' 1 by A22, NAT_D:7;
then n + 2 <= l - 1 by XREAL_0:def 2;
then (n + 2) + 1 <= (l - 1) + 1 by XREAL_1:6;
then n + 3 <= n by A6, XXREAL_0:2;
then (n + 3) - n <= n - n by XREAL_1:9;
then 3 <= 0 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

thus (l * k) mod (n + 2) = 1 by A9; :: thesis: verum