let n be Nat; :: thesis: for f being FinSequence of NAT st n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds

(Product f) mod (n + 2) = 1

defpred S_{1}[ Nat] means for f being FinSequence of NAT st len f = $1 & n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds

(Product f) mod (n + 2) = 1;

let f be FinSequence of NAT ; :: thesis: ( n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 )

set n9 = len f;

A1: for k9 being Nat st ( for n9 being Nat st n9 < k9 holds

S_{1}[n9] ) holds

S_{1}[k9]
_{1}[n9]
from NAT_1:sch 4(A1);

then S_{1}[ len f]
;

hence ( n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 ) ; :: thesis: verum

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds

(Product f) mod (n + 2) = 1

defpred S

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds

(Product f) mod (n + 2) = 1;

let f be FinSequence of NAT ; :: thesis: ( n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 )

set n9 = len f;

A1: for k9 being Nat st ( for n9 being Nat st n9 < k9 holds

S

S

proof

for n9 being Nat holds S
let k9 be Nat; :: thesis: ( ( for n9 being Nat st n9 < k9 holds

S_{1}[n9] ) implies S_{1}[k9] )

assume A2: for n9 being Nat st n9 < k9 holds

S_{1}[n9]
; :: thesis: S_{1}[k9]

thus S_{1}[k9]
:: thesis: verum

end;S

assume A2: for n9 being Nat st n9 < k9 holds

S

thus S

proof

let f be FinSequence of NAT ; :: thesis: ( len f = k9 & n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 )

assume A3: len f = k9 ; :: thesis: ( not n + 2 is prime or not rng f c= Seg n or not f is one-to-one or ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A4: n + 2 is prime ; :: thesis: ( not rng f c= Seg n or not f is one-to-one or ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A5: rng f c= Seg n ; :: thesis: ( not f is one-to-one or ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A6: f is one-to-one ; :: thesis: ( ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A7: for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ; :: thesis: (Product f) mod (n + 2) = 1

end;ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 )

assume A3: len f = k9 ; :: thesis: ( not n + 2 is prime or not rng f c= Seg n or not f is one-to-one or ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A4: n + 2 is prime ; :: thesis: ( not rng f c= Seg n or not f is one-to-one or ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A5: rng f c= Seg n ; :: thesis: ( not f is one-to-one or ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A6: f is one-to-one ; :: thesis: ( ex l being Nat st

( l in rng f & l <> 1 & ( for k being Nat holds

( not k in rng f or not k <> 1 or not k <> l or not (l * k) mod (n + 2) = 1 ) ) ) or (Product f) mod (n + 2) = 1 )

assume A7: for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ; :: thesis: (Product f) mod (n + 2) = 1

per cases
( k9 = 0 or k9 <> 0 )
;

end;

suppose A8:
k9 = 0
; :: thesis: (Product f) mod (n + 2) = 1

A9:
0 + 1 < (n + 1) + 1
by XREAL_1:6;

f = <*> NAT by A3, A8;

then Product f = 1 by RVSUM_1:94;

hence (Product f) mod (n + 2) = 1 by A9, NAT_D:24; :: thesis: verum

end;f = <*> NAT by A3, A8;

then Product f = 1 by RVSUM_1:94;

hence (Product f) mod (n + 2) = 1 by A9, NAT_D:24; :: thesis: verum

suppose A10:
k9 <> 0
; :: thesis: (Product f) mod (n + 2) = 1

reconsider f9 = f as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

dom f <> {} by A3, A10, CARD_1:27, RELAT_1:41;

then consider x1 being object such that

A11: x1 in dom f by XBOOLE_0:def 1;

reconsider x1 = x1 as Element of NAT by A11;

A12: ex m being Nat st

( len f = m + 1 & len (Del (f,x1)) = m ) by A11, FINSEQ_3:104;

A13: (Product (Del (f9,x1))) * (f9 . x1) = Product f by A11, Lm8;

A14: rng (Del (f,x1)) c= rng f by FINSEQ_3:106;

then A15: rng (Del (f,x1)) c= Seg n by A5;

set n19 = len (Del (f,x1));

A16: 0 + (len (Del (f,x1))) < 1 + (len (Del (f,x1))) by XREAL_1:6;

A17: Del (f,x1) is one-to-one by A6, Th6;

end;dom f <> {} by A3, A10, CARD_1:27, RELAT_1:41;

then consider x1 being object such that

A11: x1 in dom f by XBOOLE_0:def 1;

reconsider x1 = x1 as Element of NAT by A11;

A12: ex m being Nat st

( len f = m + 1 & len (Del (f,x1)) = m ) by A11, FINSEQ_3:104;

A13: (Product (Del (f9,x1))) * (f9 . x1) = Product f by A11, Lm8;

A14: rng (Del (f,x1)) c= rng f by FINSEQ_3:106;

then A15: rng (Del (f,x1)) c= Seg n by A5;

set n19 = len (Del (f,x1));

A16: 0 + (len (Del (f,x1))) < 1 + (len (Del (f,x1))) by XREAL_1:6;

A17: Del (f,x1) is one-to-one by A6, Th6;

per cases
( f9 . x1 = 1 or f9 . x1 <> 1 )
;

end;

suppose A18:
f9 . x1 = 1
; :: thesis: (Product f) mod (n + 2) = 1

for l being Nat st l in rng (Del (f,x1)) & l <> 1 holds

ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

end;ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

proof

hence
(Product f) mod (n + 2) = 1
by A2, A3, A4, A13, A15, A17, A12, A16, A18; :: thesis: verum
let l be Nat; :: thesis: ( l in rng (Del (f,x1)) & l <> 1 implies ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )

assume A19: l in rng (Del (f,x1)) ; :: thesis: ( not l <> 1 or ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )

assume l <> 1 ; :: thesis: ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

then consider k being Nat such that

A20: k in rng f and

A21: k <> 1 and

A22: ( k <> l & (l * k) mod (n + 2) = 1 ) by A7, A14, A19;

take k ; :: thesis: ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

thus k in rng (Del (f,x1)) by A18, A20, A21, Th8; :: thesis: ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

thus ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) by A21, A22; :: thesis: verum

end;( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )

assume A19: l in rng (Del (f,x1)) ; :: thesis: ( not l <> 1 or ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )

assume l <> 1 ; :: thesis: ex k being Nat st

( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

then consider k being Nat such that

A20: k in rng f and

A21: k <> 1 and

A22: ( k <> l & (l * k) mod (n + 2) = 1 ) by A7, A14, A19;

take k ; :: thesis: ( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

thus k in rng (Del (f,x1)) by A18, A20, A21, Th8; :: thesis: ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

thus ( k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) by A21, A22; :: thesis: verum

suppose A23:
f9 . x1 <> 1
; :: thesis: (Product f) mod (n + 2) = 1

set f99 = Del (f,x1);

A24: Del (f,x1) is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

set l = f . x1;

A25: f . x1 in rng f by A11, FUNCT_1:3;

then consider k being Nat such that

A26: k in rng f and

k <> 1 and

A27: k <> f . x1 and

A28: ((f . x1) * k) mod (n + 2) = 1 by A7, A23;

k in rng (Del (f,x1)) by A26, A27, Th8;

then consider x2 being object such that

A29: x2 in dom (Del (f,x1)) and

A30: k = (Del (f,x1)) . x2 by FUNCT_1:def 3;

reconsider x2 = x2 as Element of NAT by A29;

A31: rng (Del ((Del (f,x1)),x2)) c= rng (Del (f9,x1)) by FINSEQ_3:106;

then A32: rng (Del ((Del (f,x1)),x2)) c= Seg n by A15;

A33: for l being Nat st l in rng (Del ((Del (f,x1)),x2)) & l <> 1 holds

ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

A51: 0 + (len (Del ((Del (f,x1)),x2))) < 1 + (len (Del ((Del (f,x1)),x2))) by XREAL_1:6;

ex m being Nat st

( len (Del (f9,x1)) = m + 1 & len (Del ((Del (f,x1)),x2)) = m ) by A29, FINSEQ_3:104;

then A52: len (Del ((Del (f,x1)),x2)) < k9 by A3, A12, A16, A51, XXREAL_0:2;

A53: Del ((Del (f,x1)),x2) is one-to-one by A17, Th6;

(Product (Del ((Del (f,x1)),x2))) * ((Del (f,x1)) . x2) = Product (Del (f,x1)) by A29, Lm8, A24;

then (Product (Del ((Del (f,x1)),x2))) * (k * (f . x1)) = Product f by A13, A30;

hence (Product f) mod (n + 2) = ((Product (Del ((Del (f,x1)),x2))) * ((k * (f . x1)) mod (n + 2))) mod (n + 2) by EULER_2:7

.= 1 by A2, A4, A28, A32, A53, A33, A52 ;

:: thesis: verum

end;A24: Del (f,x1) is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

set l = f . x1;

A25: f . x1 in rng f by A11, FUNCT_1:3;

then consider k being Nat such that

A26: k in rng f and

k <> 1 and

A27: k <> f . x1 and

A28: ((f . x1) * k) mod (n + 2) = 1 by A7, A23;

k in rng (Del (f,x1)) by A26, A27, Th8;

then consider x2 being object such that

A29: x2 in dom (Del (f,x1)) and

A30: k = (Del (f,x1)) . x2 by FUNCT_1:def 3;

reconsider x2 = x2 as Element of NAT by A29;

A31: rng (Del ((Del (f,x1)),x2)) c= rng (Del (f9,x1)) by FINSEQ_3:106;

then A32: rng (Del ((Del (f,x1)),x2)) c= Seg n by A15;

A33: for l being Nat st l in rng (Del ((Del (f,x1)),x2)) & l <> 1 holds

ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

proof

set n299 = len (Del ((Del (f,x1)),x2));
A34:
1 <= f . x1
by A5, A25, FINSEQ_1:1;

A35: 0 + n < 2 + n by XREAL_1:6;

f . x1 <= n by A5, A25, FINSEQ_1:1;

then A36: n + 2 > f . x1 by A35, XXREAL_0:2;

k <= n by A5, A26, FINSEQ_1:1;

then A37: n + 2 > k by A35, XXREAL_0:2;

let l9 be Nat; :: thesis: ( l9 in rng (Del ((Del (f,x1)),x2)) & l9 <> 1 implies ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) )

A38: 0 + n < 2 + n by XREAL_1:6;

assume A39: l9 in rng (Del ((Del (f,x1)),x2)) ; :: thesis: ( not l9 <> 1 or ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) )

then A40: l9 in rng (Del (f9,x1)) by A31;

then l9 in rng f by A14;

then A41: l9 <= n by A5, FINSEQ_1:1;

assume l9 <> 1 ; :: thesis: ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 )

then consider k9 being Nat such that

A42: k9 in rng f and

A43: ( k9 <> 1 & k9 <> l9 ) and

A44: (l9 * k9) mod (n + 2) = 1 by A7, A14, A40;

take k9 ; :: thesis: ( k9 in rng (Del ((Del (f,x1)),x2)) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 )

A45: 1 <= k by A5, A26, FINSEQ_1:1;

thus k9 in rng (Del ((Del (f,x1)),x2)) :: thesis: ( k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 )

end;A35: 0 + n < 2 + n by XREAL_1:6;

f . x1 <= n by A5, A25, FINSEQ_1:1;

then A36: n + 2 > f . x1 by A35, XXREAL_0:2;

k <= n by A5, A26, FINSEQ_1:1;

then A37: n + 2 > k by A35, XXREAL_0:2;

let l9 be Nat; :: thesis: ( l9 in rng (Del ((Del (f,x1)),x2)) & l9 <> 1 implies ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) )

A38: 0 + n < 2 + n by XREAL_1:6;

assume A39: l9 in rng (Del ((Del (f,x1)),x2)) ; :: thesis: ( not l9 <> 1 or ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) )

then A40: l9 in rng (Del (f9,x1)) by A31;

then l9 in rng f by A14;

then A41: l9 <= n by A5, FINSEQ_1:1;

assume l9 <> 1 ; :: thesis: ex k being Nat st

( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 )

then consider k9 being Nat such that

A42: k9 in rng f and

A43: ( k9 <> 1 & k9 <> l9 ) and

A44: (l9 * k9) mod (n + 2) = 1 by A7, A14, A40;

take k9 ; :: thesis: ( k9 in rng (Del ((Del (f,x1)),x2)) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 )

A45: 1 <= k by A5, A26, FINSEQ_1:1;

thus k9 in rng (Del ((Del (f,x1)),x2)) :: thesis: ( k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 )

proof

thus
( k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 )
by A43, A44; :: thesis: verum
assume A46:
not k9 in rng (Del ((Del (f,x1)),x2))
; :: thesis: contradiction

end;per cases
( k9 in rng (Del (f,x1)) or not k9 in rng (Del (f,x1)) )
;

end;

suppose A47:
k9 in rng (Del (f,x1))
; :: thesis: contradiction

A48:
l9 < n + 2
by A41, A38, XXREAL_0:2;

(k * (f . x1)) mod (n + 2) = (k * l9) mod (n + 2) by A28, A30, A44, A46, A47, Th8;

then l9 = f . x1 by A4, A45, A37, A36, A48, Th20;

hence contradiction by A6, A11, A31, A39, Th7; :: thesis: verum

end;(k * (f . x1)) mod (n + 2) = (k * l9) mod (n + 2) by A28, A30, A44, A46, A47, Th8;

then l9 = f . x1 by A4, A45, A37, A36, A48, Th20;

hence contradiction by A6, A11, A31, A39, Th7; :: thesis: verum

suppose A49:
not k9 in rng (Del (f,x1))
; :: thesis: contradiction

A50:
l9 < n + 2
by A41, A38, XXREAL_0:2;

((f . x1) * k) mod (n + 2) = ((f . x1) * l9) mod (n + 2) by A28, A42, A44, A49, Th8;

then (Del (f,x1)) . x2 in rng (Del ((Del (f,x1)),x2)) by A4, A30, A39, A34, A37, A36, A50, Th20;

hence contradiction by A6, A29, Th6, Th7; :: thesis: verum

end;((f . x1) * k) mod (n + 2) = ((f . x1) * l9) mod (n + 2) by A28, A42, A44, A49, Th8;

then (Del (f,x1)) . x2 in rng (Del ((Del (f,x1)),x2)) by A4, A30, A39, A34, A37, A36, A50, Th20;

hence contradiction by A6, A29, Th6, Th7; :: thesis: verum

A51: 0 + (len (Del ((Del (f,x1)),x2))) < 1 + (len (Del ((Del (f,x1)),x2))) by XREAL_1:6;

ex m being Nat st

( len (Del (f9,x1)) = m + 1 & len (Del ((Del (f,x1)),x2)) = m ) by A29, FINSEQ_3:104;

then A52: len (Del ((Del (f,x1)),x2)) < k9 by A3, A12, A16, A51, XXREAL_0:2;

A53: Del ((Del (f,x1)),x2) is one-to-one by A17, Th6;

(Product (Del ((Del (f,x1)),x2))) * ((Del (f,x1)) . x2) = Product (Del (f,x1)) by A29, Lm8, A24;

then (Product (Del ((Del (f,x1)),x2))) * (k * (f . x1)) = Product f by A13, A30;

hence (Product f) mod (n + 2) = ((Product (Del ((Del (f,x1)),x2))) * ((k * (f . x1)) mod (n + 2))) mod (n + 2) by EULER_2:7

.= 1 by A2, A4, A28, A32, A53, A33, A52 ;

:: thesis: verum

then S

hence ( n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being Nat st l in rng f & l <> 1 holds

ex k being Nat st

( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 ) ; :: thesis: verum