let n, k be Nat; :: thesis: for a being non trivial Nat st a <> 2 & k <= n holds
2 * (Py (a,k)) < Px (a,n)
let a be non trivial Nat; :: thesis: ( a <> 2 & k <= n implies 2 * (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: 2 * (Py (a,k)) < Px (a,n)
((Px (a,k)) ^2) - (((a ^2) -' 1) * ((Py (a,k)) ^2)) = 1 by Th10;
then A3: (((a ^2) -' 1) * ((Py (a,k)) ^2)) + 1 = (Px (a,k)) ^2 ;
a >= 2 + 1 by A2, NAT_1:22, NAT_2:29;
then a ^2 >= 3 * 3 by XREAL_1:66;
then (a ^2) -' 1 >= 9 - 1 by A1, XREAL_1:9;
then (a ^2) -' 1 >= 4 by XXREAL_0:2;
then 4 * ((Py (a,k)) ^2) <= ((a ^2) -' 1) * ((Py (a,k)) ^2) by XREAL_1:64;
then (2 * (Py (a,k))) ^2 < (Px (a,k)) ^2 by A3, NAT_1:13;
then A4: 2 * (Py (a,k)) < Px (a,k) by SQUARE_1:15;
Px (a,k) <= Px (a,n) by A2, Th13;
hence 2 * (Py (a,k)) < Px (a,n) by A4, XXREAL_0:2; :: thesis: verum