let n1, n2, n3 be non zero natural number ; :: thesis: (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3
set d1 = n1 gcd n3;
set d2 = n2 gcd n3;
set M = n1 lcm n2;
reconsider d = (n1 lcm n2) gcd n3 as non empty natural number by INT_2:5;
reconsider M = n1 lcm n2 as non empty natural number by INT_2:4;
A1: ( n1 gcd n3 divides n3 & n2 gcd n3 divides n3 & n1 gcd n3 divides n1 & n2 gcd n3 divides n2 ) by NAT_D:def 5;
then A2: (n1 gcd n3) lcm (n2 gcd n3) divides n3 by NAT_D:def 4;
( n1 divides M & n2 divides M ) by NAT_D:def 4;
then ( n1 gcd n3 divides M & n2 gcd n3 divides M ) by A1, NAT_D:4;
then (n1 gcd n3) lcm (n2 gcd n3) divides M by NAT_D:def 4;
then A3: (n1 gcd n3) lcm (n2 gcd n3) divides d by A2, NAT_D:def 5;
A4: for p being natural number holds
( not p in support (pfexp d) or (ppf d) . p divides n1 or (ppf d) . p divides n2 )

proof

let p be natural number ; :: thesis: ( not p in support (pfexp d) or (ppf d) . p divides n1 or (ppf d) . p divides n2 )
assume A5: ( p in support (pfexp d) & not (ppf d) . p divides n1 & not (ppf d) . p divides n2 ) ; :: thesis: contradiction
then A6: ( not p |^ (p |-count d) divides n1 & not p |^ (p |-count d) divides n2 ) by NAT_3:def 9;
A7: p is Prime by A5, NAT_3:34;
A8: d divides M by NAT_D:def 5;
p |-count d > p |-count M

proof

A9: p |-count M = (pfexp M) . p by A7, NAT_3:def 8
.= (max (pfexp n1),(pfexp n2)) . p by NAT_3:54 ;

per cases ( (pfexp n1) . p <= (pfexp n2) . p or (pfexp n1) . p > (pfexp n2) . p ) ;

suppose (pfexp n1) . p <= (pfexp n2) . p ; :: thesis: p |-count d > p |-count M

then p |-count M = (pfexp n2) . p by A9, NAT_3:def 4
.= p |-count n2 by A7, NAT_3:def 8 ;
hence p |-count d > p |-count M by A6, A7, MOEBIUS1:9; :: thesis: verum

end;

suppose (pfexp n1) . p > (pfexp n2) . p ; :: thesis: p |-count d > p |-count M

then p |-count M = (pfexp n1) . p by A9, NAT_3:def 4
.= p |-count n1 by A7, NAT_3:def 8 ;
hence p |-count d > p |-count M by A6, A7, MOEBIUS1:9; :: thesis: verum

end;

end;

end;

hence contradiction by A7, A8, NAT_3:30; :: thesis: verum

end;

A10: for p being natural number st p in support (pfexp d) holds
(ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

proof

let p be natural number ; :: thesis: ( p in support (pfexp d) implies (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) )
assume A11: p in support (pfexp d) ; :: thesis: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)
then A12: p is Prime by NAT_3:34;
d divides n3 by NAT_D:def 5;
then p |-count d <= p |-count n3 by A12, NAT_3:30;
then p |^ (p |-count d) divides p |^ (p |-count n3) by RADIX_1:7;
then A13: (ppf d) . p divides p |^ (p |-count n3) by A11, NAT_3:def 9;
p <> 1 by A12, INT_2:def 5;
then p |^ (p |-count n3) divides n3 by NAT_3:def 7;
then A14: (ppf d) . p divides n3 by A13, NAT_D:4;
A15: ( n1 gcd n3 divides (n1 gcd n3) lcm (n2 gcd n3) & n2 gcd n3 divides (n1 gcd n3) lcm (n2 gcd n3) ) by NAT_D:def 4;

per cases ( (ppf d) . p divides n1 or (ppf d) . p divides n2 ) by A4, A11;

suppose (ppf d) . p divides n1 ; :: thesis: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

then (ppf d) . p divides n1 gcd n3 by A14, NAT_D:def 5;
hence (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) by A15, NAT_D:4; :: thesis: verum

end;

suppose (ppf d) . p divides n2 ; :: thesis: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

then (ppf d) . p divides n2 gcd n3 by A14, NAT_D:def 5;
hence (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) by A15, NAT_D:4; :: thesis: verum

end;

end;

end;

Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3)

proof

set g = ppf d;
set K = canFS (support (ppf d));
consider f being FinSequence of COMPLEX such that
A16: ( Product (ppf d) = Product f & f = (ppf d) * (canFS (support (ppf d))) ) by NAT_3:def 5;
A17: rng (canFS (support (ppf d))) = support (ppf d) by FUNCT_2:def 3;
then rng (canFS (support (ppf d))) c= NAT by XBOOLE_1:1;
then reconsider K = canFS (support (ppf d)) as FinSequence of NAT by FINSEQ_1:def 4;
rng f c= NAT by A16, VALUED_0:def 6;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
A18: for m, n being Element of NAT st m in dom f & n in dom f & m <> n holds
(f . m) gcd (f . n) = 1

proof

let m, n be Element of NAT ; :: thesis: ( m in dom f & n in dom f & m <> n implies (f . m) gcd (f . n) = 1 )
assume A19: ( m in dom f & n in dom f & m <> n ) ; :: thesis: (f . m) gcd (f . n) = 1
then A20: ( f . m = (ppf d) . (K . m) & f . n = (ppf d) . (K . n) ) by A16, FUNCT_1:22;
A21: ( m in dom K & n in dom K ) by A16, A19, FUNCT_1:21;
then ( K . m in support (ppf d) & K . n in support (ppf d) ) by A17, FUNCT_1:12;
then A22: ( K . m in support (pfexp d) & K . n in support (pfexp d) ) by NAT_3:def 9;
then A23: ( K . m is prime & K . n is prime ) by NAT_3:34;
A24: ( K . m > 0 & K . n > 0 ) by A22, NAT_3:34;
K . m <> K . n by A19, A21, FUNCT_1:def 8;
then A25: K . n,(K . m) |^ ((K . m) |-count d) are_relative_prime by A23, EULER_2:32, INT_2:47;
A26: (K . n) |^ ((K . n) |-count d),(K . m) |^ ((K . m) |-count d) are_relative_prime by A24, A25, EULER_2:32;
( f . m = (K . m) |^ ((K . m) |-count d) & f . n = (K . n) |^ ((K . n) |-count d) ) by A20, A22, NAT_3:def 9;
hence (f . m) gcd (f . n) = 1 by A26, INT_2:def 4; :: thesis: verum

end;

for m being Element of NAT st m in dom f holds
f . m divides (n1 gcd n3) lcm (n2 gcd n3)

proof

let m be Element of NAT ; :: thesis: ( m in dom f implies f . m divides (n1 gcd n3) lcm (n2 gcd n3) )
assume A27: m in dom f ; :: thesis: f . m divides (n1 gcd n3) lcm (n2 gcd n3)
then m in dom K by A16, FUNCT_1:21;
then K . m in support (ppf d) by A17, FUNCT_1:12;
then K . m in support (pfexp d) by NAT_3:def 9;
then (ppf d) . (K . m) divides (n1 gcd n3) lcm (n2 gcd n3) by A10;
hence f . m divides (n1 gcd n3) lcm (n2 gcd n3) by A16, A27, FUNCT_1:22; :: thesis: verum

end;

hence Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3) by A16, A18, Th38; :: thesis: verum

end;

then d divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_3:61;
hence (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3 by A3, NAT_D:5; :: thesis: verum