let k, m, n be Element of 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 ) by NAT_D:9;
then k divides (k * m) gcd (k * n) by NAT_D:def 5;
then consider k' being Nat such that
A2: (k * m) gcd (k * n) = k * k' by NAT_D:def 3;
reconsider k' = k' as Element of NAT by ORDINAL1:def 13;

now

k * k' divides k * m by A2, NAT_D:def 5;
hence k' divides m by A1, Th7; :: thesis: ( k' divides n & ( for p being Nat st p divides m & p divides n holds
p divides k' ) )
k * k' divides k * n by A2, NAT_D:def 5;
hence k' divides n by A1, Th7; :: thesis: for p being Nat st p divides m & p divides n holds
p divides k'
let p be Nat; :: thesis: ( p divides m & p divides n implies p divides k' )
reconsider p' = p as Element of NAT by ORDINAL1:def 13;
assume ( p divides m & p divides n ) ; :: thesis: p divides k'
then ( k * p' divides k * m & k * p' divides k * n ) by Th7;
then k * p divides k * k' by A2, NAT_D:def 5;
then p' divides k' by A1, Th7;
hence p divides k' ; :: 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:65; :: thesis: verum

end;

end;