let a, b, c, d be Integer; :: thesis: ( (a * b) gcd (c * d) = 1 implies a gcd c = 1 )
|.a.| in NAT by INT_1:3;
then reconsider k = |.a.| as Nat ;
|.b.| in NAT by INT_1:3;
then reconsider m = |.b.| as Nat ;
|.c.| in NAT by INT_1:3;
then reconsider l = |.c.| as Nat ;
|.d.| in NAT by INT_1:3;
then reconsider n = |.d.| as Nat ;
assume (a * b) gcd (c * d) = 1 ; :: thesis: a gcd c = 1
then 1 = |.(a * b).| gcd |.(c * d).| by INT_2:34
.= (|.a.| * |.b.|) gcd |.(c * d).| by COMPLEX1:65
.= (|.a.| * |.b.|) gcd (|.c.| * |.d.|) by COMPLEX1:65 ;
then k * m,l * n are_coprime ;
then k,l are_coprime by NEWTON01:41;
hence a gcd c = 1 by INT_2:34; :: thesis: verum