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)

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

end;

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;.= |.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

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

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

hence
k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)
by NAT_4:21; :: thesis: verum
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 ;

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