let n1, m1 be Element of NAT ; ( 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 that
A1:
1 <= n1
and
A2:
1 <= m1
; 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 )
reconsider n = n1, m = m1 as non zero Nat by A1, A2;
set nm1 = n1 lcm m1;
reconsider nm = n1 lcm m1 as non zero Nat by A1, A2, 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 ) } ;
A3:
{ p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } c= support (ppf n)
A4:
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
A12:
Product (ppf m) = m
by NAT_3:61;
A13:
support (ppf nm) = (support (ppf n)) \/ (support (ppf m))
by Th9;
then A14:
support (ppf n) c= support (ppf nm)
by XBOOLE_1:7;
then consider ppm, ppn being bag of SetPrimes such that
A15:
support ppm = (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) }
and
A16:
support ppn = { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) }
and
A17:
support ppm misses support ppn
and
A18:
ppm | (support ppm) = (ppf nm) | (support ppm)
and
A19:
ppn | (support ppn) = (ppf nm) | (support ppn)
and
A20:
ppm + ppn = ppf nm
by A3, Lm3, XBOOLE_1:1;
reconsider n0 = Product ppn, m0 = Product ppm as Element of NAT ;
A21:
Product (ppf n) = n
by NAT_3:61;
A22:
(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
object ;
TARSKI:def 3 ( 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) )
A23:
(
(pfexp n) . x <= (pfexp m) . x implies
(max ((pfexp n),(pfexp m))) . x = (pfexp m) . x )
by NAT_3:def 4;
A24:
(
(pfexp n) . x > (pfexp m) . x implies
(max ((pfexp n),(pfexp m))) . x = (pfexp n) . x )
by NAT_3:def 4;
assume A25:
x in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) }
;
x in support (ppf m)
then A26:
x in SetPrimes
;
A27:
x in support (ppf nm)
by A25, XBOOLE_0:def 5;
then
x in support (pfexp nm)
by NAT_3:def 9;
then A28:
(
(pfexp nm) . x = (pfexp m) . x implies
(pfexp m) . x <> 0 )
by PRE_POLY:def 7;
not
x in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) }
by A25, XBOOLE_0:def 5;
then A29:
( not
x in support (ppf n) or
(pfexp nm) . x <> (pfexp n) . x )
by A26;
support (ppf m) = support (pfexp m)
by NAT_3:def 9;
hence
x in support (ppf m)
by A13, A27, A29, A23, A24, A28, NAT_3:54, PRE_POLY:def 7, XBOOLE_0:def 3;
verum
end;
{ 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 A14, A3, XBOOLE_1:1, XBOOLE_1:45;
then A30:
(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;
dom (ppf nm) =
SetPrimes
by PARTFUN1:def 2
.=
dom (ppf m)
by PARTFUN1:def 2
;
then
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 A15, A18, A31, FUNCT_1:96;
then A34:
m0 divides m
by A22, A12, A15, Th7;
A35: n0 * m0 =
Product (ppf nm)
by A17, A20, NAT_3:19
.=
nm
by NAT_3:61
;
then A36:
m0 <> 0
;
then A41:
ppm is prime-factorization-like
;
A42:
{ p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } c= support (ppf nm)
by A14, A3;
then
ppn is prime-factorization-like
;
then
n0,m0 are_coprime
by A17, A41, Th12;
then A47:
n0 gcd m0 = 1
by INT_2:def 3;
A48:
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
dom (ppf nm) =
SetPrimes
by PARTFUN1:def 2
.=
dom (ppf n)
by PARTFUN1:def 2
;
then A53:
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 A16, A19, A49, FUNCT_1:96;
n0 <> 0
by A35;
hence
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 A3, A21, A16, A53, A35, A34, A36, A47, Th7; verum