let i, n be Nat; for a being non trivial Nat st i < n & ( not a = 2 or not n = 1 ) holds
Px (a,i) < (Px (a,n)) / 2
let a be non trivial Nat; ( i < n & ( not a = 2 or not n = 1 ) implies Px (a,i) < (Px (a,n)) / 2 )
assume A1:
( i < n & ( not a = 2 or not n = 1 ) )
; Px (a,i) < (Px (a,n)) / 2
then reconsider n1 = n - 1 as Nat ;
n = n1 + 1
;
then A2:
Px (a,n) = ((Px (a,n1)) * a) + ((Py (a,n1)) * ((a ^2) -' 1))
by HILB10_1:6;
then A3:
Px (a,n) >= ((Px (a,n1)) * a) + 0
by XREAL_1:7;
i < n1 + 1
by A1;
then
i <= n1
by NAT_1:13;
then
Px (a,i) <= Px (a,n1)
by HILB10_1:10;
then A4:
(Px (a,i)) * a <= (Px (a,n1)) * a
by XREAL_1:64;
a > 1
by NEWTON03:def 1;
then A5:
a >= 1 + 1
by NAT_1:13;
per cases
( a = 2 or a > 2 )
by A5, XXREAL_0:1;
suppose A6:
a = 2
;
Px (a,i) < (Px (a,n)) / 2then
(
n > 1 or
n < 1 )
by A1, XXREAL_0:1;
then
n - 1
> 1
- 1
by XREAL_1:9, A1, NAT_1:14;
then
Px (
a,
n)
> ((Px (a,n1)) * a) + 0
by A2, XREAL_1:8;
then
Px (
a,
n)
> (Px (a,i)) * 2
by A6, A4, XXREAL_0:2;
hence
Px (
a,
i)
< (Px (a,n)) / 2
by XREAL_1:81;
verum end; suppose
a > 2
;
Px (a,i) < (Px (a,n)) / 2then A7:
(Px (a,i)) * a > (Px (a,i)) * 2
by XREAL_1:68;
(Px (a,i)) * a <= Px (
a,
n)
by A4, A3, XXREAL_0:2;
then
Px (
a,
n)
> (Px (a,i)) * 2
by A7, XXREAL_0:2;
hence
Px (
a,
i)
< (Px (a,n)) / 2
by XREAL_1:81;
verum end;