let n be Nat; for a being non trivial Nat holds
( (((2 * a) - 1) |^ n) * (a - 1) <= Px (a,(n + 1)) & Px (a,(n + 1)) <= a * ((2 * a) |^ n) & ((2 * a) - 1) |^ n <= Py (a,(n + 1)) & Py (a,(n + 1)) <= (2 * a) |^ n )
let a be non trivial Nat; ( (((2 * a) - 1) |^ n) * (a - 1) <= Px (a,(n + 1)) & Px (a,(n + 1)) <= a * ((2 * a) |^ n) & ((2 * a) - 1) |^ n <= Py (a,(n + 1)) & Py (a,(n + 1)) <= (2 * a) |^ n )
defpred S1[ Nat] means ( ((2 * a) - 1) |^ $1 <= Py (a,($1 + 1)) & Py (a,($1 + 1)) <= (2 * a) |^ $1 & (((2 * a) - 1) |^ $1) * (a - 1) <= Px (a,($1 + 1)) & Px (a,($1 + 1)) <= a * ((2 * a) |^ $1) );
A1:
(a ^2) -' 1 = (a ^2) - 1
by XREAL_1:233, NAT_1:14;
A2:
( ((2 * a) - 1) |^ 0 = 1 & (2 * a) |^ 0 = 1 )
by NEWTON:4;
A3:
a - 1 <= a - 0
by XREAL_1:10;
( Py (a,0) = 0 & Px (a,0) = 1 )
by Th6;
then
( Py (a,(1 + 0)) = 1 + (0 * a) & Px (a,(1 + 0)) = (1 * a) + (0 * ((a ^2) -' 1)) )
by Th9;
then A4:
S1[ 0 ]
by A2, A3;
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
set k1 =
k + 1;
assume A6:
S1[
k]
;
S1[k + 1]
A7:
(
Py (
a,
((k + 1) + 1))
= (Px (a,(k + 1))) + ((Py (a,(k + 1))) * a) &
Px (
a,
((k + 1) + 1))
= ((Px (a,(k + 1))) * a) + ((Py (a,(k + 1))) * ((a ^2) -' 1)) )
by Th9;
A8:
(Py (a,(k + 1))) * a <= ((2 * a) |^ k) * a
by A6, XREAL_1:64;
A9:
(((2 * a) |^ k) * a) + (((2 * a) |^ k) * a) =
((2 * a) |^ k) * (2 * a)
.=
(2 * a) |^ (k + 1)
by NEWTON:6
;
A10:
(Py (a,(k + 1))) * a >= (((2 * a) - 1) |^ k) * a
by A6, XREAL_1:64;
A11:
((((2 * a) - 1) |^ k) * (a - 1)) + ((((2 * a) - 1) |^ k) * a) =
(((2 * a) - 1) |^ k) * ((2 * a) - 1)
.=
((2 * a) - 1) |^ (k + 1)
by NEWTON:6
;
(
(Px (a,(k + 1))) * a <= (a * ((2 * a) |^ k)) * a &
(Py (a,(k + 1))) * ((a ^2) -' 1) <= ((2 * a) |^ k) * ((a ^2) -' 1) )
by A6, XREAL_1:64;
then A12:
Px (
a,
((k + 1) + 1))
<= ((a * ((2 * a) |^ k)) * a) + (((2 * a) |^ k) * ((a ^2) -' 1))
by A7, XREAL_1:7;
((a ^2) + (a ^2)) - 1
<= ((a ^2) + (a ^2)) - 0
by XREAL_1:10;
then A13:
((2 * a) |^ k) * (((a ^2) + (a ^2)) - 1) <= ((2 * a) |^ k) * ((a ^2) + (a ^2))
by XREAL_1:64;
(
(((2 * a) - 1) |^ k) * ((a ^2) -' 1) <= (Py (a,(k + 1))) * ((a ^2) -' 1) &
((((2 * a) - 1) |^ k) * (a - 1)) * a <= (Px (a,(k + 1))) * a )
by A6, XREAL_1:64;
then A14:
((((2 * a) - 1) |^ k) * ((a ^2) -' 1)) + (((((2 * a) - 1) |^ k) * (a - 1)) * a) <= Px (
a,
((k + 1) + 1))
by A7, XREAL_1:7;
2
* 1
<= 2
* a
by XREAL_1:64, NAT_1:14;
then
1
- (- 1) <= 2
* a
;
then
((2 * (a ^2)) - a) + (1 - (2 * a)) <= ((2 * (a ^2)) - a) + (- 1)
by XREAL_1:6, XREAL_1:12;
then
(((2 * a) - 1) |^ k) * (((2 * a) - 1) * (a - 1)) <= (((2 * a) - 1) |^ k) * (((a ^2) - 1) + ((a - 1) * a))
by XREAL_1:64;
hence
S1[
k + 1]
by A8, A7, A6, XREAL_1:7, A9, A10, A11, A1, A13, A12, XXREAL_0:2, A14;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A5);
hence
( (((2 * a) - 1) |^ n) * (a - 1) <= Px (a,(n + 1)) & Px (a,(n + 1)) <= a * ((2 * a) |^ n) & ((2 * a) - 1) |^ n <= Py (a,(n + 1)) & Py (a,(n + 1)) <= (2 * a) |^ n )
; verum