let n, p be Nat; :: thesis: for a being non trivial Nat st 0 < p |^ n & p |^ n < a holds
(p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)
let a be non trivial Nat; :: thesis: ( 0 < p |^ n & p |^ n < a implies (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n) )
assume A1: ( 0 < p |^ n & p |^ n < a ) ; :: thesis: (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)
A2: ( Px (a,0) = 1 & Py (a,0) = 0 & p |^ 0 = 1 ) by HILB10_1:3, NEWTON:4;
A3: ( Py (a,(0 + 1)) = 1 + (0 * a) & Px (a,(0 + 1)) = (1 * a) + (0 * ((a ^2) -' 1)) ) by A2, HILB10_1:6;
A4: Py (a,(1 + 1)) = (Px (a,1)) + ((Py (a,1)) * a) by HILB10_1:6;
A5: ( a * a >= 0 + 1 & a * a = a ^2 ) by INT_1:7, SQUARE_1:def 1;
((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1 by HILB10_1:7;
then A6: (Px (a,n)) ^2 = (((a ^2) -' 1) * ((Py (a,n)) ^2)) + 1 ;
A7: ( ((a - 1) * (Py (a,n))) ^2 = ((a - 1) * (Py (a,n))) * ((a - 1) * (Py (a,n))) & (Py (a,n)) ^2 = (Py (a,n)) * (Py (a,n)) ) by SQUARE_1:def 1;
- ((2 * a) - 1) <= - 1 by XREAL_1:24, NAT_1:14;
then A8: ( (a ^2) + (- ((2 * a) - 1)) <= (a ^2) + (- 1) & (a - 1) ^2 = (a - 1) * (a - 1) ) by XREAL_1:6, SQUARE_1:def 1;
then ((a - 1) ^2) * ((Py (a,n)) ^2) <= ((a ^2) - 1) * ((Py (a,n)) ^2) by A5, XREAL_1:64;
then ((a - 1) * (Py (a,n))) ^2 <= ((a ^2) -' 1) * ((Py (a,n)) ^2) by A8, A7, XREAL_1:233, A5;
then ((a - 1) * (Py (a,n))) ^2 < (Px (a,n)) ^2 by A6, NAT_1:13;
then A9: (a - 1) * (Py (a,n)) < Px (a,n) by SQUARE_1:15;

per cases ( n = 0 or n = 1 or p = 1 or ( n >= 1 + 1 & p <> 1 ) ) by NAT_1:23;

suppose ( n = 0 or n = 1 ) ; :: thesis: (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)

hence (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n) by A2, A3; :: thesis: verum

end;

suppose p = 1 ; :: thesis: (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)

hence (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n) by A9, INT_1:7; :: thesis: verum

end;

suppose A10: ( n >= 1 + 1 & p <> 1 ) ; :: thesis: (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)

then n >= 1 by NAT_1:13;
then p <> 0 by A1, NEWTON:11;
then A11: (Py (a,n)) * p >= (Py (a,n)) * 2 by XREAL_1:64, A10, NAT_1:23;
( n > 2 or n = 2 ) by A10, XXREAL_0:1;
then ( Py (a,n) > Py (a,2) or Py (a,n) = Py (a,2) ) by HILB10_1:11;
then (Py (a,n)) + (Py (a,n)) >= (Py (a,n)) + (a + a) by A3, A4, XREAL_1:6;
then A12: (Py (a,n)) * p >= (Py (a,n)) + (a + a) by A11, XXREAL_0:2;
((Py (a,n)) + a) + a >= ((Py (a,n)) + a) + 1 by NAT_1:14, XREAL_1:6;
then (Py (a,n)) * p >= ((Py (a,n)) + a) + 1 by A12, XXREAL_0:2;
then (Py (a,n)) * p > (Py (a,n)) + a by NAT_1:13;
then - (((Py (a,n)) * p) - a) < - (Py (a,n)) by XREAL_1:20, XREAL_1:24;
then ((Py (a,n)) * a) + (- (((Py (a,n)) * p) - a)) < ((Py (a,n)) * a) + (- (Py (a,n))) by XREAL_1:8;
then A13: ((Py (a,n)) * (a - p)) + a < Px (a,n) by A9, XXREAL_0:2;
((Py (a,n)) * (a - p)) + a > ((Py (a,n)) * (a - p)) + (p |^ n) by A1, XREAL_1:8;
hence (p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n) by A13, XXREAL_0:2; :: thesis: verum

end;

end;