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 gcd b1 = 1 or a1 gcd b1 = - 1 ) by INT_1:9;

then a1,b1 are_coprime ;

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

( 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 gcd b1 = 1 or a1 gcd b1 = - 1 ) by INT_1:9;

then a1,b1 are_coprime ;

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