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