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

( 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