let s be Nat; for k, n being non zero Nat st k <> n & n <= s & k <= s holds
primenumber (k - 1) divides (sequenceA s) . n
let k, n be non zero Nat; ( k <> n & n <= s & k <= s implies primenumber (k - 1) divides (sequenceA s) . n )
assume that
A1:
k <> n
and
A2:
n <= s
and
A3:
k <= s
; primenumber (k - 1) divides (sequenceA s) . n
reconsider s = s as non zero Nat by A2;
set A = sequenceA s;
set p = primenumber (k - 1);
set r = primenumber (n - 1);
set g = PrimeNumbersFS s;
A4:
0 + 1 <= k
by NAT_1:13;
A5:
len (PrimeNumbersFS s) = s
by Th42;
then A6:
k in dom (PrimeNumbersFS s)
by A3, A4, FINSEQ_3:25;
A7:
(PrimeNumbersFS s) . k = primenumber (k - 1)
by A3, Th44;
n - 1 < s - 0
by A2, XREAL_1:8;
then reconsider e = (Product (PrimeNumbersFS s)) / (primenumber (n - 1)) as Nat by Th45;
set y = CRT (0,e,(- 1),(primenumber (n - 1)));
1 <= n
by NAT_1:14;
then A8:
n in dom (PrimeNumbersFS s)
by A5, A2, FINSEQ_3:25;
A9:
(sequenceA s) . n = (CRT (0,e,(- 1),(primenumber (n - 1)))) + (Product (PrimeNumbersFS s))
by A2, Def5;
A10:
(PrimeNumbersFS s) . n = primenumber (n - 1)
by A2, Th44;
then
primenumber (n - 1),e are_coprime
by A8, INT_6:25;
then
CRT (0,e,(- 1),(primenumber (n - 1))) solves_CRT 0 ,e, - 1, primenumber (n - 1)
by NUMBER14:def 2;
then A11:
CRT (0,e,(- 1),(primenumber (n - 1))), 0 are_congruent_mod e
;
e divides Product (PrimeNumbersFS s)
by NUMBER14:3;
then A12:
e divides (CRT (0,e,(- 1),(primenumber (n - 1)))) + (Product (PrimeNumbersFS s))
by A11, NAT_D:8;
consider z being Integer such that
A13:
z * ((PrimeNumbersFS s) . k) = (Product (PrimeNumbersFS s)) / ((PrimeNumbersFS s) . n)
by A1, A6, INT_6:12;
(PrimeNumbersFS s) . k divides z * ((PrimeNumbersFS s) . k)
;
hence
primenumber (k - 1) divides (sequenceA s) . n
by A7, A9, A10, A12, A13, INT_2:9; verum