let n1, n2, n3 be non zero Nat; :: 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 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 )

(ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

( 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: verum

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 )

proof

A12:
for p being Nat st p in support (pfexp d) holds
let p be Nat; :: thesis: ( not p in support (pfexp d) or (ppf d) . p divides n1 or (ppf d) . p divides n2 )

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: contradiction

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

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

end;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: contradiction

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

proof

d divides M
by NAT_D:def 5;
A11: p |-count M =
(pfexp M) . p
by A8, NAT_3:def 8

.= (max ((pfexp n1),(pfexp n2))) . p by NAT_3:54 ;

end;.= (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 )
;

end;

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

(ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

proof

Product (ppf d) 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: ( p in support (pfexp d) implies (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) )

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: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

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;

end;let p be Nat; :: thesis: ( p in support (pfexp d) implies (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3) )

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: (ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)

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
( (ppf d) . p divides n1 or (ppf d) . p divides n2 )
by A3, A15;

end;

proof

then A37:
d divides (n1 gcd n3) lcm (n2 gcd n3)
by NAT_3:61;
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

f . m divides (n1 gcd n3) lcm (n2 gcd n3)

end;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

proof

for m being Element of NAT st m in dom f holds
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 that

A23: m in dom f and

A24: n in dom f and

A25: m <> n ; :: thesis: (f . m) gcd (f . n) = 1

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: verum

end;assume that

A23: m in dom f and

A24: n in dom f and

A25: m <> n ; :: thesis: (f . m) gcd (f . n) = 1

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: verum

f . m divides (n1 gcd n3) lcm (n2 gcd n3)

proof

hence
Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3)
by A19, A22, Th38; :: thesis: verum
let m be Element of NAT ; :: thesis: ( m in dom f implies f . m divides (n1 gcd n3) lcm (n2 gcd n3) )

assume A36: m in dom f ; :: thesis: f . m divides (n1 gcd n3) lcm (n2 gcd n3)

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: verum

end;assume A36: m in dom f ; :: thesis: f . m divides (n1 gcd n3) lcm (n2 gcd n3)

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: verum

( 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: verum