let k, m, n be Nat; :: thesis: (k * m) gcd (k * n) = k * (m gcd n)

per cases ( k <> 0 or k = 0 ) ;

suppose A1: k <> 0 ; :: thesis: (k * m) gcd (k * n) = k * (m gcd n)

( k divides k * m & k divides k * n ) ;
then k divides (k * m) gcd (k * n) by NAT_D:def 5;
then consider k9 being Nat such that
A2: (k * m) gcd (k * n) = k * k9 by NAT_D:def 3;
reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;

now :: thesis: ( k9 divides m & k9 divides n & ( for p being Nat st p divides m & p divides n holds
p divides k9 ) )

k * k9 divides k * m by A2, NAT_D:def 5;
hence k9 divides m by A1, Th7; :: thesis: ( k9 divides n & ( for p being Nat st p divides m & p divides n holds
p divides k9 ) )
k * k9 divides k * n by A2, NAT_D:def 5;
hence k9 divides n by A1, Th7; :: thesis: for p being Nat st p divides m & p divides n holds
p divides k9
let p be Nat; :: thesis: ( p divides m & p divides n implies p divides k9 )
reconsider p9 = p as Element of NAT by ORDINAL1:def 12;
assume ( p divides m & p divides n ) ; :: thesis: p divides k9
then ( k * p9 divides k * m & k * p9 divides k * n ) by Th7;
then k * p divides k * k9 by A2, NAT_D:def 5;
then p9 divides k9 by A1, Th7;
hence p divides k9 ; :: thesis: verum

end;

hence (k * m) gcd (k * n) = k * (m gcd n) by A2, NAT_D:def 5; :: thesis: verum

end;

suppose k = 0 ; :: thesis: (k * m) gcd (k * n) = k * (m gcd n)

hence (k * m) gcd (k * n) = k * (m gcd n) by NEWTON:52; :: thesis: verum

end;

end;