let D be Nat; :: thesis: for p being Pell's_solution of D st not D is square holds
( p is positive iff (p `1) + ((p `2) * (sqrt D)) > 1 )
let p be Pell's_solution of D; :: thesis: ( not D is square implies ( p is positive iff (p `1) + ((p `2) * (sqrt D)) > 1 ) )
assume A1: not D is square ; :: thesis: ( p is positive iff (p `1) + ((p `2) * (sqrt D)) > 1 )
thus ( p is positive implies (p `1) + ((p `2) * (sqrt D)) > 1 ) :: thesis: ( (p `1) + ((p `2) * (sqrt D)) > 1 implies p is positive )
proof
assume A2: p is positive ; :: thesis: (p `1) + ((p `2) * (sqrt D)) > 1
A3: 1 ^2 = 1 ;
A4: sqrt D > 1 by A1, SQUARE_1:27, NAT_1:25, SQUARE_1:18, A3;
p `2 >= 0 + 1 by A2, INT_1:7;
then A5: (p `2) * (sqrt D) >= 1 * (sqrt D) by A4, XREAL_1:64;
(p `2) * (sqrt D) > 1 by XXREAL_0:2, A5, A4;
then ((p `2) * (sqrt D)) + (p `1) > 1 + 0 by XREAL_1:8, A2;
hence (p `1) + ((p `2) * (sqrt D)) > 1 ; :: thesis: verum
end;
assume A6: (p `1) + ((p `2) * (sqrt D)) > 1 ; :: thesis: p is positive
A7: sqrt D > 0 by A1, SQUARE_1:25;
((p `1) ^2) - (D * ((p `2) ^2)) = ((p `1) ^2) - (((sqrt D) ^2) * ((p `2) ^2)) by SQUARE_1:def 2;
then A8: ((p `1) + ((p `2) * (sqrt D))) * ((p `1) - ((p `2) * (sqrt D))) = 1 * 1 by Def1;
then A9: ( (p `1) - ((p `2) * (sqrt D)) > 0 & (p `1) - ((p `2) * (sqrt D)) < 1 ) by A6, XREAL_1:98;
((p `1) - ((p `2) * (sqrt D))) + ((p `2) * (sqrt D)) < 1 + ((p `2) * (sqrt D)) by A9, XREAL_1:8;
then (p `1) - (p `1) < (1 + ((p `2) * (sqrt D))) - (p `1) by XREAL_1:14;
then 0 - 1 < ((1 + ((p `2) * (sqrt D))) - (p `1)) - 1 by XREAL_1:14;
then (((p `2) * (sqrt D)) - (p `1)) + ((p `1) + ((p `2) * (sqrt D))) > (- 1) + 1 by A6, XREAL_1:8;
then ((2 * (p `2)) * (sqrt D)) / 2 > 0 / 2 ;
hence p is positive by A7, A6, A8; :: thesis: verum