let i, j be Integer; :: thesis: ( i >= 0 & j > 0 implies i gcd j = j gcd (i mod j) )
assume A1: ( i >= 0 & j > 0 ) ; :: thesis: i gcd j = j gcd (i mod j)
then A2: abs j > 0 by 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 A2, 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, INT_2:49 ; :: thesis: verum