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