let i, j be Integer; :: thesis: ( i >= 0 & j > 0 implies i gcd j = j gcd (i mod j) )
assume that
A1: i >= 0 and
A2: j > 0 ; :: thesis: i gcd j = j gcd (i mod j)
A3: abs j > 0 by A2, ABSVALUE:def 1;
thus i gcd j = (abs i) gcd (abs j) by INT_2:51
.= (abs j) gcd ((abs i) mod (abs j)) by A3, Th28
.= (abs j) gcd (abs ((abs i) mod (abs j))) by ABSVALUE:def 1
.= j gcd ((abs i) mod (abs j)) by INT_2:51
.= j gcd (i mod j) by A1, A2, INT_2:49 ; :: thesis: verum