let p be prime Nat; :: thesis: for a, b being Nat st a <> b holds
p |-count (a + b) >= p |-count (a gcd b)
let a, b be Nat; :: thesis: ( a <> b implies p |-count (a + b) >= p |-count (a gcd b) )
assume A1: a <> b ; :: thesis: p |-count (a + b) >= p |-count (a gcd b)
A1a: ( a <> 0 or b <> 0 ) by A1;
then consider k, l being Integer such that
A2: ( a = (a gcd b) * k & b = (a gcd b) * l & k,l are_coprime ) by INT_2:23;
( k >= 0 & l >= 0 ) by A1a, A2;
then ( k in NAT & l in NAT ) by INT_1:3;
then reconsider k = k, l = l as Nat ;
A4: ( not k is zero or not l is zero ) by A2;
p |-count (a + b) = p |-count ((k + l) * (a gcd b)) by A2
.= (p |-count (k + l)) + (p |-count (a gcd b)) by A1a, A4, NAT_3:28 ;
hence p |-count (a + b) >= p |-count (a gcd b) by NAT_1:12; :: thesis: verum