let n be Nat; :: thesis: for a being non trivial Nat
for x being positive Nat st a > (2 * n) * (x |^ n) holds
( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) )
let a be non trivial Nat; :: thesis: for x being positive Nat st a > (2 * n) * (x |^ n) holds
( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) )
let x be positive Nat; :: thesis: ( a > (2 * n) * (x |^ n) implies ( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) ) )
A1: ( (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) <= (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) <= (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) ) by Th21;
assume A2: a > (2 * n) * (x |^ n) ; :: thesis: ( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) )
A3: 1 - (n * (1 / (2 * a))) = 1 - ((n * 1) / (2 * a)) by XCMPLX_1:74;
(2 * (x |^ n)) * n >= 1 * n by XREAL_1:64, NAT_1:14;
then a >= n by A2, XXREAL_0:2;
then a - n >= n - n by XREAL_1:9;
then A4: (a - n) + a >= a + 0 by XREAL_1:6;
then n / ((2 * a) - n) <= n / a by XREAL_1:118;
then 1 + (n / ((2 * a) - n)) <= 1 + (n / a) by XREAL_1:6;
then A5: (x |^ n) * (1 + (n / ((2 * a) - n))) <= (x |^ n) * (1 + (n / a)) by XREAL_1:64;
A6: (2 * a) - n > 0 by A4;
A7: 1 / 1 >= 1 / (2 * a) by XREAL_1:118, NAT_1:14;
2 * a > n by A6, XREAL_1:47;
then n / (2 * a) < 1 by XREAL_1:191;
then A8: 1 - (n / (2 * a)) > 1 - 1 by XREAL_1:10;
( 1 - 1 <= 1 - (1 / (2 * a)) & 1 - (1 / (2 * a)) <= 1 - 0 ) by A7, XREAL_1:10;
then (1 - (1 / (2 * a))) |^ n >= 1 - (n / (2 * a)) by Lm5, A3;
then 1 / ((1 - (1 / (2 * a))) |^ n) <= 1 / (1 - (n / (2 * a))) by A8, XREAL_1:118;
then A9: (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) <= (x |^ n) * (1 / (1 - (n / (2 * a)))) by XREAL_1:64;
1 - (n / (2 * a)) = ((2 * a) / (2 * a)) - (n / (2 * a)) by XCMPLX_1:60
.= ((2 * a) - n) / (2 * a) by XCMPLX_1:120 ;
then A10: 1 / (1 - (n / (2 * a))) = (((2 * a) - n) + n) / ((2 * a) - n) by XCMPLX_1:57
.= (((2 * a) - n) / ((2 * a) - n)) + (n / ((2 * a) - n)) by XCMPLX_1:62
.= 1 + (n / ((2 * a) - n)) by XCMPLX_1:60, A4 ;
A11: (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) <= (x |^ n) * (1 + (n / a)) by A5, A9, A10, XXREAL_0:2;
(2 * n) * (x |^ n) = 2 * (n * (x |^ n)) ;
then n * (x |^ n) < a / 2 by A2, XREAL_1:81;
then n * (x |^ n) < (1 / 2) * a ;
then (n * (x |^ n)) / a < 1 / 2 by XREAL_1:83;
then (n / a) * (x |^ n) < 1 / 2 by XCMPLX_1:74;
then (x |^ n) + ((x |^ n) * (n / a)) < (x |^ n) + (1 / 2) by XREAL_1:6;
then A12: (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) < (x |^ n) + (1 / 2) by A11, XXREAL_0:2;
1 >= 1 / ((2 * a) * x) by XREAL_1:185, NAT_1:14;
then ( 1 - 1 <= 1 - (1 / ((2 * a) * x)) & 1 - (1 / ((2 * a) * x)) <= 1 - 0 ) by XREAL_1:10;
then A13: (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) >= (x |^ n) * (1 - (n * (1 / ((2 * a) * x)))) by Lm5, XREAL_1:64;
((x |^ n) * (n * (1 / ((2 * a) * x)))) * 2 = ((x |^ n) * ((n * 1) / ((2 * a) * x))) * 2 by XCMPLX_1:74
.= ((x |^ n) * 2) * (n / ((2 * a) * x))
.= (((x |^ n) * 2) * n) / ((2 * a) * x) by XCMPLX_1:74 ;
then A14: ((x |^ n) * (n * (1 / ((2 * a) * x)))) * 2 < a / ((2 * a) * x) by A2, XREAL_1:74;
(2 * x) * a >= 1 * a by XREAL_1:64, NAT_1:14;
then a / ((2 * a) * x) <= 1 by XREAL_1:183;
then ((x |^ n) * (n * (1 / ((2 * a) * x)))) * 2 < 1 by A14, XXREAL_0:2;
then (x |^ n) * (n * (1 / ((2 * a) * x))) < 1 / 2 by XREAL_1:81;
then (x |^ n) - ((x |^ n) * (n * (1 / ((2 * a) * x)))) > (x |^ n) - (1 / 2) by XREAL_1:15;
then (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) > (x |^ n) - (1 / 2) by A13, XXREAL_0:2;
hence ( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) ) by A12, A1, XXREAL_0:2; :: thesis: verum