let n1, n2, n3 be non zero Nat; (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 )
A12:
for p being Nat st p in support (pfexp d) holds
(ppf d) . p divides (n1 gcd n3) lcm (n2 gcd n3)
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 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
let m,
n be
Element of
NAT ;
( 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
;
(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;
verum
end;
for
m being
Element of
NAT st
m in dom f holds
f . m divides (n1 gcd n3) lcm (n2 gcd n3)
hence
Product (ppf d) divides (n1 gcd n3) lcm (n2 gcd n3)
by A19, A22, Th38;
verum
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; verum