let i, j be natural Number ; :: thesis: i * j = (i lcm j) * (i gcd j)
A0: ( i is Nat & j is Nat ) by TARSKI:1;
A1: ( i <> 0 & j <> 0 implies i * j = (i lcm j) * (i gcd j) )
proof
assume that
A2: i <> 0 and
A3: j <> 0 ; :: thesis: i * j = (i lcm j) * (i gcd j)
A4: ( i divides i implies i divides i * j ) by A0;
( j divides j implies j divides j * i ) by A0;
then i lcm j divides i * j by A4, Def4;
then consider c being Nat such that
A5: i * j = (i lcm j) * c ;
A6: i divides i lcm j by Def4;
A7: j divides i lcm j by Def4;
consider d being Nat such that
A8: i lcm j = i * d by A6;
consider e being Nat such that
A9: i lcm j = j * e by A7;
i * j = i * (c * d) by A5, A8;
then A10: j = c * d by A2, XCMPLX_1:5;
i * j = j * (c * e) by A5, A9;
then i = c * e by A3, XCMPLX_1:5;
then A11: c divides i ;
A12: c divides j by A10;
for f being Nat st f divides i & f divides j holds
f divides c
proof
let f be Nat; :: thesis: ( f divides i & f divides j implies f divides c )
assume that
A13: f divides i and
A14: f divides j ; :: thesis: f divides c
consider g being Nat such that
A15: i = f * g by A13;
consider h being Nat such that
A16: j = f * h by A14;
A17: j * g = (g * h) * f by A16;
i * h = (g * h) * f by A15;
then A18: i divides (g * h) * f ;
j divides (g * h) * f by A17;
then i lcm j divides (g * h) * f by A18, Def4;
then consider z being Nat such that
A19: (g * h) * f = (i lcm j) * z ;
A20: c * (i lcm j) = (g * (h * f)) * f by A5, A15, A16
.= ((i lcm j) * z) * f by A19
.= (z * f) * (i lcm j) ;
i lcm j <> 0 by A2, A3, INT_2:4;
then c = f * z by A20, XCMPLX_1:5;
hence f divides c ; :: thesis: verum
end;
hence i * j = (i lcm j) * (i gcd j) by A5, A11, A12, Def5; :: thesis: verum
end;
( ( i = 0 or j = 0 ) implies i * j = (i lcm j) * (i gcd j) )
proof
assume A21: ( i = 0 or j = 0 ) ; :: thesis: i * j = (i lcm j) * (i gcd j)
then i * j = 0 * (i gcd j)
.= (i lcm j) * (i gcd j) by A21, INT_2:4 ;
hence i * j = (i lcm j) * (i gcd j) ; :: thesis: verum
end;
hence i * j = (i lcm j) * (i gcd j) by A1; :: thesis: verum