let p be prime Nat; for a, b being Integer st |.a.| <> |.b.| holds
p |-count ((a |^ 3) - (b |^ 3)) = (p |-count (a - b)) + (p |-count (((a |^ 2) + (a * b)) + (b |^ 2)))
let a, b be Integer; ( |.a.| <> |.b.| implies p |-count ((a |^ 3) - (b |^ 3)) = (p |-count (a - b)) + (p |-count (((a |^ 2) + (a * b)) + (b |^ 2))) )
assume A1:
|.a.| <> |.b.|
; p |-count ((a |^ 3) - (b |^ 3)) = (p |-count (a - b)) + (p |-count (((a |^ 2) + (a * b)) + (b |^ 2)))
( a - b <> 0 & a + b <> 0 )
by A1, ABS1;
then reconsider t = |.(a - b).| as non zero Nat ;
A3:
( |.a.| |^ 2 = a |^ 2 & |.b.| |^ 2 = b |^ 2 )
by COMPLEX175;
(2 * |.a.|) * |.b.| < (|.a.| |^ 2) + (|.b.| |^ 2)
by A1, NEWTON02:55;
then
2 * (|.a.| * |.b.|) < (a |^ 2) + (b |^ 2)
by A3;
then A4:
2 * |.(a * b).| < (a |^ 2) + (b |^ 2)
by COMPLEX1:65;
2 * |.(a * b).| >= 1 * |.(a * b).|
by XREAL_1:64;
then A5:
(a |^ 2) + (b |^ 2) > |.(a * b).|
by A4, XXREAL_0:2;
|.(- (a * b)).| >= - (a * b)
by ABSVALUE:4;
then
|.(a * b).| >= - (a * b)
by COMPLEX1:52;
then
(a |^ 2) + (b |^ 2) > - (a * b)
by A5, XXREAL_0:2;
then
((a |^ 2) + (b |^ 2)) + (a * b) > (- (a * b)) + (a * b)
by XREAL_1:6;
then reconsider u = |.(((a |^ 2) + (a * b)) + (b |^ 2)).| as non zero Nat ;
p |-count ((a |^ 3) - (b |^ 3)) =
p |-count |.((((a |^ 2) + (b |^ 2)) + (a * b)) * (a - b)).|
by N3
.=
p |-count (t * u)
by COMPLEX1:65
.=
(p |-count t) + (p |-count u)
by NAT_3:28
;
hence
p |-count ((a |^ 3) - (b |^ 3)) = (p |-count (a - b)) + (p |-count (((a |^ 2) + (a * b)) + (b |^ 2)))
; verum