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_relative_prime ) )
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_relative_prime )
then A1: a gcd b <> 0 by Th35;
a gcd b divides a by Def3;
then consider a1 being Integer such that
A2: a = (a gcd b) * a1 by INT_1:def 9;
a gcd b divides b by Def3;
then consider b1 being Integer such that
A3: b = (a gcd b) * b1 by INT_1:def 9;
a1 gcd b1 divides b1 by Def3;
then consider b2 being Integer such that
A4: b1 = (a1 gcd b1) * b2 by INT_1:def 9;
b = ((a gcd b) * (a1 gcd b1)) * b2 by A3, A4;
then A5: (a gcd b) * (a1 gcd b1) divides b by INT_1:def 9;
a1 gcd b1 divides a1 by Def3;
then consider a2 being Integer such that
A6: a1 = (a1 gcd b1) * a2 by INT_1:def 9;
a = ((a gcd b) * (a1 gcd b1)) * a2 by A2, A6;
then (a gcd b) * (a1 gcd b1) divides a by INT_1:def 9;
then (a gcd b) * (a1 gcd b1) divides a gcd b by A5, Def3;
then consider c being Integer such that
A7: a gcd b = ((a gcd b) * (a1 gcd b1)) * c by INT_1:def 9;
(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:22;
then a1,b1 are_relative_prime by Def4, NAT_1:2;
hence ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) by A2, A3; :: thesis: verum