let D be non square Nat; { ab where ab is positive Pell's_solution of D : verum } is infinite
set P = { ab where ab is positive Pell's_solution of D : verum } ;
assume A1:
{ ab where ab is positive Pell's_solution of D : verum } is finite
; contradiction
set ab = the positive Pell's_solution of D;
A2:
( the positive Pell's_solution of D = [( the positive Pell's_solution of D `1),( the positive Pell's_solution of D `2)] & the positive Pell's_solution of D in { ab where ab is positive Pell's_solution of D : verum } )
;
proj2 { ab where ab is positive Pell's_solution of D : verum } c= NAT
then reconsider P2 = proj2 { ab where ab is positive Pell's_solution of D : verum } as non empty finite Subset of NAT by A1, WAYBEL26:39, A2, XTUPLE_0:def 13;
set b = max P2;
max P2 in P2
by XXREAL_2:def 8;
then consider a being object such that
A5:
[a,(max P2)] in { ab where ab is positive Pell's_solution of D : verum }
by XTUPLE_0:def 13;
consider ab being positive Pell's_solution of D such that
A6:
[a,(max P2)] = ab
by A5;
A7:
( a = ab `1 & max P2 = ab `2 )
by A6;
then reconsider a = a, b = max P2 as Nat ;
set A = (2 * (a ^2)) - 1;
set B = (2 * a) * b;
(a ^2) - ((b ^2) * D) = 1
by Lm4, A6;
then
a ^2 = 1 + ((b ^2) * D)
;
then 1 =
((((4 * (a ^2)) * (a ^2)) - (4 * (a ^2))) + 1) - (((4 * (a ^2)) * (b ^2)) * D)
.=
(((2 * (a ^2)) - 1) ^2) - ((((2 * a) * b) ^2) * D)
;
then reconsider AB = [((2 * (a ^2)) - 1),((2 * a) * b)] as Pell's_solution of D by Lm4;
a ^2 >= 1
by A7, NAT_1:14;
then
(a ^2) + (a ^2) >= 1 + 1
by XREAL_1:7;
then
(2 * (a ^2)) - 1 >= (1 + 1) - 1
by XREAL_1:9;
then
( AB `1 > 0 & AB `2 > 0 )
by A7;
then
AB is positive Pell's_solution of D
by Def2;
then
AB in { ab where ab is positive Pell's_solution of D : verum }
;
then A8:
(2 * a) * b in P2
by XTUPLE_0:def 13;
a >= 1
by A7, NAT_1:14;
then
a + a > 1 + 0
by XREAL_1:8;
then
(2 * a) * b > 1 * b
by A7, XREAL_1:68;
hence
contradiction
by A8, XXREAL_2:def 8; verum