let n be Nat; 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; 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; ( (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; (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; verum