let n be Nat; :: thesis: for p being Prime st n <> 0 holds
for x, y being positive Nat holds not x * (x + 1) = ((p |^ (2 * n)) * y) * (y + 1)
let p be Prime; :: thesis: ( n <> 0 implies for x, y being positive Nat holds not x * (x + 1) = ((p |^ (2 * n)) * y) * (y + 1) )
assume A1: n <> 0 ; :: thesis: for x, y being positive Nat holds not x * (x + 1) = ((p |^ (2 * n)) * y) * (y + 1)
given x, y being positive Nat such that A2: x * (x + 1) = ((p |^ (2 * n)) * y) * (y + 1) ; :: thesis: contradiction
A3: x + 0 < x + 1 by XREAL_1:8;
A4: x,x + 1 are_coprime ;
p |^ (2 * n) divides (p |^ (2 * n)) * (y * (y + 1)) ;
then ( p |^ (2 * n) divides x or p |^ (2 * n) divides x + 1 ) by A2, A4, Th107;
then ( x + 0 >= p |^ (2 * n) or x + 1 >= p |^ (2 * n) ) by NAT_D:7;
then x + 1 >= p |^ (2 * n) by A3, XXREAL_0:2;
then A5: 2 * (x + 1) >= 2 * (p |^ (2 * n)) by XREAL_1:64;
A6: p |^ (2 * n) = (p |^ n) |^ 2 by NEWTON:9;
A7: (p |^ n) |^ 2 = (p |^ n) ^2 by NEWTON:81;
A8: (((p |^ n) * ((2 * y) + 1)) + ((2 * x) + 1)) * (((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1)) = ((((p |^ n) * (p |^ n)) * ((2 * y) + 1)) * ((2 * y) + 1)) - ((((4 * ((p |^ n) |^ 2)) * y) * (y + 1)) + 1) by A2, A6
.= ((p |^ n) ^2) - 1 by A7 ;
then A9: ((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1) >= 0 ;
A10: (p |^ (2 * n)) - 1 = (((p |^ n) * ((2 * y) + 1)) + ((2 * x) + 1)) * (((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1)) by A6, A8, NEWTON:81;

now :: thesis: not ((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1) < 1

assume A11: ((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1) < 1 ; :: thesis: contradiction
((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1) in NAT by A9, INT_1:3;
then ((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1) = 0 by A11, NAT_1:14;
hence contradiction by A1, A10; :: thesis: verum

end;

then A12: (((p |^ n) * ((2 * y) + 1)) - ((2 * x) + 1)) * (((p |^ n) * ((2 * y) + 1)) + ((2 * x) + 1)) >= 1 * (((p |^ n) * ((2 * y) + 1)) + ((2 * x) + 1)) by XREAL_1:64;
((p |^ n) * ((2 * y) + 1)) + ((2 * x) + 1) > 0 + ((2 * x) + 1) by XREAL_1:6;
then (p |^ (2 * n)) - 1 > (2 * x) + 1 by A10, A12, XXREAL_0:2;
then ((p |^ (2 * n)) - 1) + 1 > ((2 * x) + 1) + 1 by XREAL_1:8;
then 1 * (p |^ (2 * n)) > 2 * (p |^ (2 * n)) by A5, XXREAL_0:2;
hence contradiction by XREAL_1:64; :: thesis: verum