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 )
;

end;

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;

end;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 ) )

hence
(k * m) gcd (k * n) = k * (m gcd n)
by A2, NAT_D:def 5; :: thesis: verump 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 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