let x, y be Integer; :: thesis: for D being Nat holds
( (x ^2) - (D * (y ^2)) = 1 iff [x,y] is Pell's_solution of D )
let D be Nat; :: thesis: ( (x ^2) - (D * (y ^2)) = 1 iff [x,y] is Pell's_solution of D )
A1: ( [x,y] `1 = x & [x,y] `2 = y ) ;
( x in INT & y in INT ) by INT_1:def 2;
then [x,y] in [:INT,INT:] by ZFMISC_1:87;
hence ( (x ^2) - (D * (y ^2)) = 1 implies [x,y] is Pell's_solution of D ) by A1, PELLS_EQ:def 1; :: thesis: ( [x,y] is Pell's_solution of D implies (x ^2) - (D * (y ^2)) = 1 )
assume [x,y] is Pell's_solution of D ; :: thesis: (x ^2) - (D * (y ^2)) = 1
hence (x ^2) - (D * (y ^2)) = 1 by PELLS_EQ:def 1, A1; :: thesis: verum