let k, m, n be Nat; :: thesis: for p being Prime st 1 <= k & k <= m & m <= n holds
( p divides Product (mid ((primesFinS n),k,m)) iff ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) )
let p be Prime; :: thesis: ( 1 <= k & k <= m & m <= n implies ( p divides Product (mid ((primesFinS n),k,m)) iff ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) ) )
assume A1: ( 1 <= k & k <= m & m <= n ) ; :: thesis: ( p divides Product (mid ((primesFinS n),k,m)) iff ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) )
A2: len (primesFinS n) = n by NUMBER13:def 1;
A3: ( 1 <= m & k <= n ) by A1, XXREAL_0:2;
set M = mid ((primesFinS n),k,m);
A4: m -' k = m - k by A1, XREAL_1:233;
A5: len (mid ((primesFinS n),k,m)) = (m -' k) + 1 by A1, A2, A3, FINSEQ_6:118;
thus ( p divides Product (mid ((primesFinS n),k,m)) implies ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) ) :: thesis: ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m implies p divides Product (mid ((primesFinS n),k,m)) )

proof

assume p divides Product (mid ((primesFinS n),k,m)) ; :: thesis: ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m )
then consider i being Nat such that
A6: ( i in dom (mid ((primesFinS n),k,m)) & p divides (mid ((primesFinS n),k,m)) . i ) by HILB10_5:3;
A7: p > 1 by INT_2:def 4;
A8: ( 1 <= i & i <= len (mid ((primesFinS n),k,m)) ) by A6, FINSEQ_3:25;
then A9: (mid ((primesFinS n),k,m)) . i = (primesFinS n) . ((i + k) -' 1) by A1, A2, A3, FINSEQ_6:118;
A10: 1 + 1 <= i + k by A1, A8, XREAL_1:7;
then A11: (i + k) -' 1 = (i + k) - 1 by XXREAL_0:2, XREAL_1:233;
then reconsider ik = ((i + k) -' 1) - 1 as Element of NAT by NAT_1:21, A10, XREAL_1:19;
A12: k + 0 <= k + (i - 1) by A8, XREAL_1:6;
i + k <= ((m - k) + 1) + k by A8, A4, A5, XREAL_1:7;
then A13: (i + k) -' 1 <= (m + 1) - 1 by A11, XREAL_1:9;
then ik + 1 <= m ;
then ik < m by NAT_1:13;
then ik < n by A1, XXREAL_0:2;
then (primesFinS n) . (ik + 1) = primenumber ik by NUMBER13:def 1;
then p = primenumber ik by A7, INT_2:def 4, A6, A9;
then ik = primeindex p by NUMBER10:def 4;
hence ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) by A12, A11, A13; :: thesis: verum

end;

set I = primeindex p;
assume A14: ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) ; :: thesis: p divides Product (mid ((primesFinS n),k,m))
then 1 + (primeindex p) <= n by A1, XXREAL_0:2;
then primeindex p < n by NAT_1:13;
then (primesFinS n) . ((primeindex p) + 1) = primenumber (primeindex p) by NUMBER13:def 1;
then A15: (primesFinS n) . ((primeindex p) + 1) = p by NUMBER10:def 4;
reconsider Ik = ((primeindex p) + 1) - k as Element of NAT by A14, NAT_1:21;
A16: ((1 + Ik) + k) -' 1 = (((primeindex p) + 1) + 1) -' 1
.= (primeindex p) + 1 ;
Ik <= m - k by A14, XREAL_1:9;
then A17: ( 1 <= Ik + 1 & Ik + 1 <= len (mid ((primesFinS n),k,m)) ) by A5, A4, XREAL_1:6, NAT_1:11;
then A18: (mid ((primesFinS n),k,m)) . (1 + Ik) = (primesFinS n) . (1 + (primeindex p)) by A16, A1, A2, A3, FINSEQ_6:118;
Ik + 1 in dom (mid ((primesFinS n),k,m)) by A17, FINSEQ_3:25;
then (mid ((primesFinS n),k,m)) . (1 + Ik) in rng (mid ((primesFinS n),k,m)) by FUNCT_1:def 3;
hence p divides Product (mid ((primesFinS n),k,m)) by A15, A18, NAT_3:7; :: thesis: verum