let n be natural number ; :: thesis: ( n + 2 is prime implies for l being natural number st l in Seg n & l <> 1 holds
ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
assume A1: n + 2 is prime ; :: thesis: for l being natural number st l in Seg n & l <> 1 holds
ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
let l be natural number ; :: thesis: ( l in Seg n & l <> 1 implies ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
assume A2: l in Seg n ; :: thesis: ( not l <> 1 or ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
then A3: ( 1 <= l & l <= n ) by FINSEQ_1:3;
then A4: l < n + 1 by NAT_1:13;
then A5: l + 1 < (n + 1) + 1 by XREAL_1:8;
A6: 1 - 1 <= l - 1 by A3, XREAL_1:11;
A7: 1 + n < 2 + n by XREAL_1:8;
then A8: l < n + 2 by A4, XXREAL_0:2;
then l - 1 < (n + 2) - 1 by XREAL_1:11;
then l - 1 < n + 2 by A7, XXREAL_0:2;
then A9: l -' 1 < n + 2 by XREAL_0:def 2;
assume A10: l <> 1 ; :: thesis: ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
reconsider l' = l as Element of NAT by ORDINAL1:def 13;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
reconsider n'' = n' + 2 as Element of NAT ;
( n'' is prime & l' < n' + 2 & 1 < n' + 2 & l' <> 0 ) by A2, A1, A7, A4, XXREAL_0:2, INT_2:def 5, FINSEQ_1:3;
then consider k being Element of NAT such that
A11: ( (k * l') mod (n' + 2) = 1 & k < n' + 2 ) by IDEA_1:1;
take k ; :: thesis: ( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
k <> 0 by A11, NAT_D:26;
then A12: k >= 0 + 1 by NAT_1:13;
k < (n + 1) + 1 by A11;
then A13: k <= n + 1 by NAT_1:13;
A14: n + 2 > 1 by A8, A3, XXREAL_0:2;
k <> n + 1

proof

assume k = n + 1 ; :: thesis: contradiction
then ((n + 1) * l) mod (n + 2) = 1 mod (n + 2) by A11, A14, 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 A5, NAT_D:24 ;
hence contradiction ; :: thesis: verum

end;

then k < n + 1 by A13, XXREAL_0:1;
then k <= n by NAT_1:13;
hence k in Seg n by A12; :: thesis: ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
thus A15: 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 A11, NAT_D:14;
then 0 = (l - 1) mod (n + 2) by INT_4:22
.= (l -' 1) mod (n + 2) by A6, XREAL_0:def 2
.= l -' 1 by A9, NAT_D:24
.= l - 1 by A6, XREAL_0:def 2 ;
hence contradiction by A10; :: thesis: verum

end;

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

proof

assume A16: k = l ; :: thesis: contradiction
then (l * l) mod (n + 2) = 1 mod (n + 2) by A11, A14, NAT_D:14;
then 0 = ((l * l) - 1) mod (n + 2) by INT_4:22;
then A17: n + 2 divides (l + 1) * (l - 1) by INT_1:89;

per cases ( n + 2 divides l + 1 or n + 2 divides l - 1 ) by A1, A17, 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:11;
hence contradiction by A4; :: thesis: verum

end;

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

then A18: n + 2 divides l -' 1 by A6, XREAL_0:def 2;

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

suppose l = 1 ; :: thesis: contradiction

hence contradiction by A15, A16; :: thesis: verum

end;

suppose l <> 1 ; :: thesis: contradiction

then l > 1 by A3, XXREAL_0:1;
then l - 1 > 1 - 1 by XREAL_1:11;
then l -' 1 > 0 by XREAL_0:def 2;
then n + 2 <= l -' 1 by A18, NAT_D:7;
then n + 2 <= l - 1 by XREAL_0:def 2;
then (n + 2) + 1 <= (l - 1) + 1 by XREAL_1:8;
then n + 3 <= n by A3, XXREAL_0:2;
then (n + 3) - n <= n - n by XREAL_1:11;
then 3 <= 0 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

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