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: |.j.| > 0 by A2, ABSVALUE:def 1;
thus i gcd j = |.i.| gcd |.j.| by INT_2:34
.= |.j.| gcd (|.i.| mod |.j.|) by A3, Th28
.= |.j.| gcd |.(|.i.| mod |.j.|).| by ABSVALUE:def 1
.= j gcd (|.i.| mod |.j.|) by INT_2:34
.= j gcd (i mod j) by A1, A2, INT_2:32 ; :: thesis: verum