let n, m, n1, n2, m1, m2 be Nat; :: thesis: ( n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_coprime & n1 * m1 = n2 * m2 implies ( n1 = n2 & m1 = m2 ) )

assume A1: n1 in NatDivisors n ; :: thesis: ( not m1 in NatDivisors m or not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

then A2: n1 divides n by MOEBIUS1:39;

assume A3: m1 in NatDivisors m ; :: thesis: ( not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

then A4: m1 divides m by MOEBIUS1:39;

assume A5: n2 in NatDivisors n ; :: thesis: ( not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

then A6: n2 divides n by MOEBIUS1:39;

assume A7: m2 in NatDivisors m ; :: thesis: ( not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

assume A8: n,m are_coprime ; :: thesis: ( not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

assume A9: n1 * m1 = n2 * m2 ; :: thesis: ( n1 = n2 & m1 = m2 )

A10: m2 divides m by A7, MOEBIUS1:39;

assume ( not n1 = n2 or not m1 = m2 ) ; :: thesis: contradiction

hence contradiction by A17, A9, A11, XCMPLX_1:5; :: thesis: verum

assume A1: n1 in NatDivisors n ; :: thesis: ( not m1 in NatDivisors m or not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

then A2: n1 divides n by MOEBIUS1:39;

assume A3: m1 in NatDivisors m ; :: thesis: ( not n2 in NatDivisors n or not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

then A4: m1 divides m by MOEBIUS1:39;

assume A5: n2 in NatDivisors n ; :: thesis: ( not m2 in NatDivisors m or not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

then A6: n2 divides n by MOEBIUS1:39;

assume A7: m2 in NatDivisors m ; :: thesis: ( not n,m are_coprime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

assume A8: n,m are_coprime ; :: thesis: ( not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )

assume A9: n1 * m1 = n2 * m2 ; :: thesis: ( n1 = n2 & m1 = m2 )

A10: m2 divides m by A7, MOEBIUS1:39;

A11: now :: thesis: not n1 <> n2

A17:
0 < n2
by A5, MOEBIUS1:39;reconsider m19 = m1, m29 = m2 as non zero Nat by A3, A7, MOEBIUS1:39;

A12: n gcd m > 0 by A8, INT_2:def 3;

reconsider n19 = n1, n29 = n2 as non zero Nat by A1, A5, MOEBIUS1:39;

assume n1 <> n2 ; :: thesis: contradiction

then consider p being Element of NAT such that

A13: p is prime and

A14: p |-count n19 <> p |-count n29 by NAT_4:21;

reconsider p = p as Prime by A13;

(p |-count n19) + (p |-count m19) = p |-count (n19 * m19) by NAT_3:28

.= (p |-count n29) + (p |-count m29) by A9, NAT_3:28 ;

then ( p |-count m19 <> 0 or p |-count m29 <> 0 ) by A14;

then ( p divides m19 or p divides m29 ) by MOEBIUS1:6;

then A15: p divides m by A4, A10, INT_2:9;

( p |-count n19 <> 0 or p |-count n29 <> 0 ) by A14;

then ( p divides n19 or p divides n29 ) by MOEBIUS1:6;

then p divides n by A2, A6, INT_2:9;

then p divides n gcd m by A15, INT_2:def 2;

then A16: p <= n gcd m by A12, INT_2:27;

p > 1 by INT_2:def 4;

hence contradiction by A8, A16, INT_2:def 3; :: thesis: verum

end;A12: n gcd m > 0 by A8, INT_2:def 3;

reconsider n19 = n1, n29 = n2 as non zero Nat by A1, A5, MOEBIUS1:39;

assume n1 <> n2 ; :: thesis: contradiction

then consider p being Element of NAT such that

A13: p is prime and

A14: p |-count n19 <> p |-count n29 by NAT_4:21;

reconsider p = p as Prime by A13;

(p |-count n19) + (p |-count m19) = p |-count (n19 * m19) by NAT_3:28

.= (p |-count n29) + (p |-count m29) by A9, NAT_3:28 ;

then ( p |-count m19 <> 0 or p |-count m29 <> 0 ) by A14;

then ( p divides m19 or p divides m29 ) by MOEBIUS1:6;

then A15: p divides m by A4, A10, INT_2:9;

( p |-count n19 <> 0 or p |-count n29 <> 0 ) by A14;

then ( p divides n19 or p divides n29 ) by MOEBIUS1:6;

then p divides n by A2, A6, INT_2:9;

then p divides n gcd m by A15, INT_2:def 2;

then A16: p <= n gcd m by A12, INT_2:27;

p > 1 by INT_2:def 4;

hence contradiction by A8, A16, INT_2:def 3; :: thesis: verum

assume ( not n1 = n2 or not m1 = m2 ) ; :: thesis: contradiction

hence contradiction by A17, A9, A11, XCMPLX_1:5; :: thesis: verum