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

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 )

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

k < (n + 1) + 1
by A10;
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;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

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

thus
k <> l
:: thesis: (l * k) mod (n + 2) = 1
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;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

proof

thus
(l * k) mod (n + 2) = 1
by A9; :: thesis: verum
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;

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

end;

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;then (n + 2) - 1 <= (l + 1) - 1 by XREAL_1:9;

hence contradiction by A7; :: thesis: verum

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

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

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

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