let a, b be Nat; :: thesis: for m being non zero Nat holds Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime
let m be non zero Nat; :: thesis: Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime
set A = { p where p is Prime : ( p divides m & p divides a ) } ;
set B = { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ;
assume not Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime ; :: thesis: contradiction
then consider P being Prime such that
A1: P divides Product (Sgm { p where p is Prime : ( p divides m & p divides a ) } ) and
A2: P divides Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) by PYTHTRIP:def 2;
{ p where p is Prime : ( p divides m & p divides a ) } is included_in_Seg by Lm21;
then P in { p where p is Prime : ( p divides m & p divides a ) } by A1, Th12, Lm23;
then A3: ex p being Prime st
( P = p & p divides m & p divides a ) ;
{ r where r is Prime : ( r divides m & not r divides a & not r divides b ) } is included_in_Seg by Lm22;
then P in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } by A2, Th12, Lm24;
then ex r being Prime st
( P = r & r divides m & not r divides a & not r divides b ) ;
hence contradiction by A3; :: thesis: verum