let e, t be Nat; :: thesis: ( 2 <= e & 0 < t implies ex n, i being Nat st
( t divides n + 1 & (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 ) )
set a = e + 1;
set A = ((e + 1) ^2) -' 1;
A1: (e + 1) ^2 = (e + 1) * (e + 1) by SQUARE_1:def 1;
assume A2: ( 2 <= e & 0 < t ) ; :: thesis: ex n, i being Nat st
( t divides n + 1 & (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 )
(e + 1) * (e + 1) >= 0 + 1 by INT_1:7;
then A3: ((e + 1) ^2) -' 1 = ((e + 1) * (e + 1)) - 1 by A1, XREAL_1:233
.= ((e + 1) - 1) * ((e + 1) + 1) ;
reconsider e2 = e - 2 as Nat by A2, NAT_1:21;
A4: ( ((e + 1) - 1) ^2 = ((e + 1) - 1) * ((e + 1) - 1) & t ^2 = t * t ) by SQUARE_1:def 1;
then reconsider D = ((((e + 1) ^2) -' 1) * (((e + 1) - 1) ^2)) * (t ^2) as non square Nat by A2;
consider x, y being Nat such that
A5: ( (x ^2) - (D * (y ^2)) = 1 & y <> 0 ) by PELLS_EQ:14;
A6: (D * (y ^2)) + 1 = x ^2 by A5;
reconsider n = (t * y) - 1 as Nat by A2, A5;
take n ; :: thesis: ex i being Nat st
( t divides n + 1 & (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 )
take x ; :: thesis: ( t divides n + 1 & (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = x ^2 )
( y ^2 = y * y & e ^2 = e * e & (n + 1) ^2 = (n + 1) * (n + 1) ) by SQUARE_1:def 1;
hence ( t divides n + 1 & (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = x ^2 ) by A6, A3, INT_1:def 3, A4; :: thesis: verum