let n, k be Nat; for a being non trivial Nat st k < n holds
Px (a,k) < Px (a,n)
let a be non trivial Nat; ( k < n implies Px (a,k) < Px (a,n) )
assume A1:
k < n
; Px (a,k) < Px (a,n)
then reconsider nk = n - k as Nat by NAT_1:21;
A2:
nk <> 0
by A1;
defpred S1[ Nat] means ( $1 > 0 implies Px (a,k) < Px (a,(k + $1)) );
A3:
S1[ 0 ]
;
A4:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A5:
S1[
i]
;
S1[i + 1]
A6:
Px (
a,
((k + i) + 1))
= ((Px (a,(k + i))) * a) + ((Py (a,(k + i))) * ((a ^2) -' 1))
by HILB10_1:6;
Px (
a,
(k + i))
>= Px (
a,
0)
by HILB10_1:10;
then
Px (
a,
(k + i))
>= 1
by HILB10_1:3;
then A7:
(Px (a,(k + i))) + (Px (a,(k + i))) >= (Px (a,(k + i))) + 1
by XREAL_1:7;
(Px (a,(k + i))) * a >= (Px (a,(k + i))) * 2
by NAT_2:29, XREAL_1:64;
then
Px (
a,
((k + i) + 1))
>= ((Px (a,(k + i))) * 2) + 0
by A6, XREAL_1:7;
then A8:
Px (
a,
((k + i) + 1))
>= (Px (a,(k + i))) + 1
by A7, XXREAL_0:2;
then A9:
Px (
a,
((k + i) + 1))
> Px (
a,
(k + i))
by NAT_1:13;
end;
for n1 being Nat holds S1[n1]
from NAT_1:sch 2(A3, A4);
then
Px (a,k) < Px (a,(k + nk))
by A2;
hence
Px (a,k) < Px (a,n)
; verum