let k be Nat; :: thesis: for n0, m0 being non zero Nat st n0,m0 are_coprime & k in NatDivisors (n0 * m0) holds

ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )

let n0, m0 be non zero Nat; :: thesis: ( n0,m0 are_coprime & k in NatDivisors (n0 * m0) implies ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) )

assume A1: n0,m0 are_coprime ; :: thesis: ( not k in NatDivisors (n0 * m0) or ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) )

set m1 = k gcd m0;

set n1 = k gcd n0;

assume A2: k in NatDivisors (n0 * m0) ; :: thesis: ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )

take k gcd n0 ; :: thesis: ex m1 being Nat st

( k gcd n0 in NatDivisors n0 & m1 in NatDivisors m0 & k = (k gcd n0) * m1 )

take k gcd m0 ; :: thesis: ( k gcd n0 in NatDivisors n0 & k gcd m0 in NatDivisors m0 & k = (k gcd n0) * (k gcd m0) )

( k gcd n0 divides n0 & k gcd n0 > 0 ) by NAT_D:def 5, NEWTON:58;

hence k gcd n0 in NatDivisors n0 ; :: thesis: ( k gcd m0 in NatDivisors m0 & k = (k gcd n0) * (k gcd m0) )

( k gcd m0 divides m0 & k gcd m0 > 0 ) by NAT_D:def 5, NEWTON:58;

hence k gcd m0 in NatDivisors m0 ; :: thesis: k = (k gcd n0) * (k gcd m0)

k divides n0 * m0 by A2, MOEBIUS1:39;

hence k = k gcd (n0 * m0) by NEWTON:49

.= (k gcd n0) * (k gcd m0) by A1, Th17 ;

:: thesis: verum

ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )

let n0, m0 be non zero Nat; :: thesis: ( n0,m0 are_coprime & k in NatDivisors (n0 * m0) implies ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) )

assume A1: n0,m0 are_coprime ; :: thesis: ( not k in NatDivisors (n0 * m0) or ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) )

set m1 = k gcd m0;

set n1 = k gcd n0;

assume A2: k in NatDivisors (n0 * m0) ; :: thesis: ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )

take k gcd n0 ; :: thesis: ex m1 being Nat st

( k gcd n0 in NatDivisors n0 & m1 in NatDivisors m0 & k = (k gcd n0) * m1 )

take k gcd m0 ; :: thesis: ( k gcd n0 in NatDivisors n0 & k gcd m0 in NatDivisors m0 & k = (k gcd n0) * (k gcd m0) )

( k gcd n0 divides n0 & k gcd n0 > 0 ) by NAT_D:def 5, NEWTON:58;

hence k gcd n0 in NatDivisors n0 ; :: thesis: ( k gcd m0 in NatDivisors m0 & k = (k gcd n0) * (k gcd m0) )

( k gcd m0 divides m0 & k gcd m0 > 0 ) by NAT_D:def 5, NEWTON:58;

hence k gcd m0 in NatDivisors m0 ; :: thesis: k = (k gcd n0) * (k gcd m0)

k divides n0 * m0 by A2, MOEBIUS1:39;

hence k = k gcd (n0 * m0) by NEWTON:49

.= (k gcd n0) * (k gcd m0) by A1, Th17 ;

:: thesis: verum