let a, b, c be positive Real; :: thesis: for n being Nat st (a ^2) + (b ^2) = c ^2 & n >= 3 holds
(a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2)
let n be Nat; :: thesis: ( (a ^2) + (b ^2) = c ^2 & n >= 3 implies (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) )
assume that
A1: (a ^2) + (b ^2) = c ^2 and
A2: n >= 3 ; :: thesis: (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2)
A3: n >= 1 by A2, XXREAL_0:2;
b ^2 > 0 ;
then A4: b |^ 2 > 0 by NEWTON:81;
((c ^2) - (b ^2)) + (b ^2) > 0 + (b ^2) by A1, XREAL_1:8;
then sqrt (c ^2) > sqrt (b ^2) by SQUARE_1:27;
then c > sqrt (b ^2) by SQUARE_1:22;
then c > b by SQUARE_1:22;
then c |^ n > b |^ n by A3, PREPOWER:10;
then (c |^ n) * (b |^ 2) > (b |^ n) * (b |^ 2) by A4, XREAL_1:68;
then A5: (c |^ n) * (b |^ 2) > b |^ (n + 2) by NEWTON:8;
a ^2 > 0 ;
then A6: a |^ 2 > 0 by NEWTON:81;
((c ^2) - (a ^2)) + (a ^2) > 0 + (a ^2) by A1, XREAL_1:8;
then sqrt (c ^2) > sqrt (a ^2) by SQUARE_1:27;
then c > sqrt (a ^2) by SQUARE_1:22;
then c > a by SQUARE_1:22;
then c |^ n > a |^ n by A3, PREPOWER:10;
then (c |^ n) * (a |^ 2) > (a |^ n) * (a |^ 2) by A6, XREAL_1:68;
then (c |^ n) * (a |^ 2) > a |^ (n + 2) by NEWTON:8;
then ((c |^ n) * (a |^ 2)) + ((c |^ n) * (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) by A5, XREAL_1:8;
then (c |^ n) * ((a |^ 2) + (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) ;
then (c |^ n) * ((a ^2) + (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) by NEWTON:81;
then (c |^ n) * (c ^2) > (a |^ (n + 2)) + (b |^ (n + 2)) by A1, NEWTON:81;
then (c |^ n) * (c |^ 2) > (a |^ (n + 2)) + (b |^ (n + 2)) by NEWTON:81;
hence (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) by NEWTON:8; :: thesis: verum