let a, b, c, d be Integer; :: thesis: ( b divides a & d divides c implies b * d divides a * c )

assume that

A1: b divides a and

A2: d divides c ; :: thesis: b * d divides a * c

consider t being Integer such that

A3: b * t = a by A1;

consider z being Integer such that

A4: d * z = c by A2;

(b * d) * (t * z) = a * c by A3, A4;

hence b * d divides a * c ; :: thesis: verum

assume that

A1: b divides a and

A2: d divides c ; :: thesis: b * d divides a * c

consider t being Integer such that

A3: b * t = a by A1;

consider z being Integer such that

A4: d * z = c by A2;

(b * d) * (t * z) = a * c by A3, A4;

hence b * d divides a * c ; :: thesis: verum