let k be natural number ; :: thesis: for n0, m0 being non zero natural number st n0,m0 are_relative_prime holds
k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)
let n0, m0 be non zero natural number ; :: thesis: ( n0,m0 are_relative_prime implies k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) )
assume A1: n0,m0 are_relative_prime ; :: 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)

thus k gcd (n0 * m0) = abs (n0 * m0) by A2, WSIERP_1:13
.= (abs n0) * (abs m0) by COMPLEX1:151
.= (k gcd n0) * (abs m0) by A2, WSIERP_1:13
.= (k gcd n0) * (k gcd m0) by A2, WSIERP_1:13 ; :: thesis: verum

end;

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

then reconsider k' = k as non zero natural number ;
reconsider a = k gcd (n0 * m0) as non empty 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 empty Nat ;
reconsider b1 = k gcd n0, b2 = k gcd m0 as non empty Nat by INT_2:5;
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 p' = p as Prime ;
A3: p' |-count a = min (p' |-count k'),(p' |-count (n0 * m0)) by Lm1
.= min (p' |-count k),((p' |-count n0) + (p' |-count m0)) by NAT_3:28 ;
A4: p' |-count b = (p' |-count b1) + (p' |-count b2) by NAT_3:28
.= (min (p' |-count k'),(p' |-count n0)) + (p' |-count b2) by Lm1
.= (min (p' |-count k'),(p' |-count n0)) + (min (p' |-count k'),(p' |-count m0)) by Lm1 ;
A5: p' > 1 by INT_2:def 5;
n0 gcd m0 = 1 by A1, INT_2:def 4;
then p' |-count 1 = min (p' |-count n0),(p' |-count m0) by Lm1;
then A6: min (p' |-count n0),(p' |-count m0) = 0 by A5, NAT_3:21;

per cases ( p' |-count n0 = 0 or p' |-count m0 = 0 ) by A6, XXREAL_0:15;

suppose A7: p' |-count n0 = 0 ; :: thesis: p |-count a = p |-count b

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

end;

suppose A8: p' |-count m0 = 0 ; :: thesis: p |-count a = p |-count b

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

end;

end;

end;

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

end;

end;