let n, k be Nat; :: thesis: for a being non trivial Nat st a = 2 & k <= n holds
(sqrt 3) * (Py (a,k)) < Px (a,n)
let a be non trivial Nat; :: thesis: ( a = 2 & k <= n implies (sqrt 3) * (Py (a,k)) < Px (a,n) )
set A = (a ^2) -' 1;
set S = sqrt ((a ^2) -' 1);
A1: (a ^2) -' 1 = (a ^2) - 1 by NAT_1:14, XREAL_1:233;
assume A2: ( a = 2 & k <= n ) ; :: thesis: (sqrt 3) * (Py (a,k)) < Px (a,n)
((Px (a,k)) ^2) - (((a ^2) -' 1) * ((Py (a,k)) ^2)) = 1 by Th10;
then (((a ^2) -' 1) * ((Py (a,k)) ^2)) + 1 = (Px (a,k)) ^2 ;
then A3: 3 * ((Py (a,k)) ^2) < (Px (a,k)) ^2 by A1, A2, NAT_1:13;
3 * ((Py (a,k)) ^2) = ((sqrt 3) ^2) * ((Py (a,k)) ^2) by SQUARE_1:def 2
.= ((sqrt 3) * (Py (a,k))) ^2 ;
then A4: (sqrt 3) * (Py (a,k)) < Px (a,k) by A3, SQUARE_1:15;
Px (a,k) <= Px (a,n) by A2, Th13;
hence (sqrt 3) * (Py (a,k)) < Px (a,n) by A4, XXREAL_0:2; :: thesis: verum