let a, b be Element of Gauss_INT_Ring; :: thesis: for aa, bb being G_INTEG st a = aa & b = bb & aa is_associated_to bb holds
a is_associated_to b
let aa, bb be G_INTEG; :: thesis: ( a = aa & b = bb & aa is_associated_to bb implies a is_associated_to b )
assume A1: ( a = aa & b = bb ) ; :: thesis: ( not aa is_associated_to bb or a is_associated_to b )
assume aa is_associated_to bb ; :: thesis: a is_associated_to b
then A2: ( aa Divides bb & bb Divides aa ) ;
then consider cca being G_INTEG such that
A3: bb = aa * cca ;
consider ccb being G_INTEG such that
A4: aa = bb * ccb by A2;
reconsider ca = cca as Element of Gauss_INT_Ring by Th3;
reconsider cb = ccb as Element of Gauss_INT_Ring by Th3;
b = a * ca by A1, A3, Th6;
then A5: a divides b by GCD_1:def 1;
a = b * cb by A1, A4, Th6;
then b divides a by GCD_1:def 1;
hence a is_associated_to b by A5, GCD_1:def 3; :: thesis: verum