let a be Real; for k, x, y being positive Nat st a > 0 & (x |^ (2 * k)) - (y |^ (2 * k)) = a holds
( x < k -Root a & y < k -Root a )
let k, x, y be positive Nat; ( a > 0 & (x |^ (2 * k)) - (y |^ (2 * k)) = a implies ( x < k -Root a & y < k -Root a ) )
assume that
A1:
a > 0
and
A2:
(x |^ (2 * k)) - (y |^ (2 * k)) = a
; ( x < k -Root a & y < k -Root a )
A3:
1 <= k
by NAT_1:14;
( x |^ (2 * k) = (x |^ k) |^ 2 & y |^ (2 * k) = (y |^ k) |^ 2 )
by NEWTON:9;
then A4:
(x |^ (2 * k)) - (y |^ (2 * k)) = ((x |^ k) - (y |^ k)) * ((x |^ k) + (y |^ k))
by NEWTON01:1;
then
(x |^ k) - (y |^ k) > 0
by A1, A2;
then
(x |^ k) - (y |^ k) >= 0 + 1
by NAT_1:13;
then A5:
(x |^ k) + (y |^ k) <= 1 * a
by A2, A4, XREAL_1:97;
( (x |^ k) + 0 < (x |^ k) + (y |^ k) & (y |^ k) + 0 < (x |^ k) + (y |^ k) )
by XREAL_1:6;
then
( x |^ k < a & y |^ k < a )
by A5, XXREAL_0:2;
then
( k -Root (x |^ k) < k -Root a & k -Root (y |^ k) < k -Root a )
by NAT_1:14, PREPOWER:28;
hence
( x < k -Root a & y < k -Root a )
by A3, PREPOWER:19; verum