let a, b, c be real positive number ; :: thesis: for n being Element of NAT st (a ^2 ) + (b ^2 ) = c ^2 & n >= 3 holds
(a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2)
let n be Element of NAT ; :: thesis: ( (a ^2 ) + (b ^2 ) = c ^2 & n >= 3 implies (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) )
A1: ( b ^2 > 0 & a ^2 > 0 ) ;
assume A2: ( (a ^2 ) + (b ^2 ) = c ^2 & n >= 3 ) ; :: thesis: (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2)
then ((c ^2 ) - (a ^2 )) + (a ^2 ) > 0 + (a ^2 ) by XREAL_1:10;
then sqrt (c ^2 ) > sqrt (a ^2 ) by SQUARE_1:95;
then c > sqrt (a ^2 ) by SQUARE_1:89;
then A3: c > a by SQUARE_1:89;
A4: n >= 1 by A2, XXREAL_0:2;
then A5: c |^ n > a |^ n by A3, PREPOWER:18;
((c ^2 ) - (b ^2 )) + (b ^2 ) > 0 + (b ^2 ) by A2, XREAL_1:10;
then sqrt (c ^2 ) > sqrt (b ^2 ) by SQUARE_1:95;
then c > sqrt (b ^2 ) by SQUARE_1:89;
then c > b by SQUARE_1:89;
then A6: c |^ n > b |^ n by A4, PREPOWER:18;
A7: ( a |^ 2 > 0 & b |^ 2 > 0 ) by A1, NEWTON:100;
then (c |^ n) * (a |^ 2) > (a |^ n) * (a |^ 2) by A5, XREAL_1:70;
then A8: (c |^ n) * (a |^ 2) > a |^ (n + 2) by NEWTON:13;
(c |^ n) * (b |^ 2) > (b |^ n) * (b |^ 2) by A6, A7, XREAL_1:70;
then (c |^ n) * (b |^ 2) > b |^ (n + 2) by NEWTON:13;
then ((c |^ n) * (a |^ 2)) + ((c |^ n) * (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) by A8, XREAL_1:10;
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:100;
then (c |^ n) * (c ^2 ) > (a |^ (n + 2)) + (b |^ (n + 2)) by A2, NEWTON:100;
then (c |^ n) * (c |^ 2) > (a |^ (n + 2)) + (b |^ (n + 2)) by NEWTON:100;
hence (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) by NEWTON:13; :: thesis: verum