let n, k be Nat; for a being non trivial Nat st a = 2 & k < n holds
(3 + (2 * (sqrt 3))) * (Py (a,k)) < Px (a,n)
let a be non trivial Nat; ( a = 2 & k < n implies (3 + (2 * (sqrt 3))) * (Py (a,k)) < Px (a,n) )
A1:
( (sqrt 3) ^2 = 3 & sqrt 3 >= 0 )
by SQUARE_1:def 2;
set A = (a ^2) -' 1;
set S = sqrt ((a ^2) -' 1);
assume A2:
( a = 2 & k < n )
; (3 + (2 * (sqrt 3))) * (Py (a,k)) < Px (a,n)
then A3:
k + 1 <= n
by NAT_1:13;
Py (a,(k + 1)) = (Px (a,k)) + ((Py (a,k)) * a)
by Th9;
then A4:
(sqrt 3) * ((Px (a,k)) + ((Py (a,k)) * 2)) < Px (a,n)
by A3, A2, Th18;
(sqrt 3) * (Py (a,k)) <= Px (a,k)
by A2, Th18;
then A5:
((sqrt 3) * (Py (a,k))) * (sqrt 3) <= (Px (a,k)) * (sqrt 3)
by A1, XREAL_1:64;
A6: ((sqrt 3) * (Py (a,k))) * (sqrt 3) =
((sqrt 3) * (sqrt 3)) * (Py (a,k))
.=
3 * (Py (a,k))
by A1
;
(sqrt 3) * ((Px (a,k)) + ((Py (a,k)) * 2)) = ((Py (a,k)) * (2 * (sqrt 3))) + ((Px (a,k)) * (sqrt 3))
;
then
(sqrt 3) * ((Px (a,k)) + ((Py (a,k)) * 2)) >= ((Py (a,k)) * (2 * (sqrt 3))) + (3 * (Py (a,k)))
by A5, A6, XREAL_1:7;
hence
(3 + (2 * (sqrt 3))) * (Py (a,k)) < Px (a,n)
by A4, XXREAL_0:2; verum