A1: a gcd b divides a by INT_2:def 2;
a divides a lcm b by INT_2:def 1;
then a gcd b divides a lcm b by A1, INT_2:9;
then consider k being Integer such that
A2: a lcm b = (a gcd b) * k ;
thus (a lcm b) / (a gcd b) is integer by A2, XCMPLX_1:89; :: thesis: verum