let n, m, n1, m1, n2, m2 be natural number ; :: thesis: ( n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_relative_prime & 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_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A2:
( 0 < n1 & 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_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A4:
( 0 < m1 & m1 divides m )
by MOEBIUS1:39;
assume A5:
n2 in NatDivisors n
; :: thesis: ( not m2 in NatDivisors m or not n,m are_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A6:
( 0 < n2 & n2 divides n )
by MOEBIUS1:39;
assume A7:
m2 in NatDivisors m
; :: thesis: ( not n,m are_relative_prime or not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
then A8:
( 0 < m2 & m2 divides m )
by MOEBIUS1:39;
assume A9:
n,m are_relative_prime
; :: thesis: ( not n1 * m1 = n2 * m2 or ( n1 = n2 & m1 = m2 ) )
assume A10:
n1 * m1 = n2 * m2
; :: thesis: ( n1 = n2 & m1 = m2 )
assume A11:
( not n1 = n2 or not m1 = m2 )
; :: thesis: contradiction
now assume A12:
n1 <> n2
;
:: thesis: contradictionreconsider n1' =
n1,
n2' =
n2 as non
empty Nat by A1, A5, MOEBIUS1:39;
reconsider m1' =
m1,
m2' =
m2 as non
empty Nat by A3, A7, MOEBIUS1:39;
consider p being
Element of
NAT such that A13:
(
p is
prime &
p |-count n1' <> p |-count n2' )
by A12, NAT_4:21;
reconsider p =
p as
Prime by A13;
A14:
(p |-count n1') + (p |-count m1') =
p |-count (n1' * m1')
by NAT_3:28
.=
(p |-count n2') + (p |-count m2')
by A10, NAT_3:28
;
(
p |-count m1' <> 0 or
p |-count m2' <> 0 )
by A13, A14;
then
(
p divides m1' or
p divides m2' )
by MOEBIUS1:6;
then A15:
p divides m
by A4, A8, INT_2:13;
(
p |-count n1' <> 0 or
p |-count n2' <> 0 )
by A13;
then
(
p divides n1' or
p divides n2' )
by MOEBIUS1:6;
then A16:
p divides n
by A2, A6, INT_2:13;
A17:
n gcd m > 0
by A9, INT_2:def 4;
p divides n gcd m
by A15, A16, INT_2:def 3;
then A18:
p <= n gcd m
by A17, INT_2:43;
p > 1
by INT_2:def 5;
hence
contradiction
by A18, A9, INT_2:def 4;
:: thesis: verum end;
hence
contradiction
by A10, A11, A6, XCMPLX_1:5; :: thesis: verum