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 that
A1: 1 <= n1 and
A2: 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 )
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)
proof
let x be object ; :: 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;
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
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 )
A5: ( (pfexp n) . x > (pfexp m) . x implies (max ((pfexp n),(pfexp m))) . x = (pfexp n) . x ) by NAT_3:def 4;
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 A6: 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;
A7: support (ppf n) = support (pfexp n) by NAT_3:def 9;
A8: not (pfexp n) . x > (pfexp m) . x
proof
assume A9: (pfexp n) . x > (pfexp m) . x ; :: thesis: contradiction
then A10: (pfexp nm) . x = (pfexp n) . x by A5, NAT_3:54;
A11: x in support (pfexp n) by A9, PRE_POLY:def 7;
then x in SetPrimes ;
hence contradiction by A6, A7, A10, A11; :: thesis: verum
end;
( (pfexp n) . x <= (pfexp m) . x implies (max ((pfexp n),(pfexp m))) . x = (pfexp m) . x ) by NAT_3:def 4;
hence (pfexp nm) . x = (pfexp m) . x by A8, NAT_3:54; :: thesis: verum
end;
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 ; :: 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) )
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 ) } ; :: thesis: 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; :: thesis: 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;
A31: now :: thesis: for x2 being set st x2 in (support (ppf nm)) \ { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } holds
(ppf nm) . x2 = (ppf m) . x2
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 A32: 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 reconsider x = x2 as Prime by NEWTON:def 6;
x2 in support (ppf m) by A22, A32;
then A33: x2 in support (pfexp m) by NAT_3:def 9;
x2 in support (ppf nm) by A30, A32;
then x2 in support (pfexp nm) by NAT_3:def 9;
hence (ppf nm) . x2 = x |^ (x |-count nm) by NAT_3:def 9
.= x |^ ((pfexp nm) . x) by NAT_3:def 8
.= x |^ ((pfexp m) . x) by A4, A32
.= x |^ (x |-count m) by NAT_3:def 8
.= (ppf m) . x2 by A33, NAT_3:def 9 ;
:: thesis: verum
end;
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 ;
now :: thesis: for x being Prime st x in support ppm holds
ex m being Nat st
( 0 < m & ppm . x = x |^ m )
let x be Prime; :: thesis: ( x in support ppm implies ex m being Nat st
( 0 < m & ppm . x = x |^ m ) )
assume A37: x in support ppm ; :: thesis: ex m being Nat st
( 0 < m & ppm . x = x |^ m )
then x in support (ppf nm) by A15, XBOOLE_0:def 5;
then A38: x in support (pfexp nm) by NAT_3:def 9;
then A39: (ppf nm) . x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm) . x <> 0 by A38, NAT_3:36, NAT_3:38;
then A40: 0 < x |-count nm by NAT_3:def 8;
ppm . x = (ppm | (support ppm)) . x by A37, FUNCT_1:49
.= (ppf nm) . x by A18, A37, FUNCT_1:49 ;
hence ex m being Nat st
( 0 < m & ppm . x = x |^ m ) by A39, A40; :: thesis: verum
end;
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;
now :: thesis: for x being Prime st x in support ppn holds
ex n being Nat st
( 0 < n & ppn . x = x |^ n )
let x be Prime; :: thesis: ( x in support ppn implies ex n being Nat st
( 0 < n & ppn . x = x |^ n ) )
assume A43: x in support ppn ; :: thesis: ex n being Nat st
( 0 < n & ppn . x = x |^ n )
then x in support (ppf nm) by A42, A16;
then A44: x in support (pfexp nm) by NAT_3:def 9;
then A45: (ppf nm) . x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm) . x <> 0 by A44, NAT_3:36, NAT_3:38;
then A46: 0 < x |-count nm by NAT_3:def 8;
ppn . x = (ppn | (support ppn)) . x by A43, FUNCT_1:49
.= (ppf nm) . x by A19, A43, FUNCT_1:49 ;
hence ex n being Nat st
( 0 < n & ppn . x = x |^ n ) by A45, A46; :: thesis: verum
end;
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
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;
A49: now :: thesis: for x1 being set st x1 in { p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) } holds
(ppf nm) . x1 = (ppf n) . x1
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 A50: 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 A51: x1 in support (ppf nm) by A42;
then reconsider x = x1 as Prime by NEWTON:def 6;
x1 in support (ppf n) by A3, A50;
then A52: x1 in support (pfexp n) by NAT_3:def 9;
x1 in support (pfexp nm) by A51, NAT_3:def 9;
hence (ppf nm) . x1 = x |^ (x |-count nm) by NAT_3:def 9
.= x |^ ((pfexp nm) . x) by NAT_3:def 8
.= x |^ ((pfexp n) . x) by A48, A50
.= x |^ (x |-count n) by NAT_3:def 8
.= (ppf n) . x1 by A52, NAT_3:def 9 ;
:: thesis: verum
end;
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; :: thesis: verum