let m, n be Nat; :: thesis: ( m > 0 implies n gcd m = m gcd (n mod m) )
set r = n mod m;
set x = n gcd m;
set y = m gcd (n mod m);
assume m > 0 ; :: thesis: n gcd m = m gcd (n mod m)
then consider t being Nat such that
A1: ( n = (m * t) + (n mod m) & n mod m < m ) by Def2;
reconsider t = t as Element of NAT by ORDINAL1:def 13;
A2: ( n gcd m divides n & n gcd m divides m ) by Def5;
then n gcd m divides n mod m by Th11;
then A3: n gcd m divides m gcd (n mod m) by A2, Def5;
A4: ( m gcd (n mod m) divides m & m gcd (n mod m) divides n mod m ) by Def5;
then m gcd (n mod m) divides m * t by Th9;
then m gcd (n mod m) divides n by A1, A4, Th8;
then m gcd (n mod m) divides n gcd m by A4, Def5;
hence n gcd m = m gcd (n mod m) by A3, Th5; :: thesis: verum