let m, n be Nat; :: thesis: ( m > 1 & n > 1 & m,n are_coprime implies ex p, q being Prime st
( p divides m & not p divides n & q divides n & not q divides m & p <> q ) )
assume m > 1 ; :: thesis: ( not n > 1 or not m,n are_coprime or ex p, q being Prime st
( p divides m & not p divides n & q divides n & not q divides m & p <> q ) )
then A1: m >= 1 + 1 by NAT_1:13;
assume n > 1 ; :: thesis: ( not m,n are_coprime or ex p, q being Prime st
( p divides m & not p divides n & q divides n & not q divides m & p <> q ) )
then A2: n >= 1 + 1 by NAT_1:13;
assume A3: m,n are_coprime ; :: thesis: ex p, q being Prime st
( p divides m & not p divides n & q divides n & not q divides m & p <> q )
consider p being Element of NAT such that
A4: p is prime and
A5: p divides m by A1, INT_2:31;
consider q being Element of NAT such that
A6: q is prime and
A7: q divides n by A2, INT_2:31;
reconsider p = p as Prime by A4;
reconsider q = q as Prime by A6;
take p ; :: thesis: ex q being Prime st
( p divides m & not p divides n & q divides n & not q divides m & p <> q )
take q ; :: thesis: ( p divides m & not p divides n & q divides n & not q divides m & p <> q )
thus ( p divides m & not p divides n & q divides n & not q divides m & p <> q ) by A3, A5, A7, PYTHTRIP:def 2; :: thesis: verum