let a be non trivial Nat; [a,1] = min_Pell's_solution_of ((a ^2) -' 1)
set A = (a ^2) -' 1;
set M = min_Pell's_solution_of ((a ^2) -' 1);
assume A1:
[a,1] <> min_Pell's_solution_of ((a ^2) -' 1)
; contradiction
(a ^2) -' 1 = (a ^2) - 1
by XREAL_1:233, NAT_1:14;
then
(a ^2) - (((a ^2) -' 1) * (1 ^2)) = 1
;
then reconsider a1 = [a,1] as Pell's_solution of (a ^2) -' 1 by Lm3;
( (min_Pell's_solution_of ((a ^2) -' 1)) `1 <> a or (min_Pell's_solution_of ((a ^2) -' 1)) `2 <> 1 )
by A1;
then A2:
((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1))) <> a + (1 * (sqrt ((a ^2) -' 1)))
by PELLS_EQ:3;
A3:
sqrt ((a ^2) -' 1) >= 0
by SQUARE_1:def 2;
a1 is positive
;
then A4:
( (min_Pell's_solution_of ((a ^2) -' 1)) `1 <= a1 `1 & (min_Pell's_solution_of ((a ^2) -' 1)) `2 <= a1 `2 )
by PELLS_EQ:def 3;
then
((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)) <= (a1 `2) * (sqrt ((a ^2) -' 1))
by A3, XREAL_1:64;
then
((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1))) <= (a1 `1) + ((a1 `2) * (sqrt ((a ^2) -' 1)))
by A4, XREAL_1:7;
then A5:
((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1))) < (a1 `1) + ((a1 `2) * (sqrt ((a ^2) -' 1)))
by A2, XXREAL_0:1;
1 < ((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))
by PELLS_EQ:18;
hence
contradiction
by NAT_1:14, A5, PELLS_EQ:19; verum