let D be non square Nat; :: thesis: for p being Element of [:INT,INT:] holds
( p is positive Pell's_solution of D iff ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n )
let p be Element of [:INT,INT:]; :: thesis: ( p is positive Pell's_solution of D iff ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n )
set m = min_Pell's_solution_of D;
set t = (min_Pell's_solution_of D) `1 ;
set u = (min_Pell's_solution_of D) `2 ;
set S = sqrt D;
set x = p `1 ;
set y = p `2 ;
A1: (sqrt D) ^2 = D by SQUARE_1:def 2;
thus ( p is positive Pell's_solution of D implies ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n ) :: thesis: ( ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n implies p is positive Pell's_solution of D )

proof

assume A2: p is positive Pell's_solution of D ; :: thesis: ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n
assume A3: for n being positive Nat holds (p `1) + ((p `2) * (sqrt D)) <> (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n ; :: thesis: contradiction
ex n being Nat st
( (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n < (p `1) + ((p `2) * (sqrt D)) & (p `1) + ((p `2) * (sqrt D)) < (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (n + 1) & n > 0 )

proof

set L = [\((log (10,((p `1) + ((p `2) * (sqrt D))))) / (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))))/];
A4: ( (p `1) + ((p `2) * (sqrt D)) > 1 & ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) > 1 ) by A2, Th18;
(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ 1 = ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) ;
then A6: ( (p `1) + ((p `2) * (sqrt D)) > ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) or ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) > (p `1) + ((p `2) * (sqrt D)) ) by XXREAL_0:1, A3;
( p `1 >= (min_Pell's_solution_of D) `1 & p `2 >= (min_Pell's_solution_of D) `2 ) by A2, Def3;
then A7: ( log (10,1) < log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)))) & log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)))) < log (10,((p `1) + ((p `2) * (sqrt D)))) & log (10,1) = 0 ) by A2, A4, A6, Th19, POWER:51, POWER:57;
then 1 < (log (10,((p `1) + ((p `2) * (sqrt D))))) / (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))) by XREAL_1:187;
then A8: 1 - 1 < ((log (10,((p `1) + ((p `2) * (sqrt D))))) / (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)))))) - 1 by XREAL_1:9;
((log (10,((p `1) + ((p `2) * (sqrt D))))) / (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)))))) - 1 < [\((log (10,((p `1) + ((p `2) * (sqrt D))))) / (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))))/] by INT_1:def 6;
then reconsider L = [\((log (10,((p `1) + ((p `2) * (sqrt D))))) / (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))))/] as Element of NAT by INT_1:3, A8;
take L ; :: thesis: ( (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ L < (p `1) + ((p `2) * (sqrt D)) & (p `1) + ((p `2) * (sqrt D)) < (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1) & L > 0 )
(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ L = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) to_power L by POWER:41;
then A10: log (10,((((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ L)) = L * (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))) by A4, POWER:55;
A11: 0 < L by A8, INT_1:def 6;
L * (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))) <= log (10,((p `1) + ((p `2) * (sqrt D)))) by XREAL_1:83, A7, INT_1:def 6;
then (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ L <= (p `1) + ((p `2) * (sqrt D)) by A4, A10, POWER:57;
hence (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ L < (p `1) + ((p `2) * (sqrt D)) by A11, A3, XXREAL_0:1; :: thesis: ( (p `1) + ((p `2) * (sqrt D)) < (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1) & L > 0 )
(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) to_power (L + 1) by POWER:41;
then log (10,((((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1))) = (L + 1) * (log (10,(((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))))) by A4, POWER:55;
then log (10,((((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1))) > log (10,((p `1) + ((p `2) * (sqrt D)))) by INT_1:29, XREAL_1:77, A7;
then (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1) >= (p `1) + ((p `2) * (sqrt D)) by A4, POWER:57;
hence ( (p `1) + ((p `2) * (sqrt D)) < (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (L + 1) & L > 0 ) by A3, XXREAL_0:1, INT_1:def 6, A8; :: thesis: verum

end;

then consider n being Nat such that
A12: ( (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n < (p `1) + ((p `2) * (sqrt D)) & (p `1) + ((p `2) * (sqrt D)) < (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (n + 1) ) and
A13: n > 0 ;
consider tn, un being Nat such that
A14: (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n = tn + (un * (sqrt D)) by Th4;
reconsider TU = [tn,un] as positive Pell's_solution of D by A14, A13, Th20;
A15: ( TU `1 = tn & TU `2 = un ) ;
A16: (tn ^2) - ((un ^2) * D) = 1 by A15, Lm4;
then A17: (tn + (un * (sqrt D))) * (tn - (un * (sqrt D))) = 1 by A1;
tn + (un * (sqrt D)) > 1 by A15, Th18;
then tn - (un * (sqrt D)) > 0 by A17;
then A18: ( ((((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n) * (tn - (un * (sqrt D))) < ((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) & ((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) < ((((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (n + 1)) * (tn - (un * (sqrt D))) ) by A12, XREAL_1:68;
A19: ( 1 < ((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) & ((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) < ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) )

proof

((((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ (n + 1)) * (tn - (un * (sqrt D))) = ((tn + (un * (sqrt D))) * (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)))) * (tn - (un * (sqrt D))) by A14, NEWTON:6
.= ((tn + (un * (sqrt D))) * (tn - (un * (sqrt D)))) * (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)))
.= ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) by A1, A16 ;
hence ( 1 < ((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) & ((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) < ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) ) by A18, A16, A1, A14; :: thesis: verum

end;

set a = ((p `1) * tn) - (((p `2) * un) * D);
set b = ((p `2) * tn) - ((p `1) * un);
((((p `1) * tn) - (((p `2) * un) * D)) ^2) - (D * ((((p `2) * tn) - ((p `1) * un)) ^2)) = ((((p `1) ^2) - (((p `2) ^2) * D)) * (tn - (un * (sqrt D)))) * (tn + (un * (sqrt D))) by A1
.= (1 * (tn - (un * (sqrt D)))) * (tn + (un * (sqrt D))) by A2, Def1
.= 1 by A1, A16 ;
then reconsider ab = [(((p `1) * tn) - (((p `2) * un) * D)),(((p `2) * tn) - ((p `1) * un))] as Pell's_solution of D by Lm4;
((p `1) + ((p `2) * (sqrt D))) * (tn - (un * (sqrt D))) = (ab `1) + ((ab `2) * (sqrt D)) by A1;
then A20: ab is positive by A19, Th18;
( 1 < (ab `1) + ((ab `2) * (sqrt D)) & (ab `1) + ((ab `2) * (sqrt D)) < ((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D)) ) by A19, A1;
then ( ab `1 < (min_Pell's_solution_of D) `1 & ab `2 < (min_Pell's_solution_of D) `2 ) by Th19;
hence contradiction by A20, Def3; :: thesis: verum

end;

assume ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n ; :: thesis: p is positive Pell's_solution of D
then [(p `1),(p `2)] is positive Pell's_solution of D by Th20;
hence p is positive Pell's_solution of D ; :: thesis: verum