let m, n be natural Number ; :: 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) and
n mod m < m by Def2;
reconsider t = t as Element of NAT by ORDINAL1:def 12;
A2: n gcd m divides n by Def5;
A3: n gcd m divides m by Def5;
then n gcd m divides n mod m by A2, Th11;
then A4: n gcd m divides m gcd (n mod m) by A3, Def5;
A5: m gcd (n mod m) divides m by Def5;
A6: m gcd (n mod m) divides n mod m by Def5;
m gcd (n mod m) divides m * t by A5, Th9;
then m gcd (n mod m) divides n by A1, A6, Th8;
then m gcd (n mod m) divides n gcd m by A5, Def5;
hence n gcd m = m gcd (n mod m) by A4, Th5; :: thesis: verum