let k be Nat; :: thesis: for n0, m0 being non zero Nat st n0,m0 are_coprime holds
k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)
let n0, m0 be non zero Nat; :: thesis: ( n0,m0 are_coprime implies k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) )
assume A1: n0,m0 are_coprime ; :: thesis: k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)

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

suppose A2: k = 0 ; :: thesis: k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)

hence k gcd (n0 * m0) = |.(n0 * m0).| by WSIERP_1:8
.= |.n0.| * |.m0.| by COMPLEX1:65
.= (k gcd n0) * |.m0.| by A2, WSIERP_1:8
.= (k gcd n0) * (k gcd m0) by A2, WSIERP_1:8 ;
:: thesis: verum

end;

suppose k <> 0 ; :: thesis: k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)

then reconsider k9 = k as non zero Nat ;
reconsider a = k gcd (n0 * m0) as non zero Nat by INT_2:5;
reconsider b1 = k gcd n0, b2 = k gcd m0 as non zero Nat by INT_2:5;
( k gcd n0 <> 0 & k gcd m0 <> 0 ) by INT_2:5;
then reconsider b = (k gcd n0) * (k gcd m0) as non zero Nat ;
for p being Element of NAT st p is prime holds
p |-count a = p |-count b

proof

let p be Element of NAT ; :: thesis: ( p is prime implies p |-count a = p |-count b )
assume p is prime ; :: thesis: p |-count a = p |-count b
then reconsider p9 = p as Prime ;
A3: p9 |-count a = min ((p9 |-count k9),(p9 |-count (n0 * m0))) by Lm1
.= min ((p9 |-count k),((p9 |-count n0) + (p9 |-count m0))) by NAT_3:28 ;
n0 gcd m0 = 1 by A1, INT_2:def 3;
then ( p9 > 1 & p9 |-count 1 = min ((p9 |-count n0),(p9 |-count m0)) ) by Lm1, INT_2:def 4;
then A4: min ((p9 |-count n0),(p9 |-count m0)) = 0 by NAT_3:21;
A5: p9 |-count b = (p9 |-count b1) + (p9 |-count b2) by NAT_3:28
.= (min ((p9 |-count k9),(p9 |-count n0))) + (p9 |-count b2) by Lm1
.= (min ((p9 |-count k9),(p9 |-count n0))) + (min ((p9 |-count k9),(p9 |-count m0))) by Lm1 ;

per cases ( p9 |-count n0 = 0 or p9 |-count m0 = 0 ) by A4, XXREAL_0:15;

suppose A6: p9 |-count n0 = 0 ; :: thesis: p |-count a = p |-count b

then min ((p9 |-count k),(p9 |-count n0)) = p9 |-count n0 by XXREAL_0:def 9;
hence p |-count a = p |-count b by A3, A5, A6; :: thesis: verum

end;

suppose A7: p9 |-count m0 = 0 ; :: thesis: p |-count a = p |-count b

then min ((p9 |-count k),(p9 |-count m0)) = p9 |-count m0 by XXREAL_0:def 9;
hence p |-count a = p |-count b by A3, A5, A7; :: thesis: verum

end;

end;

end;

hence k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) by NAT_4:21; :: thesis: verum

end;

end;