let n, k be Nat; for a being non trivial Nat st k < n holds
Py (a,k) < Py (a,n)
let a be non trivial Nat; ( k < n implies Py (a,k) < Py (a,n) )
assume A1:
k < n
; Py (a,k) < Py (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 Py (a,k) < Py (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:
Py (
a,
((k + i) + 1))
= ((Py (a,(k + i))) * a) + (Px (a,(k + i)))
by Th9;
a >= 2
by NAT_2:29;
then
a >= 1
by XXREAL_0:2;
then
(Py (a,(k + i))) * a >= (Py (a,(k + i))) * 1
by XREAL_1:64;
then A7:
Py (
a,
((k + i) + 1))
> ((Py (a,(k + i))) * 1) + 0
by A6, XREAL_1:8;
(
i = 0 or
i > 0 )
;
hence
S1[
i + 1]
by A7, A5, XXREAL_0:2;
verum
end;
for n1 being Nat holds S1[n1]
from NAT_1:sch 2(A3, A4);
then
S1[nk]
;
hence
Py (a,k) < Py (a,n)
by A2; verum