let D be Nat; for p1, p2 being Pell's_solution of D st 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square holds
( p1 `1 < p2 `1 & p1 `2 < p2 `2 )
let p1, p2 be Pell's_solution of D; ( 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square implies ( p1 `1 < p2 `1 & p1 `2 < p2 `2 ) )
assume A1:
( 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) )
; contradiction
per cases
( p1 `2 >= p2 `2 or p1 `1 >= p2 `1 )
by A1;
suppose A2:
p1 `2 >= p2 `2
;
contradictionA3:
sqrt D > 0
by A1, SQUARE_1:25;
A4:
p1 is
positive
by Th18, A1;
(p2 `1) + ((p2 `2) * (sqrt D)) > 1
by A1, XXREAL_0:2;
then A5:
p2 is
positive
by Th18, A1;
(((p1 `1) ^2) - (((p1 `2) ^2) * D)) + (((p1 `2) ^2) * D) = 1
+ (((p1 `2) ^2) * D)
by Def1;
then A6:
p1 `1 = sqrt (1 + (((p1 `2) ^2) * D))
by SQUARE_1:def 2, A4;
(((p2 `1) ^2) - (((p2 `2) ^2) * D)) + (((p2 `2) ^2) * D) = 1
+ (((p2 `2) ^2) * D)
by Def1;
then A7:
p2 `1 = sqrt (1 + (((p2 `2) ^2) * D))
by SQUARE_1:def 2, A5;
(p1 `2) ^2 >= (p2 `2) ^2
by SQUARE_1:15, A5, A2;
then
((p1 `2) ^2) * D >= ((p2 `2) ^2) * D
by XREAL_1:64;
then
(((p1 `2) ^2) * D) + 1
>= (((p2 `2) ^2) * D) + 1
by XREAL_1:6;
then A8:
p1 `1 >= p2 `1
by A6, A7, SQUARE_1:26;
(p1 `2) * (sqrt D) >= (p2 `2) * (sqrt D)
by A2, XREAL_1:64, A3;
hence
contradiction
by A1, A8, XREAL_1:7;
verum end; suppose A9:
p1 `1 >= p2 `1
;
contradictionA10:
sqrt D > 0
by A1, SQUARE_1:25;
A11:
p1 is
positive
by Th18, A1;
(p2 `1) + ((p2 `2) * (sqrt D)) > 1
by A1, XXREAL_0:2;
then A12:
p2 is
positive
by Th18, A1;
A13:
(((p1 `1) ^2) - (((p1 `2) ^2) * D)) + (((p1 `2) ^2) * D) = 1
+ (((p1 `2) ^2) * D)
by Def1;
A14:
p1 `1 = sqrt (1 + (((p1 `2) ^2) * D))
by A13, SQUARE_1:def 2, A11;
A15:
(((p2 `1) ^2) - (((p2 `2) ^2) * D)) + (((p2 `2) ^2) * D) = 1
+ (((p2 `2) ^2) * D)
by Def1;
A16:
p2 `1 = sqrt (1 + (((p2 `2) ^2) * D))
by A15, SQUARE_1:def 2, A12;
(
sqrt (1 + (((p1 `2) ^2) * D)) >= 0 &
sqrt (1 + (((p2 `2) ^2) * D)) >= 0 )
by SQUARE_1:25;
then A17:
(sqrt (1 + (((p1 `2) ^2) * D))) ^2 >= (sqrt (1 + (((p2 `2) ^2) * D))) ^2
by SQUARE_1:15, A9, A14, A16;
(sqrt (1 + (((p2 `2) ^2) * D))) * (sqrt (1 + (((p2 `2) ^2) * D))) = sqrt ((1 + (((p2 `2) ^2) * D)) * (1 + (((p2 `2) ^2) * D)))
by SQUARE_1:29;
then A18:
sqrt ((1 + (((p1 `2) ^2) * D)) ^2) >= sqrt ((1 + (((p2 `2) ^2) * D)) ^2)
by A17, SQUARE_1:29;
A19:
sqrt ((1 + (((p1 `2) ^2) * D)) ^2) = 1
+ (((p1 `2) ^2) * D)
by SQUARE_1:22;
sqrt ((1 + (((p2 `2) ^2) * D)) ^2) = 1
+ (((p2 `2) ^2) * D)
by SQUARE_1:22;
then
(1 + (((p1 `2) ^2) * D)) - 1
>= (1 + (((p2 `2) ^2) * D)) - 1
by XREAL_1:13, A18, A19;
then A20:
(((p1 `2) ^2) * D) / D >= (((p2 `2) ^2) * D) / D
by XREAL_1:72;
A21:
(((p1 `2) ^2) * D) / D = (p1 `2) ^2
by XCMPLX_1:89, A1;
(((p2 `2) ^2) * D) / D = (p2 `2) ^2
by XCMPLX_1:89, A1;
then A22:
sqrt ((p1 `2) ^2) >= sqrt ((p2 `2) ^2)
by SQUARE_1:26, A20, A21;
sqrt ((p2 `2) ^2) = p2 `2
by SQUARE_1:22, A12;
then A23:
p1 `2 >= p2 `2
by A22, SQUARE_1:22, A11;
(p1 `2) * (sqrt D) >= (p2 `2) * (sqrt D)
by A23, XREAL_1:64, A10;
hence
contradiction
by A1, A9, XREAL_1:7;
verum end;