let n be natural number ; :: 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 natural number st l in rng f & l <> 1 holds
ex k being natural number st
( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds
(Product f) mod (n + 2) = 1
defpred S₁[ natural number ] 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 natural number st l in rng f & l <> 1 holds
ex k being natural number 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 natural number st l in rng f & l <> 1 holds
ex k being natural number 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 natural number st ( for n9 being natural number st n9 < k9 holds
S₁[n9] ) holds
S₁[k9]

proof

let k9 be natural number ; :: thesis: ( ( for n9 being natural number st n9 < k9 holds
S₁[n9] ) implies S₁[k9] )
assume A2: for n9 being natural number 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 natural number st l in rng f & l <> 1 holds
ex k being natural number 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 natural number st
( l in rng f & l <> 1 & ( for k being natural number 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 natural number st
( l in rng f & l <> 1 & ( for k being natural number 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 natural number st
( l in rng f & l <> 1 & ( for k being natural number 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 natural number st
( l in rng f & l <> 1 & ( for k being natural number 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 natural number st l in rng f & l <> 1 holds
ex k being natural number 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;
dom f <> {} by A3, A10, CARD_1:27, RELAT_1:41;
then consider x1 being set 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, XBOOLE_1:1;
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 natural number st l in rng (Del (f,x1)) & l <> 1 holds
ex k being natural number st
( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

proof

let l be natural number ; :: thesis: ( l in rng (Del (f,x1)) & l <> 1 implies ex k being natural number 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 natural number st
( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) )
assume l <> 1 ; :: thesis: ex k being natural number st
( k in rng (Del (f,x1)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
then consider k being natural number 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);
set l = f . x1;
A24: f . x1 in rng f by A11, FUNCT_1:3;
then consider k being natural number such that
A25: k in rng f and
k <> 1 and
A26: k <> f . x1 and
A27: ((f . x1) * k) mod (n + 2) = 1 by A7, A23;
k in rng (Del (f,x1)) by A25, A26, Th8;
then consider x2 being set such that
A28: x2 in dom (Del (f,x1)) and
A29: k = (Del (f,x1)) . x2 by FUNCT_1:def 3;
reconsider x2 = x2 as Element of NAT by A28;
A30: rng (Del ((Del (f,x1)),x2)) c= rng (Del (f9,x1)) by FINSEQ_3:106;
then A31: rng (Del ((Del (f,x1)),x2)) c= Seg n by A15, XBOOLE_1:1;
A32: for l being natural number st l in rng (Del ((Del (f,x1)),x2)) & l <> 1 holds
ex k being natural number st
( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

proof

A33: 1 <= f . x1 by A5, A24, FINSEQ_1:1;
A34: 0 + n < 2 + n by XREAL_1:6;
f . x1 <= n by A5, A24, FINSEQ_1:1;
then A35: n + 2 > f . x1 by A34, XXREAL_0:2;
k <= n by A5, A25, FINSEQ_1:1;
then A36: n + 2 > k by A34, XXREAL_0:2;
let l9 be natural number ; :: thesis: ( l9 in rng (Del ((Del (f,x1)),x2)) & l9 <> 1 implies ex k being natural number st
( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) )
A37: 0 + n < 2 + n by XREAL_1:6;
assume A38: l9 in rng (Del ((Del (f,x1)),x2)) ; :: thesis: ( not l9 <> 1 or ex k being natural number st
( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 ) )
then A39: l9 in rng (Del (f9,x1)) by A30;
then l9 in rng f by A14;
then A40: l9 <= n by A5, FINSEQ_1:1;
assume l9 <> 1 ; :: thesis: ex k being natural number st
( k in rng (Del ((Del (f,x1)),x2)) & k <> 1 & k <> l9 & (l9 * k) mod (n + 2) = 1 )
then consider k9 being natural number such that
A41: k9 in rng f and
A42: ( k9 <> 1 & k9 <> l9 ) and
A43: (l9 * k9) mod (n + 2) = 1 by A7, A14, A39;
take k9 ; :: thesis: ( k9 in rng (Del ((Del (f,x1)),x2)) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod (n + 2) = 1 )
A44: 1 <= k by A5, A25, 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 A45: 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 A46: k9 in rng (Del (f,x1)) ; :: thesis: contradiction

A47: l9 < n + 2 by A40, A37, XXREAL_0:2;
(k * (f . x1)) mod (n + 2) = (k * l9) mod (n + 2) by A27, A29, A43, A45, A46, Th8;
then l9 = f . x1 by A4, A44, A36, A35, A47, Th20;
hence contradiction by A6, A11, A30, A38, Th7; :: thesis: verum

end;

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

A49: l9 < n + 2 by A40, A37, XXREAL_0:2;
((f . x1) * k) mod (n + 2) = ((f . x1) * l9) mod (n + 2) by A27, A41, A43, A48, Th8;
then (Del (f,x1)) . x2 in rng (Del ((Del (f,x1)),x2)) by A4, A29, A38, A33, A36, A35, A49, Th20;
hence contradiction by A6, A28, Th6, Th7; :: thesis: verum

end;

end;

end;

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

end;

set n299 = len (Del ((Del (f,x1)),x2));
A50: 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 A28, FINSEQ_3:104;
then A51: len (Del ((Del (f,x1)),x2)) < k9 by A3, A12, A16, A50, XXREAL_0:2;
A52: 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 A28, Lm8;
then (Product (Del ((Del (f,x1)),x2))) * (k * (f . x1)) = Product f by A13, A29;
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, A27, A31, A52, A32, A51 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

for n9 being natural number 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 natural number st l in rng f & l <> 1 holds
ex k being natural number st
( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) implies (Product f) mod (n + 2) = 1 ) ; :: thesis: verum