let n, k be Nat; 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; ( 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 )
; 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; verum