let a, b, A, B be Integer; :: thesis: ( a,b are_coprime implies ( ( a divides A & b divides B ) iff a * b divides (a * B) + (b * A) ) )
assume A1: a,b are_coprime ; :: thesis: ( ( a divides A & b divides B ) iff a * b divides (a * B) + (b * A) )
thus ( a divides A & b divides B implies a * b divides (a * B) + (b * A) ) :: thesis: ( a * b divides (a * B) + (b * A) implies ( a divides A & b divides B ) )

proof

assume A2: ( a divides A & b divides B ) ; :: thesis: a * b divides (a * B) + (b * A)
then consider x being Integer such that
A3: A = a * x by INT_1:def 3;
consider y being Integer such that
A4: B = b * y by A2, INT_1:def 3;
(a * B) + (b * A) = (a * b) * (y + x) by A3, A4;
hence a * b divides (a * B) + (b * A) by INT_1:def 3; :: thesis: verum

end;

assume a * b divides (a * B) + (b * A) ; :: thesis: ( a divides A & b divides B )
then consider x being Integer such that
A5: (a * B) + (b * A) = (a * b) * x by INT_1:def 3;
a * ((- B) + (b * x)) = b * A by A5;
hence a divides A by A1, INT_2:25, INT_1:def 3; :: thesis: b divides B
b * ((- A) + (a * x)) = a * B by A5;
hence b divides B by A1, INT_2:25, INT_1:def 3; :: thesis: verum