let n, e be Nat; :: thesis: ( 2 <= e & ex i being Nat st (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 implies (e - 1) + (e |^ (e -' 2)) <= n )
set a = e + 1;
set n1 = n + 1;
set A = ((e + 1) ^2) -' 1;
A1: (e + 1) ^2 = (e + 1) * (e + 1) by SQUARE_1:def 1;
assume A2: 2 <= e ; :: thesis: ( for i being Nat holds not (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 or (e - 1) + (e |^ (e -' 2)) <= n )
then A3: e - 2 = e -' 2 by XREAL_1:233;
(e + 1) * (e + 1) >= 0 + 1 by INT_1:7;
then A4: ((e + 1) ^2) -' 1 = ((e + 1) * (e + 1)) - 1 by XREAL_1:233, A1
.= ((e + 1) - 1) * ((e + 1) + 1) ;
reconsider e2 = e - 2 as Nat by A2, NAT_1:21;
given i being Nat such that A5: (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 ; :: thesis: (e - 1) + (e |^ (e -' 2)) <= n
( (e * (n + 1)) ^2 = (e * (n + 1)) * (e * (n + 1)) & e ^2 = e * e & (n + 1) ^2 = (n + 1) * (n + 1) ) by SQUARE_1:def 1;
then A6: (i ^2) - ((((e + 1) ^2) -' 1) * ((e * (n + 1)) ^2)) = 1 by A5, A4;
[i,(e * (n + 1))] is Pell's_solution of ((e + 1) ^2) -' 1 by A6, Lm1;
then consider j being Nat such that
A7: ( i = Px ((e + 1),j) & e * (n + 1) = Py ((e + 1),j) ) by A2, HILB10_1:4;
A8: j <> 0 by A7, A2, HILB10_1:3;
A9: Py ((e + 1),j),j are_congruent_mod (e + 1) - 1 by A2, HILB10_1:24;
0 * (n + 1),e * (n + 1) are_congruent_mod e by INT_4:11, INT_1:12;
then e divides 0 - j by INT_1:def 4, A9, A7, INT_1:15;
then e divides - (- j) by INT_2:10;
then e <= j by A8, INT_2:27;
then ( e < j or e = j ) by XXREAL_0:1;
then A10: ( Py ((e + 1),e) < Py ((e + 1),j) or Py ((e + 1),e) = Py ((e + 1),j) ) by HILB10_1:11, A2;
A11: ((2 * (e + 1)) - 1) |^ (e2 + 1) <= Py ((e + 1),((e2 + 1) + 1)) by HILB10_1:17;
(((e + 1) - 2) * e) + (e |^ (e2 + 1)) < ((2 * (e + 1)) - 1) |^ (e2 + 1)

proof

per cases ( e = 2 or e > 2 ) by A2, XXREAL_0:1;

suppose e = 2 ; :: thesis: (((e + 1) - 2) * e) + (e |^ (e2 + 1)) < ((2 * (e + 1)) - 1) |^ (e2 + 1)

hence (((e + 1) - 2) * e) + (e |^ (e2 + 1)) < ((2 * (e + 1)) - 1) |^ (e2 + 1) ; :: thesis: verum

end;

suppose e > 2 ; :: thesis: (((e + 1) - 2) * e) + (e |^ (e2 + 1)) < ((2 * (e + 1)) - 1) |^ (e2 + 1)

then A12: (e2 + 1) + 1 > 1 + 1 ;
then A13: e2 + 1 >= 1 + 1 by NAT_1:13;
e2 + 1 > 1 by A12, XREAL_1:7;
then A14: not e2 + 1 is trivial by NEWTON03:def 1;
A15: (2 * (e + 1)) - 1 = (e + 1) + e ;
e + 1 >= 0 + 1 by NAT_1:13;
then A16: ( (e + 1) |^ (e2 + 1) >= (e + 1) |^ 2 & (e + 1) |^ 2 = (e + 1) * (e + 1) ) by A13, PREPOWER:93, NEWTON:81;
A17: (e + 1) - 2 = e2 + 1 ;
( (e + 1) - 0 >= (e + 1) - 1 & (e + 1) - 0 >= (e + 1) - 2 ) by XREAL_1:13;
then (e + 1) * (e + 1) >= ((e + 1) - 1) * ((e + 1) - 2) by A17, XREAL_1:66;
then (e + 1) |^ (e2 + 1) >= ((e + 1) - 1) * ((e + 1) - 2) by A16, XXREAL_0:2;
then ((e + 1) |^ (e2 + 1)) + (e |^ (e2 + 1)) >= (((e + 1) - 1) * ((e + 1) - 2)) + (e |^ (e2 + 1)) by XREAL_1:7;
hence (((e + 1) - 2) * e) + (e |^ (e2 + 1)) < ((2 * (e + 1)) - 1) |^ (e2 + 1) by A15, A14, A2, NEWTON03:103, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then (((e + 1) - 2) * e) + (e |^ (e2 + 1)) < Py ((e + 1),((e2 + 1) + 1)) by A11, XXREAL_0:2;
then A18: (((e + 1) - 2) * e) + (e |^ (e2 + 1)) < e * (n + 1) by A7, A10, XXREAL_0:2;
e |^ (e2 + 1) = e * (e |^ e2) by NEWTON:6;
then (((e + 1) - 2) * e) + (e |^ (e2 + 1)) = e * (((e + 1) - 2) + (e |^ e2)) ;
then ((e + 1) - 2) + (e |^ e2) < n + 1 by A18, XREAL_1:64;
hence (e - 1) + (e |^ (e -' 2)) <= n by A3, INT_1:7; :: thesis: verum