let x, y be Integer; for D being Nat holds
( (x ^2) - (D * (y ^2)) = 1 iff [x,y] is Pell's_solution of D )
let D be Nat; ( (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; ( [x,y] is Pell's_solution of D implies (x ^2) - (D * (y ^2)) = 1 )
assume
[x,y] is Pell's_solution of D
; (x ^2) - (D * (y ^2)) = 1
hence
(x ^2) - (D * (y ^2)) = 1
by PELLS_EQ:def 1, A1; verum