let n1, m1 be Element of NAT ; :: thesis: ( 1 <= n1 & 1 <= m1 implies ex m0, n0 being Element of NAT st
( n1 lcm m1 = n0 * m0 & n0 gcd m0 = 1 & n0 divides n1 & m0 divides m1 & n0 <> 0 & m0 <> 0 ) )
assume A1: ( 1 <= n1 & 1 <= m1 ) ; :: thesis: ex m0, n0 being Element of NAT st
( n1 lcm m1 = n0 * m0 & n0 gcd m0 = 1 & n0 divides n1 & m0 divides m1 & n0 <> 0 & m0 <> 0 )
set nm1 = n1 lcm m1;
reconsider n = n1, m = m1 as non empty natural number by A1;
reconsider nm = n1 lcm m1 as non empty natural number by A1, INT_2:4;
set N1 = { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ;
set N2 = (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ;
A2: support (ppf nm) = (support (ppf n)) \/ (support (ppf m)) by Th9;
then A3: support (ppf n) c= support (ppf nm) by XBOOLE_1:7;
A4: { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } c= support (ppf n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } or x in support (ppf n) )
assume x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ; :: thesis: x in support (ppf n)
then ex p being Element of NAT st
( x = p & p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) ;
hence x in support (ppf n) ; :: thesis: verum

end;

then A5: { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } c= support (ppf nm) by A3, XBOOLE_1:1;
{ p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } \/ ((support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ) = support (ppf nm) by A3, A4, XBOOLE_1:1, XBOOLE_1:45;
then A6: (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } c= support (ppf nm) by XBOOLE_1:7;
A7: (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } c= support (ppf m)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } or x in support (ppf m) )
assume A8: x in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ; :: thesis: x in support (ppf m)
then A9: ( x in support (ppf nm) & not x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ) by XBOOLE_0:def 5;
A10: support (ppf m) = support (pfexp m) by NAT_3:def 9;
( not x in support (ppf n) or x in support (ppf m) )

proof

x in SetPrimes by A8;
then A11: ( not x in support (ppf n) or (pfexp nm) . x <> (pfexp n) . x ) by A9;
A12: ( ( (pfexp n) . x <= (pfexp m) . x implies (max (pfexp n),(pfexp m)) . x = (pfexp m) . x ) & ( (pfexp n) . x > (pfexp m) . x implies (max (pfexp n),(pfexp m)) . x = (pfexp n) . x ) ) by NAT_3:def 4;
x in support (pfexp nm) by A9, NAT_3:def 9;
then ( (pfexp nm) . x = (pfexp m) . x implies (pfexp m) . x <> 0 ) by POLYNOM1:def 7;
hence ( not x in support (ppf n) or x in support (ppf m) ) by A10, A11, A12, NAT_3:54, POLYNOM1:def 7; :: thesis: verum

end;

hence x in support (ppf m) by A2, A9, XBOOLE_0:def 3; :: thesis: verum

end;

A13: for x being set st x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } holds
(pfexp nm) . x = (pfexp n) . x

proof

let x be set ; :: thesis: ( x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } implies (pfexp nm) . x = (pfexp n) . x )
assume x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ; :: thesis: (pfexp nm) . x = (pfexp n) . x
then ex p being Element of NAT st
( x = p & p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) ;
hence (pfexp nm) . x = (pfexp n) . x ; :: thesis: verum

end;

A14: for x being set st x in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } holds
(pfexp nm) . x = (pfexp m) . x

proof

let x be set ; :: thesis: ( x in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } implies (pfexp nm) . x = (pfexp m) . x )
assume x in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ; :: thesis: (pfexp nm) . x = (pfexp m) . x
then A15: ( x in support (ppf nm) & not x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ) by XBOOLE_0:def 5;
A16: support (ppf n) = support (pfexp n) by NAT_3:def 9;
A17: ( ( (pfexp n) . x <= (pfexp m) . x implies (max (pfexp n),(pfexp m)) . x = (pfexp m) . x ) & ( (pfexp n) . x > (pfexp m) . x implies (max (pfexp n),(pfexp m)) . x = (pfexp n) . x ) ) by NAT_3:def 4;
not (pfexp n) . x > (pfexp m) . x

proof

assume A18: (pfexp n) . x > (pfexp m) . x ; :: thesis: contradiction
then A19: (pfexp nm) . x = (pfexp n) . x by A17, NAT_3:54;
A20: x in support (pfexp n) by A18, POLYNOM1:def 7;
then x in SetPrimes ;
hence contradiction by A15, A16, A19, A20; :: thesis: verum

end;

hence (pfexp nm) . x = (pfexp m) . x by A17, NAT_3:54; :: thesis: verum

end;

A21: Product (ppf n) = n by NAT_3:61;
A22: Product (ppf m) = m by NAT_3:61;
consider ppm, ppn being bag of such that
A23: ( support ppm = (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } & support ppn = { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } & support ppm misses support ppn & ppm | (support ppm) = (ppf nm) | (support ppm) & ppn | (support ppn) = (ppf nm) | (support ppn) & ppm + ppn = ppf nm ) by A5, Lm3;
reconsider n0 = Product ppn, m0 = Product ppm as Element of NAT ;
A24: dom (ppf nm) = SetPrimes by PARTFUN1:def 4
.= dom (ppf n) by PARTFUN1:def 4 ;

A25: now

let x1 be set ; :: thesis: ( x1 in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } implies (ppf nm) . x1 = (ppf n) . x1 )
assume A26: x1 in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ; :: thesis: (ppf nm) . x1 = (ppf n) . x1
then A27: x1 in support (ppf nm) by A5;
then A28: x1 in support (pfexp nm) by NAT_3:def 9;
x1 in support (ppf n) by A4, A26;
then A29: x1 in support (pfexp n) by NAT_3:def 9;
x1 is Element of SetPrimes by A27;
then reconsider x = x1 as Prime by NEWTON:def 6;
thus (ppf nm) . x1 = x |^ (x |-count nm) by A28, NAT_3:def 9
.= x |^ ((pfexp nm) . x) by NAT_3:def 8
.= x |^ ((pfexp n) . x) by A13, A26
.= x |^ (x |-count n) by NAT_3:def 8
.= (ppf n) . x1 by A29, NAT_3:def 9 ; :: thesis: verum

end;

A30: ppn | { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } = (ppf n) | { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } by A23, A24, A25, FUNCT_1:166;
A31: dom (ppf nm) = SetPrimes by PARTFUN1:def 4
.= dom (ppf m) by PARTFUN1:def 4 ;

A32: now

let x2 be set ; :: thesis: ( x2 in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } implies (ppf nm) . x2 = (ppf m) . x2 )
assume A33: x2 in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ; :: thesis: (ppf nm) . x2 = (ppf m) . x2
then x2 in support (ppf nm) by A6;
then A34: x2 in support (pfexp nm) by NAT_3:def 9;
x2 in support (ppf m) by A7, A33;
then A35: x2 in support (pfexp m) by NAT_3:def 9;
x2 is Element of SetPrimes by A33;
then reconsider x = x2 as Prime by NEWTON:def 6;
thus (ppf nm) . x2 = x |^ (x |-count nm) by A34, NAT_3:def 9
.= x |^ ((pfexp nm) . x) by NAT_3:def 8
.= x |^ ((pfexp m) . x) by A14, A33
.= x |^ (x |-count m) by NAT_3:def 8
.= (ppf m) . x2 by A35, NAT_3:def 9 ; :: thesis: verum

end;

A36: ppm | ((support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ) = (ppf m) | ((support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } ) by A23, A31, A32, FUNCT_1:166;
A37: n0 * m0 = Product (ppf nm) by A23, NAT_3:19
.= nm by NAT_3:61 ;
A38: m0 divides m by A7, A22, A23, A36, Th7;
A39: n0 <> 0 by A37;
A40: m0 <> 0 by A37;

now

let x be Prime; :: thesis: ( x in support ppm implies ex m being natural number st
( 0 < m & ppm . x = x |^ m ) )
assume A41: x in support ppm ; :: thesis: ex m being natural number st
( 0 < m & ppm . x = x |^ m )
then x in support (ppf nm) by A23, XBOOLE_0:def 5;
then A42: ( x in support (pfexp nm) & x is natural number ) by NAT_3:def 9;
then A43: (ppf nm) . x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm) . x <> 0 by A42, NAT_3:36, NAT_3:38;
then 0 <> x |-count nm by NAT_3:def 8;
then A44: 0 < x |-count nm ;
ppm . x = (ppm | (support ppm)) . x by A41, FUNCT_1:72
.= (ppf nm) . x by A23, A41, FUNCT_1:72 ;
hence ex m being natural number st
( 0 < m & ppm . x = x |^ m ) by A43, A44; :: thesis: verum

end;

then A45: ppm is prime-factorization-like by Def1;

now

let x be Prime; :: thesis: ( x in support ppn implies ex n being natural number st
( 0 < n & ppn . x = x |^ n ) )
assume A46: x in support ppn ; :: thesis: ex n being natural number st
( 0 < n & ppn . x = x |^ n )
then x in support (ppf nm) by A5, A23;
then A47: ( x in support (pfexp nm) & x is natural number ) by NAT_3:def 9;
then A48: (ppf nm) . x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm) . x <> 0 by A47, NAT_3:36, NAT_3:38;
then 0 <> x |-count nm by NAT_3:def 8;
then A49: 0 < x |-count nm ;
ppn . x = (ppn | (support ppn)) . x by A46, FUNCT_1:72
.= (ppf nm) . x by A23, A46, FUNCT_1:72 ;
hence ex n being natural number st
( 0 < n & ppn . x = x |^ n ) by A48, A49; :: thesis: verum

end;

then ppn is prime-factorization-like by Def1;
then A50: n0,m0 are_relative_prime by A23, A45, Th12;
A51: n0 gcd m0 = 1 by A50, INT_2:def 4;
thus ex m0, n0 being Element of NAT st
( n1 lcm m1 = n0 * m0 & n0 gcd m0 = 1 & n0 divides n1 & m0 divides m1 & n0 <> 0 & m0 <> 0 ) by A4, A21, A23, A30, A37, A38, A39, A40, A51, Th7; :: thesis: verum