let k, m, n be Nat; ( 1 <= k & k <= m & m <= n implies PrimeDivisors (Product (mid ((primesFinS n),k,m))) = rng (mid ((primesFinS n),k,m)) )
assume A1:
( 1 <= k & k <= m & m <= n )
; PrimeDivisors (Product (mid ((primesFinS n),k,m))) = rng (mid ((primesFinS n),k,m))
set P = primesFinS n;
set M = mid ((primesFinS n),k,m);
A2:
PrimeDivisors (Product (mid ((primesFinS n),k,m))) c= rng (mid ((primesFinS n),k,m))
proof
let x be
object ;
TARSKI:def 3 ( not x in PrimeDivisors (Product (mid ((primesFinS n),k,m))) or x in rng (mid ((primesFinS n),k,m)) )
assume A3:
x in PrimeDivisors (Product (mid ((primesFinS n),k,m)))
;
x in rng (mid ((primesFinS n),k,m))
x in { k where k is Prime : k divides Product (mid ((primesFinS n),k,m)) }
by A3, NUMBER12:def 3;
then consider p being
Prime such that A4:
(
x = p &
p divides Product (mid ((primesFinS n),k,m)) )
;
A5:
(
k <= 1
+ (primeindex p) & 1
+ (primeindex p) <= m )
by A1, A4, Th3;
set I =
primeindex p;
A6:
len (primesFinS n) = n
by NUMBER13:def 1;
A7:
( 1
<= m &
k <= n )
by A1, XXREAL_0:2;
set M =
mid (
(primesFinS n),
k,
m);
A8:
m -' k = m - k
by A1, XREAL_1:233;
A9:
len (mid ((primesFinS n),k,m)) = (m -' k) + 1
by A1, A6, A7, FINSEQ_6:118;
1
+ (primeindex p) <= n
by A5, 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 A10:
(primesFinS n) . ((primeindex p) + 1) = p
by NUMBER10:def 4;
reconsider Ik =
((primeindex p) + 1) - k as
Element of
NAT by A5, NAT_1:21;
A11:
((1 + Ik) + k) -' 1 =
(((primeindex p) + 1) + 1) -' 1
.=
(primeindex p) + 1
;
Ik <= m - k
by A5, XREAL_1:9;
then A12:
( 1
<= Ik + 1 &
Ik + 1
<= len (mid ((primesFinS n),k,m)) )
by A9, A8, XREAL_1:7, NAT_1:11;
A13:
(mid ((primesFinS n),k,m)) . (1 + Ik) = p
by A10, A12, A11, A1, A6, A7, FINSEQ_6:118;
Ik + 1
in dom (mid ((primesFinS n),k,m))
by A12, FINSEQ_3:25;
hence
x in rng (mid ((primesFinS n),k,m))
by A4, A13, FUNCT_1:def 3;
verum
end;
rng (mid ((primesFinS n),k,m)) c= PrimeDivisors (Product (mid ((primesFinS n),k,m)))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (mid ((primesFinS n),k,m)) or y in PrimeDivisors (Product (mid ((primesFinS n),k,m))) )
assume A14:
y in rng (mid ((primesFinS n),k,m))
;
y in PrimeDivisors (Product (mid ((primesFinS n),k,m)))
rng (mid ((primesFinS n),k,m)) c= rng (primesFinS n)
by FINSEQ_6:119;
then consider i being
object such that A15:
(
i in dom (primesFinS n) &
(primesFinS n) . i = y )
by A14, FUNCT_1:def 3;
reconsider i =
i as
Nat by A15;
1
<= i
by A15, FINSEQ_3:25;
then reconsider i1 =
i - 1 as
Nat ;
i1 + 1
<= len (primesFinS n)
by A15, FINSEQ_3:25;
then
(
i1 < len (primesFinS n) &
len (primesFinS n) = n )
by NAT_1:13, NUMBER13:def 1;
then A16:
(primesFinS n) . (i1 + 1) = primenumber i1
by NUMBER13:def 1;
A17:
(primesFinS n) . i divides Product (mid ((primesFinS n),k,m))
by A14, A15, NAT_3:7;
(primesFinS n) . i in { k where k is Prime : k divides Product (mid ((primesFinS n),k,m)) }
by A16, A17;
hence
y in PrimeDivisors (Product (mid ((primesFinS n),k,m)))
by A15, NUMBER12:def 3;
verum
end;
hence
PrimeDivisors (Product (mid ((primesFinS n),k,m))) = rng (mid ((primesFinS n),k,m))
by A2, XBOOLE_0:def 10; verum