let a, b be non zero Integer; :: thesis: for p being odd prime Nat st |.a.| <> |.b.| & not p divides b holds
p |-count ((a |^ 2) - (b |^ 2)) = max ((p |-count (a - b)),(p |-count (a + b)))
let p be odd prime Nat; :: thesis: ( |.a.| <> |.b.| & not p divides b implies p |-count ((a |^ 2) - (b |^ 2)) = max ((p |-count (a - b)),(p |-count (a + b))) )
assume A1: ( |.a.| <> |.b.| & not p divides b ) ; :: thesis: p |-count ((a |^ 2) - (b |^ 2)) = max ((p |-count (a - b)),(p |-count (a + b)))
A2: ( not p is trivial & a - b <> 0 & a + b <> 0 ) by A1, ABS1;
( p divides a - b implies not p divides a + b ) by A1, SUD;
then A3: ( p |-count (a - b) <> 0 implies p |-count (a + b) = 0 ) by A2, NAT327;
p |-count ((a |^ 2) - (b |^ 2)) = p |-count ((a - b) * (a + b)) by NEWTON01:1
.= (p |-count (a - b)) + (p |-count (a + b)) by A2, NAT328 ;
hence p |-count ((a |^ 2) - (b |^ 2)) = max ((p |-count (a - b)),(p |-count (a + b))) by A3, XXREAL_0:def 10; :: thesis: verum