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

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