let p be prime Nat; :: thesis: for a, b being Integer st |.a.| <> |.b.| holds
p |-count ((a |^ 2) - (b |^ 2)) = (p |-count (a - b)) + (p |-count (a + b))
let a, b be Integer; :: thesis: ( |.a.| <> |.b.| implies p |-count ((a |^ 2) - (b |^ 2)) = (p |-count (a - b)) + (p |-count (a + b)) )
assume A1: |.a.| <> |.b.| ; :: thesis: p |-count ((a |^ 2) - (b |^ 2)) = (p |-count (a - b)) + (p |-count (a + b))
( a - b <> 0 & a + b <> 0 ) by A1, ABS1;
then reconsider t = |.(a - b).|, u = |.(a + b).| as non zero Nat ;
p |-count ((a |^ 2) - (b |^ 2)) = p |-count |.((a + b) * (a - b)).| by NEWTON01:1
.= p |-count (t * u) by COMPLEX1:65
.= (p |-count |.(a - b).|) + (p |-count |.(a + b).|) by NAT_3:28 ;
hence p |-count ((a |^ 2) - (b |^ 2)) = (p |-count (a - b)) + (p |-count (a + b)) ; :: thesis: verum