let i, x, y be Integer; :: thesis: ( x divides i & y divides i & x,y are_coprime implies x * y divides i )
assume that
A1: x divides i and
A2: ( y divides i & x,y are_coprime ) ; :: thesis: x * y divides i
consider m being Integer such that
A3: i = x * m by A1;
y divides m by A2, A3, INT_2:25;
then consider r being Integer such that
A4: m = y * r ;
i = (x * y) * r by A3, A4;
hence x * y divides i ; :: thesis: verum