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₁[ 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₁[n9] ) holds
S₁[k9]

proof

let k9 be Nat; :: thesis: ( ( for n9 being Nat st n9 < k9 holds
S₁[n9] ) implies S₁[k9] )
assume A2: for n9 being Nat st n9 < k9 holds
S₁[n9] ; :: thesis: S₁[k9]
thus S₁[k9] :: thesis: verum

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

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

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;

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;

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

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 )

proof

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;

hence (Product f) mod (n + 2) = 1 by A2, A3, A4, A13, A15, A17, A12, A16, A18; :: thesis: verum

end;

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 )

proof

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 )

proof

assume A46: not k9 in rng (Del ((Del (f,x1)),x2)) ; :: thesis: contradiction

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

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;

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;

end;

end;

thus ( k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 ) by A43, A44; :: thesis: verum

end;

set n299 = len (Del ((Del (f,x1)),x2));
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;

end;

end;

end;

end;

end;

for n9 being Nat holds S₁[n9] from NAT_1:sch 4(A1);
then S₁[ 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