let a, b be non empty Nat; :: thesis: ( a,b are_relative_prime implies ppf (a * b) = (ppf a) + (ppf b) )
assume A1: a,b are_relative_prime ; :: thesis: ppf (a * b) = (ppf a) + (ppf b)
reconsider an = a, bn = b as non empty natural number ;

now

let i be set ; :: thesis: ( i in SetPrimes implies (ppf (a * b)) . b₁ = ((ppf a) + (ppf b)) . b₁ )
assume A2: i in SetPrimes ; :: thesis: (ppf (a * b)) . b₁ = ((ppf a) + (ppf b)) . b₁
reconsider p = i as prime Element of NAT by A2, NEWTON:def 6;
A3: p |-count (an * bn) = (p |-count a) + (p |-count b) by Th28;
A4: p > 1 by INT_2:def 5;
A5: a gcd b = 1 by A1, INT_2:def 4;

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

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

then A7: ( p |-count a = 0 & p |-count b = 0 ) by A3;
thus (ppf (a * b)) . i = 0 by A6, Th55
.= 0 + ((ppf b) . i) by A7, Th55
.= ((ppf a) . i) + ((ppf b) . i) by A7, Th55
.= ((ppf a) + (ppf b)) . i by POLYNOM1:def 5 ; :: thesis: verum

end;

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

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

proof

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

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

A10: now

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

end;

hence (ppf (a * b)) . i = p |^ (p |-count a) by A3, A8, Th56
.= ((ppf a) . p) + 0 by A9, Th56
.= ((ppf a) . p) + ((ppf b) . p) by A10, Th55
.= ((ppf a) + (ppf b)) . i by POLYNOM1:def 5 ;
:: thesis: verum

end;

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

A17: now

assume A18: p |-count a <> 0 ; :: thesis: contradiction
consider kb being Nat such that
A19: p |-count b = kb + 1 by A16, NAT_1:6;
p |^ (p |-count b) divides b by A4, Def7;
then p * (p |^ kb) divides b by A19, NEWTON:11;
then consider lb being Nat such that
A20: b = (p * (p |^ kb)) * lb by NAT_D:def 3;
b = p * ((p |^ kb) * lb) by A20;
then A21: p divides b by NAT_D:def 3;
consider ka being Nat such that
A22: p |-count a = ka + 1 by A18, NAT_1:6;
p |^ (p |-count a) divides a by A4, Def7;
then p * (p |^ ka) divides a by A22, NEWTON:11;
then consider la being Nat such that
A23: a = (p * (p |^ ka)) * la by NAT_D:def 3;
a = p * ((p |^ ka) * la) by A23;
then p divides a by NAT_D:def 3;
then p divides 1 by A5, A21, NAT_D:def 5;
hence contradiction by A4, NAT_D:7; :: thesis: verum

end;

hence (ppf (a * b)) . i = p |^ (p |-count b) by A3, A8, Th56
.= 0 + ((ppf b) . p) by A16, Th56
.= ((ppf a) . p) + ((ppf b) . p) by A17, Th55
.= ((ppf a) + (ppf b)) . i by POLYNOM1:def 5 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

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