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

let p be Nat; :: thesis:
assume that
A4: p in support (pfexp d) and
A5: not (ppf d) . p divides n1 and
A6: not (ppf d) . p divides n2 ; :: thesis:
A7: not p |^ (p |-count d) divides n2 by A4, A6, NAT_3:def 9;
A8: p is Prime by A4, NAT_3:34;
A9: not p |^ (p |-count d) divides n1 by A4, A5, NAT_3:def 9;
A10: p |-count d > p |-count M

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

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

suppose (pfexp n1) . p <= (pfexp n2) . p ; :: thesis:

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

end;

suppose (pfexp n1) . p > (pfexp n2) . p ; :: thesis:

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

end;

end;

end;

d divides M by NAT_D:def 5;
hence contradiction by A8, A10, NAT_3:30; :: thesis:

end;

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

A13: n2 gcd n3 divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_D:def 4;
let p be Nat; :: thesis:
A14: n1 gcd n3 divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_D:def 4;
assume A15: p in support (pfexp d) ; :: thesis:
then A16: p is Prime by NAT_3:34;
d divides n3 by NAT_D:def 5;
then p |-count d <= p |-count n3 by A16, NAT_3:30;
then p |^ (p |-count d) divides p |^ (p |-count n3) by NEWTON:89;
then A17: (ppf d) . p divides p |^ (p |-count n3) by A15, NAT_3:def 9;
p <> 1 by A16, INT_2:def 4;
then p |^ (p |-count n3) divides n3 by NAT_3:def 7;
then A18: (ppf d) . p divides n3 by A17, NAT_D:4;

per cases ) . p divides n1 or (ppf d) . p divides n2 ) by A3, A15;

suppose (ppf d) . p divides n1 ; :: thesis:

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

end;

suppose (ppf d) . p divides n2 ; :: thesis:

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

end;

end;

end;

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

set g = ppf d;
set K = canFS (support (ppf d));
consider f being FinSequence of COMPLEX such that
A19: Product (ppf d) = Product f and
A20: f = (ppf d) * (canFS (support (ppf d))) by NAT_3:def 5;
rng f c= NAT by A20, VALUED_0:def 6;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
A21: 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;
A22: 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

let m, n be Element of NAT ; :: thesis:
assume that
A23: m in dom f and
A24: n in dom f and
A25: m <> n ; :: thesis:
A26: m in dom K by A20, A23, FUNCT_1:11;
then K . m in support (ppf d) by A21, FUNCT_1:3;
then A27: K . m in support (pfexp d) by NAT_3:def 9;
then A28: K . m is prime by NAT_3:34;
A29: n in dom K by A20, A24, FUNCT_1:11;
then K . n in support (ppf d) by A21, FUNCT_1:3;
then A30: K . n in support (pfexp d) by NAT_3:def 9;
then A31: K . n is prime by NAT_3:34;
f . n = (ppf d) . (K . n) by A20, A24, FUNCT_1:12;
then A32: f . n = (K . n) |^ ((K . n) |-count d) by A30, NAT_3:def 9;
f . m = (ppf d) . (K . m) by A20, A23, FUNCT_1:12;
then A33: f . m = (K . m) |^ ((K . m) |-count d) by A27, NAT_3:def 9;
K . m <> K . n by A25, A26, A29, FUNCT_1:def 4;
then A34: K . n,(K . m) |^ ((K . m) |-count d) are_coprime by A28, A31, EULER_2:17, INT_2:30;
A35: K . n > 0 by A30, NAT_3:34;
K . m > 0 by A27, NAT_3:34;
then (K . n) |^ ((K . n) |-count d),(K . m) |^ ((K . m) |-count d) are_coprime by A35, A34, EULER_2:17;
hence (f . m) gcd (f . n) = 1 by A33, A32, INT_2:def 3; :: thesis:

end;

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

let m be Element of NAT ; :: thesis:
assume A36: m in dom f ; :: thesis:
then m in dom K by A20, FUNCT_1:11;
then K . m in support (ppf d) by A21, FUNCT_1:3;
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 A12;
hence f . m divides (n1 gcd n3) lcm (n2 gcd n3) by A20, A36, FUNCT_1:12; :: thesis:

end;

hence Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3) by A19, A22, Th38; :: thesis:

end;

then A37: d divides (n1 gcd n3) lcm (n2 gcd n3) by NAT_3:61;
( n1 gcd n3 divides n1 & n1 divides M ) by NAT_D:def 4, NAT_D:def 5;
then n1 gcd n3 divides M by NAT_D:4;
then (n1 gcd n3) lcm (n2 gcd n3) divides M by A2, NAT_D:def 4;
then (n1 gcd n3) lcm (n2 gcd n3) divides d by A1, NAT_D:def 5;
hence (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3 by A37, NAT_D:5; :: thesis: