let p be FinSequence; ( len p is prime & ex i being Nat st
( 0 < i & i < len p & p = (p /^ i) ^ (p | i) ) implies rng p c= {(p . 1)} )
set L = len p;
assume A1:
len p is prime
; ( for i being Nat holds
( not 0 < i or not i < len p or not p = (p /^ i) ^ (p | i) ) or rng p c= {(p . 1)} )
reconsider P = p as FinSequence of (rng p) \/ {1} by XBOOLE_1:7, FINSEQ_1:def 4;
given j being Nat such that A2:
0 < j
and
A3:
j < len p
and
A4:
p = (p /^ j) ^ (p | j)
; rng p c= {(p . 1)}
defpred S1[ Nat] means p . 1 = p . (((j * $1) mod (len p)) + 1);
set p1j = p /^ j;
set pj = p | j;
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
set jk =
(j * k) mod (len p);
j * (k + 1) = (j * k) + j
;
then A7:
(j * (k + 1)) mod (len p) = (((j * k) mod (len p)) + j) mod (len p)
by NAT_D:23;
A8:
len (p | j) = j
by A3, FINSEQ_1:59;
A9:
len (p /^ j) = (len p) - j
by A3, RFINSEQ:def 1;
((j * k) mod (len p)) + 1
<= len p
by NAT_D:1, A3, NAT_1:13;
then A10:
((j * k) mod (len p)) + 1
in dom p
by NAT_1:11, FINSEQ_3:25;
per cases
( ((j * k) mod (len p)) + 1 in dom (p /^ j) or ex n being Nat st
( n in dom (p | j) & ((j * k) mod (len p)) + 1 = (len (p /^ j)) + n ) )
by A4, A10, FINSEQ_1:25;
suppose
ex
n being
Nat st
(
n in dom (p | j) &
((j * k) mod (len p)) + 1
= (len (p /^ j)) + n )
;
S1[k + 1]then consider n being
Nat such that A13:
n in dom (p | j)
and A14:
((j * k) mod (len p)) + 1
= (len (p /^ j)) + n
;
len (p | j) >= n
by A13, FINSEQ_3:25;
then A15:
n < len p
by A8, A3, XXREAL_0:2;
reconsider n1 =
n - 1 as
Nat by A13, FINSEQ_3:25, NAT_1:21;
n1 < n1 + 1
by NAT_1:13;
then A16:
n1 < len p
by A15, XXREAL_0:2;
((j * k) mod (len p)) + j = (1 * (len p)) + n1
by A14, A9;
then A17:
(((j * k) mod (len p)) + j) mod (len p) =
n1 mod (len p)
by NAT_D:21
.=
n1
by A16, NAT_D:24
;
p . (((j * k) mod (len p)) + 1) =
(p | j) . n
by A4, A13, A14, FINSEQ_1:def 7
.=
p . n
by A13, FUNCT_1:47
;
hence
S1[
k + 1]
by A17, A7, A6;
verum end;
end;
(j * 0) mod (len p) = 0
by NAT_D:26;
then A18:
S1[ 0 ]
;
A19:
for k being Nat holds S1[k]
from NAT_1:sch 2(A18, A5);
let y be object ; TARSKI:def 3 ( not y in rng p or y in {(p . 1)} )
assume
y in rng p
; y in {(p . 1)}
then consider m being object such that
A20:
m in dom p
and
A21:
p . m = y
by FUNCT_1:def 3;
reconsider m = m as Nat by A20;
A22:
m <= len p
by A20, FINSEQ_3:25;
reconsider m1 = m - 1 as Nat by A20, FINSEQ_3:25, NAT_1:21;