let k be natural number ; :: thesis: for n0, m0 being non zero natural number st n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) holds
ex n1, m1 being natural number st
( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )
let n0, m0 be non zero natural number ; :: thesis: ( n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) implies ex n1, m1 being natural number st
( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) )
assume A1: n0,m0 are_relative_prime ; :: thesis: ( not k in NatDivisors (n0 * m0) or ex n1, m1 being natural number st
( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) )
assume k in NatDivisors (n0 * m0) ; :: thesis: ex n1, m1 being natural number st
( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )
then A2: ( 0 < k & k divides n0 * m0 ) by MOEBIUS1:39;
set n1 = k gcd n0;
set m1 = k gcd m0;
take k gcd n0 ; :: thesis: ex m1 being natural number 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:71;
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:71;
hence k gcd m0 in NatDivisors m0 ; :: thesis: k = (k gcd n0) * (k gcd m0)
thus k = k gcd (n0 * m0) by A2, NEWTON:62
.= (k gcd n0) * (k gcd m0) by A1, Th17 ; :: thesis: verum