let a, b be Integer; :: thesis: ( ( a <> 0 or b <> 0 ) implies ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_coprime ) )
assume ( a <> 0 or b <> 0 ) ; :: thesis: ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_coprime )
then A1: a gcd b <> 0 by Th5;
a gcd b divides a by Def2;
then consider a1 being Integer such that
A2: a = (a gcd b) * a1 ;
a gcd b divides b by Def2;
then consider b1 being Integer such that
A3: b = (a gcd b) * b1 ;
a1 gcd b1 divides b1 by Def2;
then consider b2 being Integer such that
A4: b1 = (a1 gcd b1) * b2 ;
b = ((a gcd b) * (a1 gcd b1)) * b2 by A3, A4;
then A5: (a gcd b) * (a1 gcd b1) divides b ;
a1 gcd b1 divides a1 by Def2;
then consider a2 being Integer such that
A6: a1 = (a1 gcd b1) * a2 ;
a = ((a gcd b) * (a1 gcd b1)) * a2 by A2, A6;
then (a gcd b) * (a1 gcd b1) divides a ;
then (a gcd b) * (a1 gcd b1) divides a gcd b by A5, Def2;
then consider c being Integer such that
A7: a gcd b = ((a gcd b) * (a1 gcd b1)) * c ;
(a gcd b) * 1 = (a gcd b) * ((a1 gcd b1) * c) by A7;
then 1 = (a1 gcd b1) * c by A1, XCMPLX_1:5;
then a1,b1 are_coprime by INT_1:9;
hence ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_coprime ) by A2, A3; :: thesis: verum