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

( (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