let i, n be Nat; :: thesis: 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; :: thesis: ( 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 ) ) ; :: thesis: 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;

Px (a,i) < (Px (a,n)) / 2

let a be non trivial Nat; :: thesis: ( 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 ) ) ; :: thesis: 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;

end;

suppose A6:
a = 2
; :: thesis: Px (a,i) < (Px (a,n)) / 2

then
( 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; :: thesis: verum

end;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; :: thesis: verum