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