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