let n be Nat; :: thesis: for a being non trivial Nat
for x being positive Nat holds
( (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)) )
let a be non trivial Nat; :: thesis: for x being positive Nat holds
( (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)) )
let x be positive Nat; :: thesis: ( (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)) )
set z = n;
1 - (1 / ((2 * a) * x)) = (((2 * a) * x) / ((2 * a) * x)) - (1 / ((2 * a) * x)) by XCMPLX_1:60
.= (((2 * a) * x) - 1) / ((2 * a) * x) by XCMPLX_1:120 ;
then x * (1 - (1 / ((2 * a) * x))) = (((2 * a) * x) - 1) / (2 * a) by XCMPLX_1:92;
then A1: (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) = ((((2 * a) * x) - 1) / (2 * a)) to_power n by NEWTON:7
.= ((((2 * a) * x) - 1) to_power n) / ((2 * a) to_power n) by POWER:31 ;
A2: ( ((2 * a) - 1) |^ n <= Py (a,(n + 1)) & Py (a,(n + 1)) <= (2 * a) |^ n ) by Th20;
A3: ( ((2 * (a * x)) - 1) |^ n <= Py ((a * x),(n + 1)) & Py ((a * x),(n + 1)) <= (2 * (a * x)) |^ n ) by Th20;
((((2 * a) * x) - 1) |^ n) * (Py (a,(n + 1))) <= (Py ((a * x),(n + 1))) * ((2 * a) |^ n) by A2, A3, XREAL_1:66;
hence (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) <= (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) by A1, XREAL_1:102; :: thesis: (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) <= (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n))
a >= 1 by NAT_1:14;
then a + a >= 1 + 1 by XREAL_1:7;
then 1 * (2 * a) > 1 by NAT_1:13;
then 1 > 1 / (2 * a) by XREAL_1:83;
then A4: 1 - (1 / (2 * a)) > (1 / (2 * a)) - (1 / (2 * a)) by XREAL_1:14;
A5: (Py ((a * x),(n + 1))) * (((2 * a) - 1) |^ n) <= (((2 * a) * x) |^ n) * (Py (a,(n + 1))) by A2, A3, XREAL_1:66;
(2 * a) / (2 * a) = 1 by XCMPLX_1:60;
then ((2 * a) - 1) / (2 * a) = 1 - (1 / (2 * a)) by XCMPLX_1:120;
then (2 * a) / ((2 * a) - 1) = 1 / (1 - (1 / (2 * a))) by XCMPLX_1:57;
then ((2 * a) * x) / ((2 * a) - 1) = x * (1 / (1 - (1 / (2 * a)))) by XCMPLX_1:74;
then ((2 * a) * x) / ((2 * a) - 1) = (x * 1) / (1 - (1 / (2 * a))) by XCMPLX_1:74;
then (((2 * a) * x) to_power n) / (((2 * a) - 1) to_power n) = (x / (1 - (1 / (2 * a)))) to_power n by POWER:31
.= (1 * (x to_power n)) / ((1 - (1 / (2 * a))) to_power n) by A4, POWER:31
.= (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) by XCMPLX_1:74 ;
hence (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) <= (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) by A5, XREAL_1:102; :: thesis: verum