let a, b be non zero Nat; :: thesis: ( a,b are_coprime implies Bnumber_of_divisors (a * b) = (Bnumber_of_divisors a) + (Bnumber_of_divisors b) )
reconsider an = a, bn = b as non zero Nat ;
assume A1: a,b are_coprime ; :: thesis: Bnumber_of_divisors (a * b) = (Bnumber_of_divisors a) + (Bnumber_of_divisors b)

now :: thesis: for i being object st i in SetPrimes holds
(Bnumber_of_divisors (a * b)) . i = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i

let i be object ; :: thesis: ( i in SetPrimes implies (Bnumber_of_divisors (a * b)) . b₁ = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . b₁ )
assume i in SetPrimes ; :: thesis: (Bnumber_of_divisors (a * b)) . b₁ = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . b₁
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
A2: p |-count (an * bn) = (p |-count a) + (p |-count b) by NAT_3:28;
A4: p > 1 by INT_2:def 4;

per cases ( p |-count (a * b) = 0 or p |-count (a * b) <> 0 ) ;

suppose A5: p |-count (a * b) = 0 ; :: thesis: (Bnumber_of_divisors (a * b)) . b₁ = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . b₁

then A6: p |-count b = 0 by A2;
A7: p |-count a = 0 by A2, A5;
thus (Bnumber_of_divisors (a * b)) . i = 0 by A5, Th48
.= 0 + ((Bnumber_of_divisors b) . i) by A6, Th48
.= ((Bnumber_of_divisors a) . i) + ((Bnumber_of_divisors b) . i) by A7, Th48
.= ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i by PRE_POLY:def 5 ; :: thesis: verum

end;

suppose A8: p |-count (a * b) <> 0 ; :: thesis: (Bnumber_of_divisors (a * b)) . b₁ = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . b₁

thus (Bnumber_of_divisors (a * b)) . i = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i :: thesis: verum

proof

per cases ( p |-count a <> 0 or p |-count b <> 0 ) by A2, A8;

suppose A9: p |-count a <> 0 ; :: thesis: (Bnumber_of_divisors (a * b)) . i = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i

A10: now :: thesis: not p |-count b <> 0

consider ka being Nat such that
A11: p |-count a = ka + 1 by A9, NAT_1:6;
reconsider ka = ka as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count a) divides a by A4, NAT_3:def 7;
then p * (p |^ ka) divides a by A11, NEWTON:6;
then consider la being Nat such that
A12: a = (p * (p |^ ka)) * la by NAT_D:def 3;
a = p * ((p |^ ka) * la) by A12;
then A13: p divides a ;
assume p |-count b <> 0 ; :: thesis: contradiction
then consider kb being Nat such that
A14: p |-count b = kb + 1 by NAT_1:6;
reconsider kb = kb as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count b) divides b by A4, NAT_3:def 7;
then p * (p |^ kb) divides b by A14, NEWTON:6;
then consider lb being Nat such that
A15: b = (p * (p |^ kb)) * lb by NAT_D:def 3;
b = p * ((p |^ kb) * lb) by A15;
then p divides b ;
then p divides 1 by A1, A13, NAT_D:def 5;
hence contradiction by A4, NAT_D:7; :: thesis: verum

end;

thus (Bnumber_of_divisors (a * b)) . i = (p |-count (a * b)) + 1 by A8, Th49
.= ((p |-count a) + (p |-count b)) + 1 by NAT_3:28
.= ((p |-count a) + 1) + (p |-count b)
.= ((Bnumber_of_divisors a) . p) + (p |-count b) by A9, Th49
.= ((Bnumber_of_divisors a) . p) + ((Bnumber_of_divisors b) . p) by A10, Th48
.= ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i by PRE_POLY:def 5 ; :: thesis: verum

end;

suppose A16: p |-count b <> 0 ; :: thesis: (Bnumber_of_divisors (a * b)) . i = ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i

A17: now :: thesis: not p |-count a <> 0

assume p |-count a <> 0 ; :: thesis: contradiction
then consider ka being Nat such that
A18: p |-count a = ka + 1 by NAT_1:6;
reconsider ka = ka as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count a) divides a by A4, NAT_3:def 7;
then p * (p |^ ka) divides a by A18, NEWTON:6;
then consider la being Nat such that
A19: a = (p * (p |^ ka)) * la by NAT_D:def 3;
a = p * ((p |^ ka) * la) by A19;
then A20: p divides a ;
consider kb being Nat such that
A21: p |-count b = kb + 1 by A16, NAT_1:6;
reconsider kb = kb as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count b) divides b by A4, NAT_3:def 7;
then p * (p |^ kb) divides b by A21, NEWTON:6;
then consider lb being Nat such that
A22: b = (p * (p |^ kb)) * lb by NAT_D:def 3;
b = p * ((p |^ kb) * lb) by A22;
then p divides b ;
then p divides 1 by A1, A20, NAT_D:def 5;
hence contradiction by A4, NAT_D:7; :: thesis: verum

end;

thus (Bnumber_of_divisors (a * b)) . i = (p |-count (a * b)) + 1 by A8, Th49
.= ((p |-count a) + (p |-count b)) + 1 by NAT_3:28
.= (p |-count a) + ((p |-count b) + 1)
.= (p |-count a) + ((Bnumber_of_divisors b) . p) by A16, Th49
.= ((Bnumber_of_divisors a) . p) + ((Bnumber_of_divisors b) . p) by A17, Th48
.= ((Bnumber_of_divisors a) + (Bnumber_of_divisors b)) . i by PRE_POLY:def 5 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence Bnumber_of_divisors (a * b) = (Bnumber_of_divisors a) + (Bnumber_of_divisors b) by PBOOLE:3; :: thesis: verum