let k, m, n, o, p be Nat; :: thesis: ( 1 <= k & k <= m & m < n & n <= o & o <= p implies Product (mid ((primesFinS p),k,m)), Product (mid ((primesFinS p),n,o)) are_coprime )
assume A1: ( 1 <= k & k <= m & m < n & n <= o & o <= p ) ; :: thesis: Product (mid ((primesFinS p),k,m)), Product (mid ((primesFinS p),n,o)) are_coprime
set P = primesFinS p;
set M1 = mid ((primesFinS p),k,m);
set M2 = mid ((primesFinS p),n,o);
assume not Product (mid ((primesFinS p),k,m)), Product (mid ((primesFinS p),n,o)) are_coprime ; :: thesis: contradiction
then not (Product (mid ((primesFinS p),k,m))) gcd (Product (mid ((primesFinS p),n,o))) is trivial by NAT_2:def 1;
then consider q being prime Nat such that
A2: q divides (Product (mid ((primesFinS p),k,m))) gcd (Product (mid ((primesFinS p),n,o))) by NEWTON03:29;
n <= p by A1, XXREAL_0:2;
then A3: m <= p by A1, XXREAL_0:2;
(Product (mid ((primesFinS p),k,m))) gcd (Product (mid ((primesFinS p),n,o))) divides Product (mid ((primesFinS p),k,m)) by INT_2:def 2;
then q divides Product (mid ((primesFinS p),k,m)) by A2, INT_2:9;
then 1 + (primeindex q) <= m by A1, A3, Th3;
then A4: 1 + (primeindex q) < n by A1, XXREAL_0:2;
1 <= m by A1, XXREAL_0:2;
then A5: 1 <= n by A1, XXREAL_0:2;
(Product (mid ((primesFinS p),k,m))) gcd (Product (mid ((primesFinS p),n,o))) divides Product (mid ((primesFinS p),n,o)) by INT_2:def 2;
then q divides Product (mid ((primesFinS p),n,o)) by A2, INT_2:9;
hence contradiction by A4, A1, A5, Th3; :: thesis: verum