let a be Real; for n, x, y being positive Nat st a > 0 & 2 <= n & (x |^ n) - (y |^ n) = a holds
( x < (n - 1) -Root a & y < (n - 1) -Root a )
let n, x, y be positive Nat; ( a > 0 & 2 <= n & (x |^ n) - (y |^ n) = a implies ( x < (n - 1) -Root a & y < (n - 1) -Root a ) )
assume that
A1:
a > 0
and
A2:
2 <= n
and
A3:
(x |^ n) - (y |^ n) = a
; ( x < (n - 1) -Root a & y < (n - 1) -Root a )
set F = (x,y) Subnomial (n - 1);
A4:
2 - 1 <= n - 1
by A2, XREAL_1:7;
A5:
a = (x - y) * (Sum ((x,y) Subnomial (n - 1)))
by A3, NEWTON04:51;
then A6:
x - y > 0
by A1;
then reconsider w = x - y as Element of NAT by INT_1:3;
w >= 0 + 1
by A6, NAT_1:13;
then A7:
Sum ((x,y) Subnomial (n - 1)) <= 1 * a
by A5, XREAL_1:97;
(x |^ (n - 1)) + (y |^ (n - 1)) <= Sum ((x,y) Subnomial (n - 1))
by A4, NEWTON04:84;
then A8:
(x |^ (n - 1)) + (y |^ (n - 1)) <= a
by A7, XXREAL_0:2;
( (x |^ (n - 1)) + 0 < (x |^ (n - 1)) + (y |^ (n - 1)) & (y |^ (n - 1)) + 0 < (x |^ (n - 1)) + (y |^ (n - 1)) )
by XREAL_1:6;
then
( x |^ (n - 1) < a & y |^ (n - 1) < a )
by A8, XXREAL_0:2;
then
( (n - 1) -Root (x |^ (n - 1)) < (n - 1) -Root a & (n - 1) -Root (y |^ (n - 1)) < (n - 1) -Root a )
by A4, PREPOWER:28;
hence
( x < (n - 1) -Root a & y < (n - 1) -Root a )
by A4, PREPOWER:19; verum