let i, j be Nat; :: thesis: i * j = (i lcm j) * (i gcd j)
A1: ( i <> 0 & j <> 0 implies i * j = (i lcm j) * (i gcd j) )

proof

assume A2: ( i <> 0 & j <> 0 ) ; :: thesis: i * j = (i lcm j) * (i gcd j)
A3: ( i divides i implies i divides i * j ) by Th9;
( j divides j implies j divides j * i ) by Th9;
then i lcm j divides i * j by A3, Def4;
then consider c being Nat such that
A4: i * j = (i lcm j) * c by Def3;
A5: ( i divides i lcm j & j divides i lcm j ) by Def4;
then consider d being Nat such that
A6: i lcm j = i * d by Def3;
consider e being Nat such that
A7: i lcm j = j * e by A5, Def3;
i * j = i * (c * d) by A4, A6;
then A8: j = c * d by A2, XCMPLX_1:5;
i * j = j * (c * e) by A4, A7;
then i = c * e by A2, XCMPLX_1:5;
then A9: ( c divides i & c divides j ) by A8, Def3;
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 A10: ( f divides i & f divides j ) ; :: thesis: f divides c
then consider g being Nat such that
A11: i = f * g by Def3;
consider h being Nat such that
A12: j = f * h by A10, Def3;
A13: j * g = (g * h) * f by A12;
i * h = (g * h) * f by A11;
then ( i divides (g * h) * f & j divides (g * h) * f ) by A13, Def3;
then i lcm j divides (g * h) * f by Def4;
then consider z being Nat such that
A14: (g * h) * f = (i lcm j) * z by Def3;
A15: c * (i lcm j) = (g * (h * f)) * f by A4, A11, A12
.= ((i lcm j) * z) * f by A14
.= (z * f) * (i lcm j) ;
i lcm j <> 0 by A2, INT_2:4;
then c = f * z by A15, XCMPLX_1:5;
hence f divides c by Def3; :: thesis: verum

end;

hence i * j = (i lcm j) * (i gcd j) by A4, A9, Def5; :: thesis: verum

end;

( ( i = 0 or j = 0 ) implies i * j = (i lcm j) * (i gcd j) )

proof

assume A16: ( 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 A16, 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