:: The {M}atiyasevich Theorem -- Preliminaries :: by Karol P\kak :: :: Received November 29, 2017 :: Copyright (c) 2017-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XXREAL_0, SUBSET_1, TARSKI, ARYTM_3, RELAT_1, ARYTM_1, CARD_1, SQUARE_1, REAL_1, PYTHTRIP, FUNCT_1, XBOOLE_0, ZFMISC_1, MCART_1, NAT_1, INT_1, COMPLEX1, FINSEQ_1, NEWTON, PELLS_EQ, HILB10_1, ABSVALUE, ABIAN, INT_2, XCMPLX_0, VALUED_0, FINSEQ_2, ORDINAL4, CARD_3, POWER; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, SQUARE_1, INT_1, FUNCT_1, DOMAIN_1, PYTHTRIP, VALUED_0, FINSEQ_2, RVSUM_1, ABSVALUE, POWER, NEWTON, NAT_D, PELLS_EQ, ABIAN, INT_2, FINSEQ_1; constructors RELSET_1, DOMAIN_1, PEPIN, NEWTON, NAT_D, PELLS_EQ, ABSVALUE, ABIAN, WSIERP_1, POWER; registrations NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, SQUARE_1, RELAT_1, FUNCT_1, XTUPLE_0, NAT_1, MEMBERED, MCART_1, NEWTON03, INT_1, NEWTON, PYTHTRIP, VALUED_0, PELLS_EQ, ABIAN, NEWTON02, ABSVALUE, NAT_6, XBOOLE_0, FINSEQ_1, FINSEQ_2, VALUED_1, CARD_1, RVSUM_1, POWER, NEWTON04; requirements NUMERALS, SUBSET, ARITHM, REAL; definitions TARSKI; equalities SQUARE_1, FINSEQ_1; expansions PELLS_EQ; theorems TARSKI, FUNCT_1, CARD_1, NAT_1, ZFMISC_1, XREAL_1, XXREAL_0, NEWTON, PYTHTRIP, INT_1, FINSEQ_3, FINSEQ_1, SQUARE_1, XCMPLX_1, ABSVALUE, COMPLEX1, XREAL_0, NEWTON02, PEPIN, PELLS_EQ, NAT_2, RVSUM_1, ABIAN, FINSEQ_5, VALUED_0, FINSEQ_2, VALUED_1, POWER, INT_4, EULER_1, INT_2, NAT_D, RVSUM_2, ORDINAL1, WSIERP_1; schemes NAT_1, FINSEQ_1; begin :: Preliminaries reserve i,j,n,n1,n2,m,k,u for Nat, r,r1,r2 for Real, x,y for Integer, a,b for non trivial Nat; Lm1: [\(2*n +1)/ 2 /] = n proof 2*n < 2*n +1 by NAT_1:13; then A1:n < (2*n +1)/ 2 by XREAL_1:81; 2*n -1 < 2*n -0 by XREAL_1:15; then (2*n +1-2)/ 2 by A5,FINSEQ_1:40; hence thesis; end; suppose A7: k >0; F is non empty by A5; then len F in dom F by FINSEQ_5:6; then (F|k) ^ <*F.k1*> = F| k1 by A5,FINSEQ_5:10 .=F by A5; then A8: Sum F = Sum (F|k) + F.k1 by RVSUM_1:74; A9: k <= k1 by NAT_1:11; A10: len (F|k) = k by A5,NAT_1:11,FINSEQ_1:59; for i be Nat st 1 < i <= len (F|k) holds ((F|k).i) mod n = 0 proof let i be Nat such that A11: 1< i <= len (F|k); (F|k).i = F.i & i <= len F by A10,A11,A5,A9,FINSEQ_3:112,XXREAL_0:2; hence thesis by A11,A6; end; then A12: Sum (F|k) mod n = ((F|k).1) mod n by A4,A10; A13: F.1 mod n = Sum (F|k) mod n by A7,NAT_1:14,A12,FINSEQ_3:112; per cases; suppose n=0; then Sum F mod n = 0 = (F.1) mod n by INT_1:def 10; hence thesis; end; suppose A14: n >0; A15: Sum(F|k) is Nat & Sum(F) is Nat by TARSKI:1; 0+1< k1 by A7,XREAL_1:8; then 0= (Sum F - Sum (F|k))mod n by A5,A6,A8; hence thesis by A13, A15,A14,INT_4:22; end; end; end; P[k] from NAT_1:sch 2(A1,A3); hence thesis; end; theorem Th2: for f be complex-valued FinSequence ex e,o be complex-valued FinSequence st len e = [\len f/2/] & len o = [/len f/2 \] & Sum f = Sum e + Sum o & for n holds e.n = f.(2*n) & o.n = f.(2*n-1) proof defpred P[Nat] means for f be complex-valued FinSequence st len f=\$1 ex e,o be complex-valued FinSequence st len e = [\len f/2/] & len o = [/len f/2 \] & Sum f = Sum e + Sum o & for n holds e.n = f.(2*n) & o.n = f.(2*n-1); A1:P[0] proof let f be complex-valued FinSequence such that A2: len f=0; take f,f; thus len f = [\len f/2/] & len f = [/len f/2 \] by A2,INT_1:25,INT_1:30; f=<*>REAL by A2; hence Sum f=Sum f+Sum f by RVSUM_1:72; let n; f={} by A2; then f.n = 0=f.(2*n) & f.n = 0 = f.(2*n-1); hence thesis; end; A3: P[n] implies P[n+1] proof assume A4: P[n];set n1=n+1; let f be complex-valued FinSequence such that A5: len f=n1; set fn=f|n; A6: f = fn^<*f.n1*> by A5,FINSEQ_3:55; n < n1 by NAT_1:13; then len fn = n by A5,FINSEQ_1:59; then consider e,o be complex-valued FinSequence such that A7: len e = [\n/2/] & len o = [/n/2 \] and A8: Sum (fn) = Sum e + Sum o and A9: for k holds e.k = fn.(2*k) & o.k = fn.(2*k-1) by A4; per cases; suppose n is even; then consider k such that A10: 2*k=n by ABIAN:def 2; take e,oF=o^<*f.n1*>; A11: len oF = len o+1 by FINSEQ_2:16; A12: [\n/2/] = k = [\(n+1)/2/] & [/n/2 \] = k & [/(n+1)/2 \] =k+1 by A10,INT_1:25,30,Lm1,Lm2; hence len e = [\len f/2/] & len oF = [/len f/2 \] by FINSEQ_2:16,A5,A7; thus Sum f = Sum fn+f.n1 by A6,RVSUM_2:31 .= Sum e + (Sum o+f.n1) by A8 .= Sum e + Sum oF by RVSUM_2:31; let i be Nat; thus e.i = f.(2*i) proof per cases; suppose 2*i <=n; then fn.(2*i) = f.(2*i) by FINSEQ_3:112; hence thesis by A9; end; suppose 2*i > n; then A13: i > k by A10,XREAL_1:64; then i >= k+1 by NAT_1:13; then 2*i >= 2*(k+1) & 2*(k+1) = len f+1 by A10,A5,XREAL_1:64; then 2*i > len f by NAT_1:13; then not 2*i in dom f & not i in dom e by FINSEQ_3:25,A7,A12,A13; then f.(2*i) = 0 = e.i by FUNCT_1:def 2; hence thesis; end; end; thus oF.i = f.(2*i-1) proof per cases; suppose i=0; then not i in dom oF & not (2*i-1) in dom f by FINSEQ_3:25; then oF.i = 0 = f.(2*i-1) by FUNCT_1:def 2; hence thesis; end; suppose A14: i<>0 & 2*i <=n; then 1<= i <= k by A10,XREAL_1:68,NAT_1:14; then i in dom o by A7,A12,FINSEQ_3:25; then A15: oF.i = o.i by FINSEQ_1:def 7 .= fn.(2*i-1) by A9; 2*i-1 <=n-0 by XREAL_1:13,A14; hence thesis by A15,A14,FINSEQ_3:112; end; suppose 2*i > n; then i > k by A10,XREAL_1:64; then i >= k+1 by NAT_1:13; then 2*i >= 2*(k+1) & 2*(k+1) = len f+1 by A10,A5,XREAL_1:64; then A16: 2*i-1 >= len f by XREAL_1:19; per cases by A16,XXREAL_0:1; suppose 2*i-1 = len f; hence thesis by A5,A10,A7,A12; end; suppose A17: 2*i -1 > len f; then not (2*i-1) in dom f by FINSEQ_3:25; then A18: f.(2*i-1) = 0 by FUNCT_1:def 2; 2*i > len f+1 by A17,XREAL_1:20; then 2*i > 2*(k+1) by A10,A5; then i > k+1 by XREAL_1:64; then not i in dom oF by A11,A12,A7,FINSEQ_3:25; hence thesis by A18,FUNCT_1:def 2; end; end; end; end; suppose n is odd; then consider k such that A19: n =2*k+1 by ABIAN:9; take eF=e^<*f.n1*>,o; A20: len eF = len e+1 by FINSEQ_2:16; A21: [\n/2/] = k & [\(n+1)/2/]=k+1 & [/n/2 \] = k+1 & [/(n+1)/2 \] =k+1 by A19,INT_1:25,30,Lm1,Lm2; hence len eF = [\len f/2/] & len o = [/len f/2 \] by FINSEQ_2:16,A5,A7; thus Sum f = Sum fn+f.n1 by A6,RVSUM_2:31 .= (Sum e + f.n1) + Sum o by A8 .= Sum eF + Sum o by RVSUM_2:31; let i be Nat; thus eF.i = f.(2*i) proof per cases; suppose i=0; hence thesis; end; suppose i <>0 & i <= k; then 1<=i<=k & 2*i <= 2*k by NAT_1:14,XREAL_1:64; then i in dom e & 2*i < n by A19,NAT_1:13,FINSEQ_3:25,A7,A21; then eF.i =e.i & fn.(2*i) = f.(2*i) by FINSEQ_1:def 7,FINSEQ_3:112; hence thesis by A9; end; suppose i > k; then A22: i >= k+1 by NAT_1:13; per cases by A22,XXREAL_0:1; suppose i = k+1; hence thesis by A19,A7,A21; end; suppose A23: i > k+1; then not i in dom eF by FINSEQ_3:25,A7,A20,A21; then A24: eF.i = 0 by FUNCT_1:def 2; 2*i > 2*(k+1) by A23,XREAL_1:68; then not 2*i in dom f by A5,A19,FINSEQ_3:25; hence thesis by A24,FUNCT_1:def 2; end; end; end; thus o.i = f.(2*i-1) proof per cases; suppose i =0; then not i in dom o & not (2*i-1) in dom f by FINSEQ_3:25; then o.i= 0 = f.(2*i-1) by FUNCT_1:def 2; hence thesis; end; suppose A25: i<>0 & 2*i-1 <=n; fn.(2*i-1) = f.(2*i-1) by A25,FINSEQ_3:112; hence thesis by A9; end; suppose 2*i-1 > n; then 2*i > n+1 by XREAL_1:20; then 2*i > 2*(k+1) by A19; then A26: i > k+1 by XREAL_1:64; then not i in dom o by FINSEQ_3:25,A7,A21; then A27: o.i = 0 by FUNCT_1:def 2; i >= k+1+1 by A26,NAT_1:13; then 2*i >= 2*(k+1+1) by XREAL_1:64; then 2*i >= len f+1+1 by A19,A5; then 2*i > len f+1 by NAT_1:13; then not 2*i-1 in dom f by XREAL_1:20,FINSEQ_3:25; hence thesis by A27,FUNCT_1:def 2; end; end; end; end; P[n] from NAT_1:sch 2(A1,A3); hence thesis; end; registration let a; cluster a^2 -' 1 -> non square; coherence proof assume A1: a^2 -' 1 is square; a >=2 by NAT_2:29; then A2: a^2>=2*2 by XREAL_1:66; A3: a^2-'1 = a^2-1 by XREAL_1:233,NAT_1:14; then a^2-'1 is non zero by A2; then a^2-'1+1 is non square by A1; hence thesis by A3; end; end; begin :: Solutions of Pell's Equation - Special Case definition let a,n be Nat; assume A1:a is non trivial; func Px(a,n) -> Nat means :Def1: for b be non trivial Nat st b=a ex y be Nat st it + y*sqrt (b^2-'1) = ( (min_Pell's_solution_of (b^2-'1))`1 + (min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n; existence proof reconsider A=a as non trivial Nat by A1; consider x,y be Nat such that A2: x + y*sqrt (A^2-'1) = ( (min_Pell's_solution_of (A^2-'1))`1 + (min_Pell's_solution_of (A^2-'1))`2 *sqrt ((A^2-'1)) ) |^ n by PELLS_EQ:4; take x; thus thesis by A2; end; uniqueness proof reconsider A=a as non trivial Nat by A1; let p1,p2 be Nat such that A3: for b be non trivial Nat st b=a ex y be Nat st p1 + y*sqrt (b^2-'1) = ( (min_Pell's_solution_of (b^2-'1))`1 + (min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n and A4: for b be non trivial Nat st b=a ex y be Nat st p2 + y*sqrt (b^2-'1) = ( (min_Pell's_solution_of (b^2-'1))`1 + (min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n; set m=min_Pell's_solution_of (A^2-'1); A5: ex y be Nat st p1 + y*sqrt (A^2-'1) = ( m`1 + m`2 *sqrt ((A^2-'1)) ) |^ n by A3; ex y be Nat st p2 + y*sqrt (A^2-'1) =( m`1 + m`2 *sqrt ((A^2-'1)) ) |^ n by A4; hence thesis by A5,PELLS_EQ:3; end; end; definition let a,n be Nat; assume A1:a is non trivial; func Py(a,n) -> Nat means :Def2: for b be non trivial Nat st b=a holds Px(b,n) + it*sqrt (b^2-'1) = ( (min_Pell's_solution_of (b^2-'1))`1 + (min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n; existence proof reconsider A=a as non trivial Nat by A1; consider y be Nat such that A2: Px(A,n) + y*sqrt (A^2-'1) = ( (min_Pell's_solution_of (A^2-'1))`1 + (min_Pell's_solution_of (A^2-'1))`2 *sqrt ((A^2-'1)) ) |^ n by Def1; take y; thus thesis by A2; end; uniqueness proof reconsider A=a as non trivial Nat by A1; let p1,p2 be Nat such that A3: for b be non trivial Nat st b=a holds Px(b,n) + p1*sqrt (b^2-'1) = ( (min_Pell's_solution_of (b^2-'1))`1 + (min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n and A4: for b be non trivial Nat st b=a holds Px(b,n) + p2*sqrt (b^2-'1) = ( (min_Pell's_solution_of (b^2-'1))`1 + (min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n; set m=min_Pell's_solution_of (A^2-'1); Px(A,n) + p1*sqrt (A^2-'1) = ( m`1 + m`2 *sqrt ((A^2-'1)) ) |^ n = Px(A,n) + p2*sqrt (A^2-'1) by A3,A4; hence thesis by PELLS_EQ:3; end; end; theorem Th6: Px(a,0) = 1 & Py(a,0) = 0 proof set A = a^2-'1,M=min_Pell's_solution_of A; Px(a,0) + Py(a,0)*sqrt (a^2-'1) = ( M`1 + M`2 *sqrt A ) |^ 0 by Def2 .= 1+0*sqrt A by NEWTON:4; hence thesis by PELLS_EQ:3; end; Lm3:for x,y be Integer, D be Nat holds x^2 - D*y^2 = 1 iff [x,y] is Pell's_solution of D proof let x,y be Integer, D be Nat; A1:[x,y]`1 = x & [x,y]`2 =y; x in INT & y in INT by INT_1:def 2; then [x,y] in [:INT,INT:] by ZFMISC_1:87; hence x^2 - D*y^2 = 1 implies [x,y] is Pell's_solution of D by A1,PELLS_EQ:def 1; assume [x,y] is Pell's_solution of D; hence thesis by PELLS_EQ:def 1,A1; end; theorem Th7: [n1,n2] is Pell's_solution of (a^2-'1) implies ex n st n1 = Px(a,n) & n2 = Py(a,n) proof set D=a^2-'1; assume A1: [n1,n2] is Pell's_solution of D; then reconsider N=[n1,n2] as Pell's_solution of D; A2: n1^2-(a^2-'1)*n2^2 = 1 by A1,Lm3; per cases; suppose A3: n2=0; then n1 <=1 & n1 >=1 by A2,SQUARE_1:51,NAT_1:14; then n1=1 by XXREAL_0:1; then n1=Px(a,0) & n2=Py(a,0) by A3,Th6; hence thesis; end; suppose n2 >0; then N is positive by A2; then consider n be positive Nat such that A4: n1 + n2 * sqrt D =( (min_Pell's_solution_of D)`1 + (min_Pell's_solution_of D)`2 *sqrt D ) |^ n by PELLS_EQ:21; consider y be Nat such that A5: Px(a,n) + y*sqrt D = ( (min_Pell's_solution_of D)`1 + (min_Pell's_solution_of D)`2 *sqrt (D) ) |^ n by Def1; A6: n1 = Px(a,n) by A5,A4,PELLS_EQ:3; Px(a,n) + Py(a,n)*sqrt D = n1 + n2 * sqrt D by A4,Def2; then n2 = Py(a,n) by PELLS_EQ:3; hence thesis by A6; end; end; theorem Th8: [a,1] = min_Pell's_solution_of (a^2-'1) proof set A=a^2-'1,M=min_Pell's_solution_of A; assume A1: [a,1] <> M; 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 by Lm3; M`1 <> a or M`2 <> 1 by A1; then A2: M`1 + M`2 * sqrt A <> a + 1 *sqrt A by PELLS_EQ:3; A3: sqrt A >=0 by SQUARE_1:def 2; a1 is positive; then A4: M`1 <= a1`1 & M`2 <= a1`2 by PELLS_EQ:def 3; then M`2 * sqrt A <= a1`2 *sqrt A by A3,XREAL_1:64; then M`1 + M`2 * sqrt A <= a1`1 + a1`2 *sqrt A by A4,XREAL_1:7; then A5: M`1 + M`2 * sqrt A < a1`1 + a1`2 *sqrt A by A2,XXREAL_0:1; 1 < M`1 + M`2 * sqrt A by PELLS_EQ:18; hence thesis by NAT_1:14,A5,PELLS_EQ:19; end; theorem Th9: Px(a,n+1) = Px(a,n)*a + Py(a,n)*(a^2-'1) & Py(a,n+1) = Px(a,n) + Py(a,n)*a proof set A=a^2-'1,M=min_Pell's_solution_of A; set n1=n+1; A1:(sqrt A)^2 =A by SQUARE_1:def 2; A2: M = [a,1] by Th8; Px(a,n1) + Py(a,n1) * sqrt A = ( M`1 + M`2 * sqrt A) |^n1 by Def2 .= (M`1 + M`2 * sqrt A) |^n * (M`1 + M`2 * sqrt A) by NEWTON:6 .= (Px(a,n) + Py(a,n) * sqrt A) * (M`1 + M`2 * sqrt A) by Def2 .= (Px(a,n) * a + Py(a,n)* A) + (Px(a,n) + Py(a,n) * a) * sqrt A by A2,A1; hence thesis by PELLS_EQ:3; end; theorem Th10: Px(a,n)^2 - (a^2-'1) *Py(a,n)^2 = 1 proof set m=min_Pell's_solution_of (a^2-'1); per cases; suppose n=0; then Px(a,n) = 1 & Py(a,n) = 0 by Th6; hence thesis; end; suppose A1: n >0; Px(a,n) + Py(a,n)*sqrt (a^2-'1) = (m`1 + m`2 *sqrt ((a^2-'1)) ) |^ n by Def2; then reconsider PP=[Px(a,n),Py(a,n)] as positive Pell's_solution of (a^2-'1) by A1,PELLS_EQ:20; (PP`1)^2 - (a^2-'1)* (PP`2)^2 =1 by PELLS_EQ:def 1; hence thesis; end; end; theorem Th11: Px(a,n) + Py(a,n) * sqrt (a^2-'1) = (a + sqrt (a^2-'1)) |^ n & Px(a,n) + (- Py(a,n)) * sqrt (a^2-'1) = (a - sqrt (a^2-'1)) |^ n proof set A=a^2-'1,M=min_Pell's_solution_of A; set n1=n+1; A1: M = [a,1] by Th8; A2:Px(a,n) + Py(a,n) * sqrt A = ( M`1 + M`2 * sqrt A) |^n by Def2 .= (a+ 1*sqrt A) |^n by A1; then Px(a,n) - Py(a,n) * sqrt A = (a- 1*sqrt A) |^n by PELLS_EQ:6; hence thesis by A2; end; theorem Th12: ex Fy,Fx be FinSequence of NAT st Sum Fy = Py(a,n) & len Fy = [\ (n+1)/2 /] & (for i st 1 <= i <= (n+1)/2 holds Fy.i = (n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a^2-'1) |^ (i-'1))& a|^n + Sum Fx = Px(a,n) & len Fx = [\ n/2 /] & for i st 1 <= i <= n/2 holds Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * (a^2-'1) |^ i proof set A = a^2-'1; defpred P[Nat] means ex Fy,Fx be FinSequence of NAT st Sum Fy = Py(a,\$1) & len Fy = [\ (\$1+1)/2 /] & (for i be Nat st 1 <= i <= (\$1+1)/2 holds Fy.i = (\$1 choose (2*i-'1)) * a |^ (\$1+1-'2*i) * A |^ (i-'1))& a|^\$1 + Sum Fx = Px(a,\$1) & len Fx = [\ \$1/2 /] & for i be Nat st 1 <= i <= \$1/2 holds Fx.i = (\$1 choose (2*i)) * a |^ (\$1-'2*i) * A |^ i; A1:P[0] proof set F = <*>NAT; A2: len F = 0; A3: 0 = [\(0*2+1)/2/] by Lm1; A4: for i be Nat st 1 <= i <= (0+1)/2 holds F.i = (0 choose (2*i-'1)) * a |^ (0+1-'2*i) * A |^ (i-'1) by XXREAL_0:2; A5: Sum F = Py(a,0) by Th6,RVSUM_1:72; a|^0 = 1 by NEWTON:4; then A6: a|^0 + Sum F = Px(a,0) by RVSUM_1:72,Th6; for i be Nat st 1 <= i <= 0/2 holds F.i = (0 choose (2*i)) * a |^ (0-'2*i) * A |^ i; hence thesis by A2,A3,A4,A5,A6; end; A7: for n be Nat st P[n] holds P[n+1] proof let n; set n1=n+1; assume P[n]; then consider Fy,Fx be FinSequence of NAT such that A8: Sum Fy = Py(a,n) & len Fy = [\ n1/2 /] and A9: for i be Nat st 1 <= i <= n1/2 holds Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ (i-'1)and A10: a|^n + Sum Fx = Px(a,n) & len Fx = [\ n/2 /] and A11: for i be Nat st 1 <= i <= n/2 holds Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * A |^ i; set Fxa = <*a|^n*>^Fx; set Fx0=Fx^<*0*>; set Fy0=Fy^<*0*>; A12: Px(a,n1) = (a|^n + Sum Fx)*a + (Sum Fy)*A by Th9,A8,A10 .= (a|^n *a) + (Sum Fx)*a + (Sum Fy)*A .= a|^n1 + (Sum Fx)*a + (Sum Fy)*A by NEWTON:6 .= a|^n1 + Sum (a*Fx) + (Sum Fy)*A by RVSUM_1:87; A13: (Sum Fy)*A = Sum (A*Fy) by RVSUM_1:87; A14: Sum Fy0 = Sum Fy+0 by RVSUM_1:74; A15: Sum Fx0 = Sum Fx+0 by RVSUM_1:74; A16: Sum (a*Fx0) = a * Sum Fx0 by RVSUM_1:87; A17: Py(a,n1) = Px(a,n) + Py(a,n) * a by Th9 .= Sum Fxa + (Sum Fy) *a by A8,A10,RVSUM_1:76; per cases; suppose A18: n is odd; then consider k such that A19: n = 2*k+1 by ABIAN:9; set k1=k+1; A20: [\ n1/2 /] = k1 & [\ n/2 /] = k by A19,INT_1:25,Lm1; then A21: len Fxa =k1 & len (a*Fy) = k1 by A10,FINSEQ_5:8,A8,RVSUM_1:117; rng Fxa c= REAL & rng (a*Fy) c= REAL; then Fxa is FinSequence of REAL & a*Fy is FinSequence of REAL by FINSEQ_1:def 4; then reconsider FxA=Fxa,aFy=a*Fy as Element of k1-tuples_on REAL by A21,FINSEQ_2:92; rng (Fxa + a*Fy) c= NAT by VALUED_0:def 6; then reconsider FY = Fxa + a*Fy as FinSequence of NAT by FINSEQ_1:def 4; A22: len (a*Fx0) = len Fx0 = k1 & len (A*Fy) = k1 by A20,A8,A10,FINSEQ_2:16,RVSUM_1:117; reconsider AFx0=a*Fx0,AFy=A*Fy as Element of k1-tuples_on REAL by A22,FINSEQ_2:92; rng (a*Fx0 + A*Fy) c= NAT by VALUED_0:def 6; then reconsider FX = a*Fx0 + A*Fy as FinSequence of NAT by FINSEQ_1:def 4; take FY,FX; thus Sum FY = Sum (FxA) + Sum aFy by RVSUM_1:89 .= Py(a,n1) by A17,RVSUM_1:87; A23: n1+1 = 2*k1+1 by A19; len (FxA+aFy) = k1 by CARD_1:def 7; hence len FY = [\(n1+1)/2/] by A23,Lm1; thus for i be Nat st 1 <= i <= (n1+1)/2 holds FY.i = (n1 choose (2*i-'1)) * a |^ ((n1+1)-'2*i) * A |^ (i-'1) proof let i be Nat such that A24: 1 <= i <= (n1+1)/2; set i1=i-'1; A25: i1 +1 = i by A24,XREAL_1:235; 2*1 <=2*i by A24,XREAL_1:66; then A26: 2*i-'1 = 2*i-1 by XREAL_1:233,XXREAL_0:2; A27: 2*i <= n1+1 by A24,XREAL_1:83; then A28: 2*i < n1+1 by A18,XXREAL_0:1; then A29: 2*i <= n1 by NAT_1:13; A30: i <= n1/2 by A28,NAT_1:13,XREAL_1:77; A31: n1-'2*i = n1-2*i by A29,XREAL_1:233; A32: n1+1-'2*i = n1+1-2*i by XREAL_1:233,A27; then A33: n1+1-'2*i = 1+ (n1-'2*i) by A31; Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A24,A9,A30; then A34: (a*Fy).i = a*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1) by VALUED_1:6 .= (n choose (2*i-'1)) * (a * a |^ (n1-'2*i)) * A |^ i1 .= (n choose (2*i1+1)) * a |^ (n1+1-'2*i) * A |^ i1 by A26,A25,A33,NEWTON:6; 2*i <= n1+1 by A24,XREAL_1:83; then 2*i1+1+1 <= n1+1 by A25; then 2*i1+1 <= n1 by XREAL_1:8; then A35: 2*i1 < n1 by NAT_1:13; then A36: 2*i1 <=n by NAT_1:13; then A37: n-'2*i1 = n-2*i1 by XREAL_1:233; A38: Fxa.i = (n choose (2*i1)) * a |^ (n-'2*i1) * A |^ i1 proof per cases; suppose A39: i > 1; then A40: i1 >=1 by A25,NAT_1:13; i1 <= n/2 by XREAL_1:77,A35,NAT_1:13; then A41: Fx.i1 = (n choose (2*i1)) * a |^ (n-'2*i1) * A |^ i1 by A11,A39,A25,NAT_1:13; 2*i1< 2*k+1 by A36,A19,XXREAL_0:1; then i1 <= k by XREAL_1:68,NAT_1:13; then i1 in dom Fx by A40,A20,A10,FINSEQ_3:25; hence thesis by A41,A25,FINSEQ_3:103; end; suppose i <=1; then A42: i=1 by A24,XXREAL_0:1; A43: n choose (2*i1) = 1 by A42,A25,NEWTON:19; n-'2*i1 = n-0 by A42,A25,XREAL_1:233; hence thesis by A43,NEWTON:4,A42,A25; end; end; thus FY.i = (FxA.i) + (aFy.i) by RVSUM_1:11 .= ((n choose (2*i1))+(n choose (2*i1+1))) * a |^ (n1+1-'2*i) * A |^ i1 by A38,A34,A37,A32,A25 .= (n1 choose (2*i-'1)) * a |^ (n1+1-'2*i) * A |^ i1 by A26,A25,NEWTON:22; end; Sum FX = Sum AFx0 + Sum AFy by RVSUM_1:89 .= Sum (a*Fx) + Sum (A*Fy) by RVSUM_1:87,A15,A16; hence a|^n1 + Sum FX = Px(a,n1) by A12,A13; len (AFx0 + AFy) = k1 by CARD_1:def 7; hence len FX = [\ n1/2 /] by A19,INT_1:25; thus for i be Nat st 1 <= i <= n1/2 holds FX.i = (n1 choose (2*i)) * a |^ (n1-'2*i) * A |^ i proof let i be Nat such that A44: 1 <= i <= n1/2; set i1=i-'1; i1 +1 = i by A44,XREAL_1:235; then A45: A* A |^ i1 = A |^ i by NEWTON:6; Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A9,A44; then A46: (A*Fy).i = A*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1) by VALUED_1:6 .= (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i by A45; 2*i <= n1 by A44,XREAL_1:83; then A47: n1-'2*i=n1-2*i by XREAL_1:233; A48: (a*Fx0).i = a * (Fx0.i) by VALUED_1:6; A49: (a*Fx0).i = (n choose (2*i)) * a |^ (n1-'2*i) * A |^ i proof per cases; suppose A50: i <= k; then A51: 2*i < n by A19,NAT_1:13,XREAL_1:66; then i <= n / 2 by XREAL_1:77; then A52: Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * A |^ i by A11,A44; A53: i in dom Fx by A44,A50,A10,A20,FINSEQ_3:25; A54: n-'2*i = n- 2*i by A51,XREAL_1:233; n1-'2*i = 1+ (n-'2*i) by A54,A47; then A55: a |^ (n1-'2*i) = a * a |^ (n-'2*i) by NEWTON:6; (a*Fx0).i = a*((n choose (2*i)) * a |^ (n-'2*i) * A |^ i) by A48,A52,A53,FINSEQ_1:def 7 .= (n choose (2*i)) * a |^ (n1-'2*i) * A |^ i by A55; hence thesis; end; suppose i > k; then i >= k1 by NAT_1:13; then A56: 2*i >= 2*k1 by XREAL_1:66; then A57: 2*i >= n1 by A19; 2*i <= n1 by A44,XREAL_1:83; then A58:2*i = 2*k1 by A56,A19,XXREAL_0:1; 2*i> n by A57,NAT_1:13; then n choose (2*i)=0 by NEWTON:def 3; hence thesis by A58,A10,A20,A48; end; end; A59: 2*i-'1+1 =2*i by XREAL_1:235,NAT_1:14,A44; thus FX.i = (AFx0).i + (AFy).i by RVSUM_1:11 .= ((n choose (2*i-'1))+(n choose (2*i)))* a |^ (n1-'2*i) * A |^ i by A46,A49 .= (n1 choose (2*i))* a |^ (n1-'2*i) * A |^ i by A59,NEWTON:22; end; end; suppose n is even; then consider k such that A60: n = 2*k by ABIAN:def 2;set k1=k+1; A61: [\ n1/2 /] = k & [\ n/2 /] = k by A60,INT_1:25,Lm1; then A62: len Fxa =k1 & len Fy0 = k1 & len (a*Fy0) = len Fy0 by FINSEQ_2:16,FINSEQ_5:8,A8,A10,RVSUM_1:117; rng Fxa c= REAL & rng (a*Fy0) c= REAL; then Fxa is FinSequence of REAL & a*Fy0 is FinSequence of REAL by FINSEQ_1:def 4; then reconsider FxA=Fxa,aFy0=a*Fy0 as Element of k1-tuples_on REAL by A62,FINSEQ_2:92; rng (Fxa + a*Fy0) c= NAT by VALUED_0:def 6; then reconsider FY = Fxa + a*Fy0 as FinSequence of NAT by FINSEQ_1:def 4; A63: len (a*Fx) = len Fx = k & len (A*Fy) = k by A61,A8,A10,RVSUM_1:117; reconsider AFx=a*Fx,AFy=A*Fy as Element of k-tuples_on REAL by A63,FINSEQ_2:92; rng (a*Fx + A*Fy) c= NAT by VALUED_0:def 6; then reconsider FX = a*Fx + A*Fy as FinSequence of NAT by FINSEQ_1:def 4; take FY,FX; thus Sum FY = Sum (FxA) + Sum aFy0 by RVSUM_1:89 .= Py(a,n1) by A17,A14,RVSUM_1:87; len (FxA+aFy0) = k1 by CARD_1:def 7; hence len FY = [\(n1+1)/2/] by A60,INT_1:25; thus for i be Nat st 1 <= i <= (n1+1)/2 holds FY.i = (n1 choose (2*i-'1)) * a |^ ((n1+1)-'2*i) * A |^ (i-'1) proof let i be Nat such that A64: 1 <= i <= (n1+1)/2; set i1=i-'1; A65: i1 +1 = i by A64,XREAL_1:235; A66: 2*i <= n1+1 by A64,XREAL_1:83; then A67: 2*i1+2 <= n+2 by A65; then A68: 2*i1 <= n by XREAL_1:8; A69: n-'2*i1 = n-2*i1 & n1+1-'2*i = n1+1-2*i by A67,A66,XREAL_1:8,233; 2*1 <=2*i by A64,XREAL_1:66; then A70: 2*i-'1 = 2*i-1 by XREAL_1:233,XXREAL_0:2; A71: FxA.i = (n choose (2*i1)) * a |^ (n1+1-'2*i) * A |^ i1 proof per cases; suppose A72: i > 1; then A73: i1 >=1 by A65,NAT_1:13; i1 <= n/2 by A68,XREAL_1:77; then A74: Fx.i1 = (n choose (2*i1)) * a |^ (n-'2*i1) * A |^ i1 by A11,A72,A65,NAT_1:13; i1 <= k by A68,A60,XREAL_1:68; then i1 in dom Fx by A73,A61,A10,FINSEQ_3:25; hence thesis by A69,A74,A65,FINSEQ_3:103; end; suppose i <=1; then A75: i=1 by A64,XXREAL_0:1; A76: n choose (2*i1) = 1 by A75,A65,NEWTON:19; n1+1-'2*i = n+2-2*1 by A75,NAT_1:11,XREAL_1:233; hence thesis by A76,NEWTON:4,A75,A65; end; end; A77: (a*Fy0).i = (n choose (2*i1+1)) * a |^ (n1+1-'2*i) * A |^ i1 proof per cases; suppose A78: i <= k; then A79: 2*i <= n1 by NAT_1:13,A60,XREAL_1:66; then A80: 2*i <= n1+1 by NAT_1:13; i <= n1 / 2 by A79, XREAL_1:77; then A81: Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A9,A64; i in dom Fy by A64,A78,A8,A61,FINSEQ_3:25; then A82: Fy.i = Fy0.i by FINSEQ_1:def 7; A83: n1-'2*i = n1- 2*i & n1+1-'2*i = n1+1-2*i by A79,A80,XREAL_1:233; n1+1-'2*i = 1+ (n1-'2*i) by A83; then A84: a |^ (n1+1-'2*i) = a * a |^ (n1-'2*i) by NEWTON:6; (a*Fy0).i = a*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1) by A81,A82,VALUED_1:6 .= (n choose (2*i-'1)) * a |^ (n1+1-'2*i) * A |^ i1 by A84; hence thesis by A70,A65; end; suppose A85: i > k; then i1 >=k by A65,NAT_1:13; then A86: 2*i1+1 > n by NAT_1:13,A60,XREAL_1:66; i >= k1 by A85,NAT_1:13; then 2*i >= 2*k1 by XREAL_1:66; then 2*i = 2*k1 by A60,A66,XXREAL_0:1; then Fy0.i = 0 by A8,A61; then A87: (a*Fy0).i=a*0 by VALUED_1:6; n choose (2*i1+1)=0 by A86,NEWTON:def 3; hence thesis by A87; end; end; thus FY.i = (FxA.i) + (aFy0.i) by RVSUM_1:11 .= ((n choose (2*i1))+ (n choose (2*i1+1))) * a |^ (n1+1-'2*i) * A |^ i1 by A71,A77 .= (n1 choose (2*i-'1)) * a |^ (n1+1-'2*i) * A |^ i1 by A70,A65,NEWTON:22; end; Sum FX = Sum AFx + Sum AFy by RVSUM_1:89 .= Sum (a*Fx) + Sum (A*Fy); hence a|^n1 + Sum FX = Px(a,n1) by A12,A13; len (AFx + AFy) = k by CARD_1:def 7; hence len FX = [\ n1/2 /] by A60,Lm1; thus for i be Nat st 1 <= i <= n1/2 holds FX.i = (n1 choose (2*i)) * a |^ (n1-'2*i) * A |^ i proof let i be Nat such that A88: 1 <= i <= n1/2; set i1=i-'1; i1 +1 = i by A88,XREAL_1:235; then A89: A* A |^ i1 = A |^ i by NEWTON:6; Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A9,A88; then A90: (A*Fy).i = A*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1) by VALUED_1:6 .= (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i by A89; A91: 2*i <= n1 by A88,XREAL_1:83; then A92: n1-'2*i=n1-2*i by XREAL_1:233; A93: 2*i < n1 by A91,A60,XXREAL_0:1; then A94: 2*i <= n by NAT_1:13; A95: i <= n/2 by A93,NAT_1:13, XREAL_1:77; A96: n-'2*i = n- 2*i by A94,XREAL_1:233; n1-'2*i = 1+ (n-'2*i) by A96,A92; then A97: a |^ (n1-'2*i) = a * a |^ (n-'2*i) by NEWTON:6; A98: (a*Fx).i = a * (Fx.i) by VALUED_1:6 .= a*((n choose (2*i)) * a |^ (n-'2*i) * A |^ i) by A95,A11,A88 .= (n choose (2*i)) * a |^ (n1-'2*i) * A |^ i by A97; A99: 2*i-'1+1 =2*i by XREAL_1:235,NAT_1:14,A88; thus FX.i = (AFx).i + (AFy).i by RVSUM_1:11 .= ((n choose (2*i-'1))+(n choose (2*i)))* a |^ (n1-'2*i) * A |^ i by A90,A98 .= (n1 choose (2*i))* a |^ (n1-'2*i) * A |^ i by A99,NEWTON:22; end; end; end; for n holds P[n] from NAT_1:sch 2(A1,A7); hence thesis; end; begin :: Solutions of Pell's Equation - Inequalities theorem Th13: k <= n implies Px(a,k) <= Px(a,n) proof assume k <=n; then reconsider nk=n-k as Nat by NAT_1:21; defpred P[Nat] means Px(a,k) <= Px(a,k+\$1); A1: P[0]; A2: for i be Nat holds P[i] implies P[i+1] proof let i be Nat; assume A3: P[i]; A4: Px(a,k+i+1) = Px(a,k+i)*a+Py(a,k+i)*(a^2-'1) by Th9; a >=2 by NAT_2:29; then a >= 1 by XXREAL_0:2; then Px(a,k+i)*a >= Px(a,k+i)*1 by XREAL_1:64; then Px(a,k+i+1) >= Px(a,k+i)*1+0 by A4,XREAL_1:7; hence thesis by A3,XXREAL_0:2; end; P[n1] from NAT_1:sch 2(A1,A2); then P[nk]; hence thesis; end; registration let a,k; cluster Px(a,k)-> positive; coherence proof Px(a,0) = 1 & Px(a,0) <= Px(a,k) by Th6,Th13; hence thesis; end; end; theorem Th14: k < n implies Py(a,k) < Py(a,n) proof assume A1: k 0 by A1; defpred P[Nat] means \$1 > 0 implies Py(a,k) < Py(a,k+\$1); A3: P[0]; A4: for i be Nat holds P[i] implies P[i+1] proof let i be Nat; assume A5: P[i]; A6: Py(a,k+i+1) = Py(a,k+i)*a+Px(a,k+i) by Th9; a >=2 by NAT_2:29; then a >= 1 by XXREAL_0:2; then Py(a,k+i)*a >= Py(a,k+i)*1 by XREAL_1:64; then A7: Py(a,k+i+1) > Py(a,k+i)*1+0 by A6,XREAL_1:8; i = 0 or i >0; hence thesis by A7,A5,XXREAL_0:2; end; P[n1] from NAT_1:sch 2(A3,A4); then P[nk]; hence thesis by A2; end; theorem Th15: Py(a,k) = Py(a,n) implies k = n proof assume Py(a,k) = Py(a,n); then k >= n >= k by Th14; hence thesis by XXREAL_0:1; end; theorem Th16: Py(a,n) >= n proof defpred P[Nat] means Py(a,\$1) >= \$1; A1:P[0]; A2:P[k] implies P[k+1] proof k+1 > k by NAT_1:13; then A3: Py(a,k)+1 <= Py(a,k+1) by Th14,NAT_1:13; assume P[k]; then k+1 <= Py(a,k)+1 by XREAL_1:6; hence thesis by A3,XXREAL_0:2; end; P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; Lm4:Py(a,k) = 0 implies k=0 proof assume Py(a,k) = 0; then Py(a,k) = Py(a,0) by Th6; hence thesis by Th15; end; registration let a; let k be non zero Nat; cluster Py(a,k) -> non zero; coherence by Lm4; end; registration let a be non trivial Nat; let x be positive Nat; cluster a*x -> non trivial; coherence proof a >= 2 & x >= 1 by NAT_1:14,NAT_2:29; then a*x >= 2*1 by XREAL_1:66; then a*x <>1; hence thesis by NAT_2:28; end; end; theorem Th17: a <> 2 & k <= n implies 2 * Py(a,k) < Px(a,n) proof set A=a^2-'1,S = sqrt A; A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233; assume A2: a<>2 & k <=n; Px(a,k)^2 - (a^2-'1) *Py(a,k)^2 =1 by Th10;then A3: A*(Py(a,k))^2+1 = Px(a,k)^2; a >=2+1 by A2,NAT_1:22,NAT_2:29; then a^2 >= 3*3 by XREAL_1:66; then A >= 9-1 by A1,XREAL_1:9; then A >= 4 by XXREAL_0:2; then 4*(Py(a,k))^2 <= A*(Py(a,k))^2 by XREAL_1:64; then (2*Py(a,k))^2 < Px(a,k)^2 by A3,NAT_1:13; then A4: 2 * Py(a,k) < Px(a,k) by SQUARE_1:15; Px(a,k)<=Px(a,n) by A2,Th13; hence thesis by A4,XXREAL_0:2; end; theorem Th18: a = 2 & k <= n implies (sqrt 3) * Py(a,k) < Px(a,n) proof set A=a^2-'1,S = sqrt A; A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233; assume A2: a = 2 & k <=n; Px(a,k)^2 - (a^2-'1) *Py(a,k)^2 =1 by Th10;then A*(Py(a,k))^2+1 = Px(a,k)^2; then A3: 3*(Py(a,k))^2 < Px(a,k)^2 by A1,A2,NAT_1:13; 3* Py(a,k)^2 = (sqrt 3)^2 * Py(a,k)^2 by SQUARE_1:def 2 .= ((sqrt 3)* Py(a,k))^2; then A4: (sqrt 3)* Py(a,k) < Px(a,k) by A3,SQUARE_1:15; Px(a,k)<=Px(a,n) by A2,Th13; hence thesis by A4,XXREAL_0:2; end; theorem Th19: a = 2 & k < n implies (3 + 2*sqrt 3) * Py(a,k) < Px(a,n) proof A1:(sqrt 3)^2 = 3 & sqrt 3 >= 0 by SQUARE_1:def 2; set A=a^2-'1,S = sqrt A; assume A2: a = 2 & k = Py(a,k) * (2*sqrt 3) + 3*Py(a,k) by A5,A6,XREAL_1:7; hence thesis by A4,XXREAL_0:2; end; theorem Th20: (2*a-1)|^n *(a-1) <= Px(a,n+1) <= a * (2*a) |^ n & (2*a-1)|^n <= Py(a,n+1) <= (2*a) |^ n proof defpred P[Nat] means (2*a-1)|^\$1 <= Py(a,\$1+1) <= (2*a) |^ \$1 & (2*a-1)|^\$1 *(a-1) <= Px(a,\$1+1) <= a * (2*a) |^ \$1; A1: a^2-'1 = a^2-1 by XREAL_1:233,NAT_1:14; A2: (2*a-1)|^0 = 1 & (2*a) |^ 0 =1 by NEWTON:4; A3: a-1 <= a-0 by XREAL_1:10; Py(a,0) = 0 & Px(a,0)= 1 by Th6; then Py(a,1+0) = 1+0*a & Px(a,1+0) = 1*a+ 0*(a^2-'1) by Th9; then A4: P[0] by A2,A3; A5: P[k] implies P[k+1] proof set k1=k+1; assume A6: P[k]; A7: Py(a,k1+1) = Px(a,k1) + Py(a,k1)*a & Px(a,k1+1) = Px(a,k1)*a + Py(a,k1)*(a^2-'1) by Th9; A8: Py(a,k1)*a <= (2*a) |^ k*a by A6,XREAL_1:64; A9: (2*a) |^ k*a + (2*a) |^ k*a = (2*a) |^ k*(2*a) .= (2*a) |^ k1 by NEWTON:6; A10: Py(a,k1)*a >= (2*a-1)|^k*a by A6,XREAL_1:64; A11: (2*a-1)|^k *(a-1) + (2*a-1)|^k*a = (2*a-1)|^k *(2*a-1) .= (2*a-1)|^k1 by NEWTON:6; Px(a,k1)*a <= a * (2*a) |^ k *a & Py(a,k1)*(a^2-'1) <= (2*a) |^ k * (a^2-'1) by A6,XREAL_1:64; then A12: Px(a,k1+1) <= a * (2*a) |^ k *a + (2*a) |^ k * (a^2-'1) by A7,XREAL_1:7; a^2 +a^2-1 <= a^2+a^2-0 by XREAL_1:10; then A13: (2*a) |^ k * (a^2 +a^2-1) <= (2*a) |^ k * (a^2 +a^2) by XREAL_1:64; (2*a-1)|^k * (a^2-'1) <= Py(a,k1)*(a^2-'1) & (2*a-1)|^k *(a-1)*a <= Px(a,k1)*a by A6,XREAL_1:64; then A14: (2*a-1)|^k * (a^2-'1) + (2*a-1)|^k *(a-1)*a <= Px(a,k1+1) by A7,XREAL_1:7; 2*1 <= 2*a by XREAL_1:64,NAT_1:14; then 1--1 <= 2*a; then 2*a^2-a+(1-2*a) <= 2*a^2-a+-1 by XREAL_1:6,12; then (2*a-1)|^k * ((2*a-1)*(a-1)) <= (2*a-1)|^k * (a^2-1 + (a-1)*a) by XREAL_1:64; hence thesis by A8,A7,A6,XREAL_1:7,A9,A10,A11,A1,A13,A12,XXREAL_0:2,A14; end; P[k] from NAT_1:sch 2(A4,A5); hence thesis; end; theorem Th21: for x be positive Nat holds x|^n * (1-1/(2*a*x)) |^ n <= Py(a*x,n+1)/Py(a,n+1) <= (x|^n) * (1 / (1-1/(2*a))|^n) proof let x be positive Nat; set z=n; 1-1/(2*a*x) = (2*a*x)/(2*a*x)-1/(2*a*x) by XCMPLX_1:60 .= (2*a*x-1)/(2*a*x) by XCMPLX_1:120; then x *(1-1/(2*a*x)) = (2*a*x-1)/(2*a) by XCMPLX_1:92; then A1: x|^z * (1-1/(2*a*x)) |^ z = ((2*a*x-1)/(2*a)) to_power z by NEWTON:7 .= ((2*a*x-1) to_power z) / ((2*a) to_power z) by POWER:31; A2: (2*a-1)|^z <= Py(a,z+1) <= (2*a) |^ z by Th20; A3: (2*(a*x)-1)|^z <= Py(a*x,z+1) <= (2*(a*x)) |^ z by Th20; ((2*a*x-1)|^z)*Py(a,z+1) <=Py(a*x,z+1)*((2*a) |^ z) by A2,A3,XREAL_1:66; hence x|^z * (1-1/(2*a*x)) |^ z <= Py(a*x,z+1)/Py(a,z+1) by A1,XREAL_1:102; a>=1 by NAT_1:14; then a+a >= 1+1 by XREAL_1:7; then 1*(2*a) > 1 by NAT_1:13; then 1 > 1/(2*a) by XREAL_1:83; then A4: 1 - 1/(2*a) >1/(2*a)-1/(2*a) by XREAL_1:14; A5: Py(a*x,z+1)*((2*a-1) |^ z)<= ((2*a*x) |^ z)*Py(a,z+1) by A2,A3,XREAL_1:66; (2*a)/(2*a)=1 by XCMPLX_1:60; then (2*a-1)/(2*a) = 1 - (1/(2*a)) by XCMPLX_1:120; then (2*a)/(2*a-1) = 1 / (1 - (1/(2*a))) by XCMPLX_1:57; then (2*a*x)/(2*a-1)= x* (1 / (1 - (1/(2*a)))) by XCMPLX_1:74; then (2*a*x)/(2*a-1)= (x*1) / (1 - 1/(2*a)) by XCMPLX_1:74; then ((2*a*x) to_power z) / ((2*a-1) to_power z) = (x / (1 - 1/(2*a))) to_power z by POWER:31 .= (1*(x to_power z)) / ((1 - 1/(2*a)) to_power z) by A4,POWER:31 .= (x|^z) * (1 / (1-1/(2*a))|^z) by XCMPLX_1:74; hence thesis by A5,XREAL_1:102; end; Lm5: 0 <= 1-r <= 1 implies (1-r) |^ n >= 1-n*r proof defpred P[Nat] means 1-\$1*r >=0 implies (1-r) |^ \$1 >= 1 - \$1 * r; assume A1: 0 <= 1-r <=1; 1-0=1; then A2: r >=0 by A1,XREAL_1:10; A3: P[0] by NEWTON:4; A4: P[k] implies P[k+1] proof assume A5: P[k]; A6: (1-r) |^ (k+1) = (1-r) * (1-r) |^ k by NEWTON:6; assume 1-(k+1)*r >=0; then 1-k*r-r+r >= 0+r by XREAL_1:6; then 1-k*r >= 0; then A7: (1-r) |^ (k+1) >= (1-r)* (1-k*r) by A5,A6,A1,XREAL_1:66; 1-k*r -r +r*r*k >= 1-k*r -r+0 by A2,XREAL_1:7; hence thesis by A7,XXREAL_0:2; end; A8: P[k] from NAT_1:sch 2(A3,A4); 1-n*r>=0 or 1-n*r<0; hence thesis by A8,A1; end; theorem Th22: for x be positive Nat st a > 2*n*(x|^n) holds x|^n - 1/2 < Py(a*x,n+1)/Py(a,n+1) < x|^n + 1/2 proof let x be positive Nat; A1: x|^n * (1-1/(2*a*x)) |^ n <= Py(a*x,n+1)/Py(a,n+1)<= (x|^n) * (1 / (1-1/(2*a))|^n) by Th21; assume A2: a > 2*n*(x|^n); A3: 1- n*(1/(2*a)) = 1- ((n*1)/(2*a)) by XCMPLX_1:74; 2*(x|^n)*n >= 1*n by XREAL_1:64,NAT_1:14; then a >= n by A2,XXREAL_0:2; then a-n >=n-n by XREAL_1:9; then A4: a-n+a >= a+0 by XREAL_1:6; then n / (2*a -n)<= n/a by XREAL_1:118; then 1 + n/(2*a -n) <= 1+n/a by XREAL_1:6; then A5: (x |^ n) * (1 + n/(2*a -n)) <= (x|^n) * (1+n/a) by XREAL_1:64; A6: 2*a - n >0 by A4; A7: 1/1>=1/(2*a) by XREAL_1:118,NAT_1:14; 2*a >n by A6,XREAL_1:47; then n/(2*a)<1 by XREAL_1:191; then A8: 1- (n/(2*a)) >1-1 by XREAL_1:10; 1-1<=1-1/(2*a)<=1-0 by A7,XREAL_1:10; then (1-1/(2*a))|^n >= 1- (n/(2*a)) by Lm5,A3; then 1/ ((1-1/(2*a))|^n) <= 1 / (1- (n/(2*a))) by A8,XREAL_1:118; then A9: x|^n * (1/((1-1/(2*a))|^n)) <= x|^n * (1/(1- (n/(2*a)))) by XREAL_1:64; 1- (n/(2*a)) = (2*a)/(2*a) - (n/(2*a)) by XCMPLX_1:60 .= (2*a -n)/(2*a) by XCMPLX_1:120; then A10: 1/(1- (n/(2*a))) = (2*a-n+n) / (2*a -n) by XCMPLX_1:57 .= (2*a -n)/(2*a -n) + n/(2*a -n) by XCMPLX_1:62 .= 1 + n/(2*a -n) by XCMPLX_1:60,A4; A11: x|^n * (1/((1-1/(2*a))|^n)) <= x|^n * (1+n/a) by A5,A9,A10,XXREAL_0:2; 2*n*(x|^n) = 2*(n*(x|^n)); then n*(x|^n) < a/2 by A2,XREAL_1:81; then n*(x|^n) < 1/2*a; then (n * (x|^n))/a < 1/2 by XREAL_1:83; then (n/a) * (x|^n) < 1/2 by XCMPLX_1:74; then (x|^n) + (x|^n) * (n/a) < x|^n + 1/2 by XREAL_1:6; then A12: x|^n * (1 / (1-1/(2*a))|^n) < x|^n + 1/2 by A11,XXREAL_0:2; 1 >= 1/(2*a*x) by XREAL_1:185,NAT_1:14; then 1-1<= 1-1/(2*a*x) <=1-0 by XREAL_1:10; then A13: x|^n * (1-1/(2*a*x)) |^ n >= x|^n * (1 - n*(1/(2*a*x))) by Lm5,XREAL_1:64; (x|^n)*(n*(1/(2*a*x)))*2 = (x|^n)*((n*1)/(2*a*x))*2 by XCMPLX_1:74 .= ((x|^n)*2)*(n/(2*a*x)) .= (x|^n *2*n) /(2*a*x) by XCMPLX_1:74; then A14: (x|^n)*(n*(1/(2*a*x)))*2 < a / (2*a*x) by A2,XREAL_1:74; 2*x*a >= 1*a by XREAL_1:64,NAT_1:14; then a / (2*a*x) <= 1 by XREAL_1:183; then (x|^n)*(n*(1/(2*a*x)))*2 < 1 by A14,XXREAL_0:2; then (x|^n)*(n*(1/(2*a*x))) < 1/2 by XREAL_1:81; then x|^n - (x|^n)*(n*(1/(2*a*x))) > x|^n -1/2 by XREAL_1:15; then x|^n * (1-1/(2*a*x)) |^ n > (x|^n -1/2) by A13,XXREAL_0:2; hence thesis by A12,A1,XXREAL_0:2; end; begin :: Solutions of Pell's Equation - Equality theorem Th23: x >=0 implies sgn(x)*Py(a,|.x.|) = Py(a,|.x.|) proof assume x>=0; then x=0 or x >0; then sgn(x) =1 or (sgn(x)=0 & x=0) by ABSVALUE:def 2; hence thesis by Th6; end; theorem Th24: x <= 0 implies sgn(x)*Py(a,|.x.|) = -Py(a,|.x.|) proof A1: Py(a,|.0.|)=0 by Th6; assume x<=0; then x=0 or x <0; then sgn(x) = -1 or (sgn(x)=0 & x=0 ) by ABSVALUE:def 2; hence thesis by A1; end; theorem Th25: Px(a,|.x+y.|) = Px(a,|.x.|)*Px(a,|.y.|) + (a^2-'1) * sgn(x)*Py(a,|.x.|)*sgn(y)*Py(a,|.y.|) & sgn(x+y)*Py(a,|.x+y.|) = Px(a,|.x.|)*sgn(y)*Py(a,|.y.|) + sgn(x)*Py(a,|.x.|)*Px(a,|.y.|) proof set i=x,j=y,I=|.x.|,J=|.y.|,IJ = |.x+y.|; set A=a^2-'1,S = sqrt A; A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233; A2: S^2= A by SQUARE_1:def 2; A3: 1 = ((a + S)*(a - S)) |^I by A2,A1 .= ((a + S) |^I)*((a - S) |^I) by NEWTON:7; A4: 1 = ((a + S)*(a - S)) |^J by A2,A1 .= ((a + S) |^J)*((a - S) |^J) by NEWTON:7; deffunc PX(Integer) = Px(a,|.\$1.|); deffunc PY(Integer) = sgn(\$1)*Py(a,|.\$1.|); per cases; suppose A5: i>=0 & j >=0; then A6: i = I & j=J by ABSVALUE:def 1; A7: PY(i) = Py(a,I) by Th23,A5; A8: PY(j) = Py(a,J) by A5,Th23; A9: IJ=i+j by A5,ABSVALUE:def 1; PY(i+j) = Py(a,IJ) by Th23,A5; then PX(i+j) + PY(i+j) * S = (a+ S) |^ IJ by Th11 .= ((a+ S) |^ I) * ((a+ S) |^ J) by A6,A9,NEWTON:8 .= (PX(i) + PY(i) * S) * ((a+ S) |^ J) by A7,Th11 .= (PX(i) + PY(i) * S) * (PX(j) + PY(j) * S) by A8,Th11 .= PX(i)*PX(j) + A * PY(i)*PY(j) + S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2; hence thesis by PELLS_EQ:3; end; suppose A10: i <0 & j >=0; then A11: -i = I & j=J by ABSVALUE:def 1; A12: PY(i) = -Py(a,I) by A10,Th24; A13: PY(j) = Py(a,J) by A10,Th23; per cases; suppose A14: i+j>=0; then IJ=i+j by ABSVALUE:def 1; then A15: IJ+I = J by A11; PY(i+j) = Py(a,IJ) by A14,Th23; then PX(i+j) + PY(i+j) * S = ((a+ S) |^ IJ) * (((a + S) |^I)*((a - S) |^I)) by Th11,A3 .= ((a+ S) |^ IJ) * ((a + S) |^I)* ((a - S) |^I) .= ((a+ S) |^ J)* ((a - S) |^I) by A15,NEWTON:8 .= (PX(j) + PY(j) * S)* ((a - S) |^I) by A13,Th11 .= (PX(j) + PY(j) * S)* (PX(i) + PY(i)*S) by A12,Th11 .= PX(i)*PX(j) + A * PY(i)*PY(j) + S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2; hence thesis by PELLS_EQ:3; end; suppose A16:i+j <0; then IJ=-(i+j) by ABSVALUE:def 1; then A17: IJ+J = I by A11; PY(i+j) = -Py(a,IJ) by A16,Th24; then PX(i+j) + PY(i+j) * S = ((a- S) |^ IJ) * (((a + S) |^J)*((a - S) |^J)) by Th11,A4 .= ((a- S) |^ IJ) * ((a - S) |^J)* ((a + S) |^J) .= ((a- S) |^ I)* ((a + S) |^J) by A17,NEWTON:8 .= (PX(i) + PY(i) * S)* ((a + S) |^J) by A12,Th11 .= (PX(i) + PY(i) * S)* (PX(j) + PY(j)*S) by A13,Th11 .= PX(i)*PX(j) + A * PY(i)*PY(j) + S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2; hence thesis by PELLS_EQ:3; end; end; suppose A18: i >=0 & j <0; then A19: i = I & -j=J by ABSVALUE:def 1; A20: PY(i) = Py(a,I) by Th23,A18; A21: PY(j) = -Py(a,J) by A18,Th24; per cases; suppose A22: i+j>=0; then IJ=i+j by ABSVALUE:def 1; then A23: IJ+J = I by A19; PY(i+j) = Py(a,IJ) by A22,Th23; then PX(i+j) + PY(i+j) * S = ((a+ S) |^ IJ) * (((a + S) |^J)*((a - S) |^J)) by A4,Th11 .= ((a+ S) |^ IJ) * ((a + S) |^J)* ((a - S) |^J) .= ((a+ S) |^ I)* ((a - S) |^J) by A23,NEWTON:8 .= (PX(i) + PY(i) * S)* ((a - S) |^J) by A20,Th11 .= (PX(i) + PY(i) * S)* (PX(j) + PY(j)*S) by A21,Th11 .= PX(i)*PX(j) + A * PY(i)*PY(j) + S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2; hence thesis by PELLS_EQ:3; end; suppose A24:i+j <0; then IJ=-(i+j) by ABSVALUE:def 1; then A25: IJ+I = J by A19; PY(i+j) = -Py(a,IJ) by A24,Th24; then PX(i+j) + PY(i+j) * S = ((a- S) |^ IJ) * (((a - S) |^I)*((a + S) |^I)) by Th11,A3 .= ((a- S) |^ IJ) * ((a - S) |^I)* ((a + S) |^I) .= ((a- S) |^ J)* ((a + S) |^I) by A25,NEWTON:8 .= (PX(j) + PY(j) * S)* ((a + S) |^I) by A21,Th11 .= (PX(j) + PY(j) * S)* (PX(i) + PY(i)*S) by A20,Th11 .= PX(i)*PX(j) + A * PY(i)*PY(j) + S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2; hence thesis by PELLS_EQ:3; end; end; suppose A26: i<0 & j <0; then A27: -i = I & -j=J by ABSVALUE:def 1; A28: PY(i) = -Py(a,I) by A26,Th24; A29: PY(j) = -Py(a,J) by A26,Th24; A30: IJ=-(i+j) by A26,ABSVALUE:def 1; A31: IJ = I+J by A27,A30; PX(i+j) + PY(i+j) * S = PX(i+j) + (-Py(a,IJ)) * S by A26,Th24 .= (a- S) |^ IJ by Th11 .= ((a- S) |^ I) * ((a- S) |^ J) by A31,NEWTON:8 .= (PX(i) + PY(i) * S) * ((a- S) |^ J) by A28,Th11 .= (PX(i) + PY(i) * S) * (PX(j) + PY(j) * S) by A29,Th11 .= PX(i)*PX(j) + A * PY(i)*PY(j) + S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2; hence thesis by PELLS_EQ:3; end; end; begin :: Solutions of Pell's Equation - Congruences theorem Th26: Px(a,n),Py(a,n) are_coprime proof defpred P[Nat] means Px(a,\$1) gcd Py(a,\$1)=1; Px(a,0) =1 & Py(a,0)=0 by Th6; then A1: P[0]; A2: for n st P[n] holds P[n+1] proof set A=a^2-'1; A3: A = a^2 -1 by NAT_1:14,XREAL_1:233; let n such that A4: P[n]; A5: Px(a,n+1) = Px(a,n)*a + Py(a,n)*A& Py(a,n+1) = Px(a,n) + Py(a,n) * a by Th9; thus 1 = (Px(a,n) + Py(a,n) * a) gcd Py(a,n) by A4,EULER_1:8 .= Py(a,n+1) gcd -Py(a,n) by A5, NEWTON02:1 .= (-Py(a,n) + a* Py(a,n+1)) gcd Py(a,n+1) by NEWTON02:5 .= Px(a,n+1) gcd Py(a,n+1) by A3,A5; end; for n holds P[n] from NAT_1:sch 2(A1,A2); then Px(a,n) gcd Py(a,n)=1; hence thesis by INT_2:def 3; end; theorem Th27: Py(a,n),n are_congruent_mod (a-1) proof set A=a-1; A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233; consider Fy,Fx be FinSequence of NAT such that A2:Sum Fy = Py(a,n) & len Fy = [\ (n+1)/2 /] and A3:for i be Nat st 1 <= i <= (n+1)/2 holds Fy.i = (n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a^2-'1) |^ (i-'1) and a|^n + Sum Fx = Px(a,n) & len Fx = [\ n/2 /] & for i be Nat st 1 <= i <= n/2 holds Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * (a^2-'1) |^ i by Th12; per cases; suppose A4: n=0; then Py(a,n) = 0 by Th6; hence thesis by A4,INT_1:11; end; suppose A5: n <> 0; for i be Nat st 1 < i <= len Fy holds (Fy.i) mod A = 0 proof let i be Nat such that A6: 1 < i <= len Fy; i -'1 = i-1 by A6,XREAL_1:233; then i-'1 <> 0 by A6; then reconsider ii= i-'1-1 as Element of NAT by NAT_1:20; i-'1 = ii+1; then A7: (a^2-'1) |^ (i-'1) = A* (a+1) * ((a^2-'1) |^ ii) by A1,NEWTON:6; [\ (n+1)/2 /]<=(n+1)/2 by INT_1:def 6;then i <= (n+1)/2 by A2,A6,XXREAL_0:2; then Fy.i = (n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a^2-'1) |^ (i-'1) by A6,A3 .=(n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a+1) * ((a^2-'1) |^ ii) *A by A7; then A divides Fy.i by INT_1:def 3; hence thesis by INT_1:62; end; then Py(a,n) mod A = Fy.1 mod A by Th1,A2; then (Py(a,n) - Fy.1) mod A =0 by INT_4:22; then A divides Py(a,n)-Fy.1 by INT_1:62; then A8: Py(a,n),Fy.1 are_congruent_mod A by INT_1:def 4; n >=1 by A5,NAT_1:14; then n+1 >= 1+1 & 1+1=2*1 by XREAL_1:7; then A9: (n+1)/2>=1 by XREAL_1:77; 1-'1=1-1 by XREAL_1:233; then A10: (a^2-'1) |^ (1-'1) = 1 by NEWTON:4; 2*1-'1 = 2-1 by XREAL_1:233; then A11: n choose (2*1-'1) = n by A5,NAT_1:14,NEWTON:23; A12: Fy.1 = n * (a |^ (n+1-'2*1)) *1 by A9,A10,A11,A3; A13: A >= 2-1 by NAT_2:29,XREAL_1:9; per cases by A13,XXREAL_0:1; suppose A=1; then A * (Py(a,n)- n) = Py(a,n)- n; hence thesis by INT_1:def 5; end; suppose A14: A >1; a = A*1+1; then a mod A =1 mod A by PEPIN:10 .= 1 by A14,PEPIN:5; then a |^ (n+1-'2*1) mod A = 1 by A14,PEPIN:35; then a |^ (n+1-'2*1),1 are_congruent_mod A by A14,PEPIN:39; then Fy.1,1*n are_congruent_mod A by A12,INT_4:11; hence thesis by A8,INT_1:15; end; end; end; theorem Th28: Px(a,n),Px(b,n) are_congruent_mod (a-b) & Py(a,n),Py(b,n) are_congruent_mod (a-b) proof defpred P[Nat] means Px(a,\$1),Px(b,\$1) are_congruent_mod (a-b) & Py(a,\$1),Py(b,\$1) are_congruent_mod (a-b); Px(a,0) = 1 = Px(b,0) & Py(a,0) = 0 = Py(b,0) by Th6; then A1: P[0] by INT_1:11; A2: for n st P[n] holds P[n+1] proof set A=a^2-'1,B= b^2-'1; A = a^2 -1 & B = b^2-1 by NAT_1:14,XREAL_1:233; then A-B = (a-b)*(a+b); then A3: A,B are_congruent_mod (a-b) by INT_1:def 5; a-b = 1*(a-b); then A4: a,b are_congruent_mod (a-b) by INT_1:def 5; let n such that A5: P[n]; A6: Px(a,n+1) = Px(a,n)*a + Py(a,n)*A & Px(b,n+1) = Px(b,n)*b + Py(b,n)*B by Th9; A7: Py(a,n)*A,Py(b,n)*B are_congruent_mod (a-b) by A5,A3,INT_1:18; Px(a,n)*a,Px(b,n)*b are_congruent_mod (a-b) by A5,A4,INT_1:18; hence Px(a,n+1),Px(b,n+1) are_congruent_mod (a-b) by A6,A7,INT_1:16; A8: Py(a,n+1) = Px(a,n) + Py(a,n)*a& Py(b,n+1) = Px(b,n) + Py(b,n)*b by Th9; Py(a,n)*a,Py(b,n)*b are_congruent_mod (a-b) by A4,A5,INT_1:18; hence Py(a,n+1),Py(b,n+1) are_congruent_mod (a-b) by A8,A5,INT_1:16; end; for n holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th29: a,b are_congruent_mod k implies Py(a,n),Py(b,n) are_congruent_mod k proof assume a,b are_congruent_mod k; then consider x be Integer such that A1: k*x = a-b by INT_1:def 5; consider p be Integer such that A2: (a-b)*p = Py(a,n)-Py(b,n) by Th28,INT_1:def 5; p*(a-b) = p*(x*k) by A1 .= p*x*k; hence thesis by A2, INT_1:def 5; end; Lm6:sgn(x)*sgn(x)*Py(a,|.x.|)=Py(a,|.x.|) proof per cases; suppose A1: x >= 0; thus sgn(x)*sgn(x)*Py(a,|.x.|)=sgn(x)*(sgn(x)*Py(a,|.x.|)) .= sgn(x)*Py(a,|.x.|) by A1,Th23 .= Py(a,|.x.|) by A1,Th23; end; suppose A2: x <= 0; thus sgn(x)*sgn(x)*Py(a,|.x.|)=sgn(x)*(sgn(x)*Py(a,|.x.|)) .= sgn(x)*(-Py(a,|.x.|)) by A2,Th24 .= -(sgn(x)*Py(a,|.x.|)) .= --Py(a,|.x.|) by A2,Th24 .= Py(a,|.x.|); end; end; theorem Th30: sgn(2*x+y)*Py(a,|.2*x+y.|),-sgn(y)*Py(a,|.y.|) are_congruent_mod Px(a,|.x.|) proof set i=x,j=y,A=a^2-'1; 2*i+j = i+(i+j); then sgn(2*i+j)*Py(a,|.2*i+j.|) = Px(a,|.i.|)*sgn(i+j)*Py(a,|.i+j.|) + sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|) by Th25; then sgn(2*i+j)*Py(a,|.2*i+j.|) - sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|) = Px(a,|.i.|)*(sgn(i+j)*Py(a,|.i+j.|)); then A1: sgn(2*i+j)*Py(a,|.2*i+j.|), sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|) are_congruent_mod Px(a,|.i.|) by INT_1:def 5; A2:sgn(i)*Py(a,|.i.|)*(A * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|)) = (sgn(i)*sgn(i)*Py(a,|.i.|))*(a^2-'1)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) .= Py(a,|.i.|) * A*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) by Lm6; A3: Px(a,|.i.|)^2 - (a^2-'1) *Py(a,|.i.|)^2 =1 by Th10; Px(a,|.i+j.|) = Px(a,|.i.|)*Px(a,|.j.|) + (a^2-'1) * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) by Th25; then Px(a,|.i+j.|)- (a^2-'1) * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) = Px(a,|.i.|)*Px(a,|.j.|); then Px(a,|.i+j.|), (a^2-'1) * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|) by INT_1:def 5; then sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|), Py(a,|.i.|)*A*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|) by A2,INT_4:11; then A4: sgn(2*i+j)*Py(a,|.2*i+j.|), (Px(a,|.i.|)^2-1)*sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|) by A3,A1,INT_1:15; (Px(a,|.i.|)^2-1)*sgn(j)*Py(a,|.j.|)-(- sgn(j)*Py(a,|.j.|)) = Px(a,|.i.|) * (Px(a,|.i.|)*sgn(j)*Py(a,|.j.|)); then (Px(a,|.i.|)^2-1)*sgn(j)*Py(a,|.j.|),- sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|) by INT_1:def 5; hence thesis by A4,INT_1:15; end; Lm7: for i,j be Integer holds sgn(4*i+j)*Py(a,|.4*i+j.|),sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|) proof let i,j be Integer; 4*i+j = 2*i+(2*i+j); then A1: sgn(4*i+j)*Py(a,|.4*i+j.|),-sgn(2*i+j)*Py(a,|.2*i+j.|) are_congruent_mod Px(a,|.i.|) by Th30; (-1)* (sgn(2*i+j)*Py(a,|.2*i+j.|)), (-1) * (-sgn(j)*Py(a,|.j.|)) are_congruent_mod Px(a,|.i.|) by Th30,INT_4:11; hence thesis by A1,INT_1:15; end; theorem Th31: sgn(4*x*n+y)*Py(a,|.4*x*n+y.|),sgn(y)*Py(a,|.y.|) are_congruent_mod Px(a,|.x.|) proof defpred P[Nat] means sgn(4*x*\$1+y)*Py(a,|.4*x*\$1+y.|),sgn(y)*Py(a,|.y.|) are_congruent_mod Px(a,|.x.|); A1: P[0] by INT_1:11; A2: for n holds P[n] implies P[n+1] proof let n;set n1=n+1; assume A3: P[n]; 4*x*n1+y = 4*x + (4*x*n+y); then sgn(4*x*n1+y)*Py(a,|.4*x*n1+y.|),sgn(4*x*n+y)*Py(a,|.4*x*n+y.|) are_congruent_mod Px(a,|.x.|) by Lm7; hence thesis by A3,INT_1:15; end; for n holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th32: sgn(x+y)*Py(a,|.x+y.|),sgn(x-y)*Py(a,|.x-y.|) are_congruent_mod Px(a,|.x.|) proof x+y = 2*x+(-x+y); then A1: sgn(x+y)*Py(a,|.x+y.|),-sgn(-x+y)*Py(a,|.-x+y.|) are_congruent_mod Px(a,|.x.|) by Th30; A2: |. -x+y.|= |.-(-x+y).| by COMPLEX1:52; -x+y= (-1)*(x-y); then sgn(-x+y) = sgn(x-y)*sgn(-1) & sgn(-1)=-1 by ABSVALUE:18,def 2; hence thesis by A2,A1; end; Lm8: |.r1.| < r2 implies -r2 < r1 < r2 proof assume A1: |.r1.| < r2; then A2: -|.r1.| > -r2 by XREAL_1:24; -|.r1.| <= r1 <= |.r1.| by ABSVALUE:4; hence thesis by A1,A2,XXREAL_0:2; end; theorem Th33: n1 < n2 <= n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) implies x = y proof assume A1: n1 < n2 <= n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n); then consider i be Integer such that A2: x - y = Px(a,n)*i by INT_1:def 5; A3: n1 < n by A1,XXREAL_0:2; -Px(a,n) < x-y < Px(a,n) proof per cases; suppose A4: a=2; A5: (sqrt 3)^2 = 3 by SQUARE_1:def 2; A6: sqrt 3 >0 by SQUARE_1:25; (3 + 2*sqrt 3)*Py(a,n1) < Px(a,n) by A4,A3,Th19; then Py(a,n1) < Px(a,n) / (3 + 2*sqrt 3) by A6,XREAL_1:81; then A7: - Px(a,n) / (3 + 2*sqrt 3) < x < Px(a,n) / (3 + 2*sqrt 3) by Lm8,A1; (sqrt 3)*Py(a,n2) < Px(a,n) by A4,Th18,A1; then Py(a,n2) < Px(a,n)/(sqrt 3) by XREAL_1:81,A6; then -Px(a,n)/(sqrt 3) < y < Px(a,n)/(sqrt 3) by Lm8,A1; then A8: - Px(a,n) / (3 + 2*sqrt 3) - Px(a,n)/(sqrt 3)< x-y < Px(a,n)/(3 + 2*sqrt 3) - - Px(a,n)/(sqrt 3) by A7,XREAL_1:14; A9: Px(a,n) / (3 + 2*sqrt 3) + Px(a,n)/(sqrt 3) = (Px(a,n) * (sqrt 3) + Px(a,n) * (3 + 2*sqrt 3)) / ((3 + 2*sqrt 3)*(sqrt 3)) by XCMPLX_1:116,A6 .= (Px(a,n) * (3 + 3*sqrt 3))/ ((3 + 2*sqrt 3)*(sqrt 3)) .= Px(a,n) * ((3 + 3*sqrt 3)/ (3* (sqrt 3) + 6)) by A5,XCMPLX_1:74; 3 + 3*sqrt 3 <= 6+3* sqrt 3 by XREAL_1:7; then (3 + 3*sqrt 3)/ (3* (sqrt 3) + 6) <=1 by A6,XREAL_1:183; then A10: Px(a,n) * ((3 + 3*sqrt 3)/ (3* (sqrt 3) + 6)) <= Px(a,n)*1 by XREAL_1:64; then -(Px(a,n) / (3 + 2*sqrt 3) + Px(a,n)/(sqrt 3)) >= -Px(a,n) by A9, XREAL_1:24; hence thesis by A10,A8,A9,XXREAL_0:2; end; suppose A11: a<>2; 2*Py(a,n1) < Px(a,n) by A11,A3,Th17; then |.x.| < Px(a,n)/2 by A1,XREAL_1:81; then A12: - Px(a,n)/2 < x < Px(a,n)/2 by Lm8; 2*Py(a,n2) < Px(a,n) by A11,Th17,A1; then |.y.| < Px(a,n)/2 by A1,XREAL_1:81; then - Px(a,n)/2 < y < Px(a,n)/2 by Lm8; then -Px(a,n)/2 -Px(a,n)/2 < x-y < Px(a,n)/2 - -Px(a,n)/2 by A12,XREAL_1:14; hence thesis; end; end; then (-1)*Px(a,n) < Px(a,n)*i < 1*Px(a,n) by A2; then -1 < i < 1+0 by XREAL_1:64; then 0<= i <=0 by INT_1:7,8; then x - y = 0 by A2; hence thesis; end; Lm9: n1 < n2 <= 2*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) implies n1 = 2*n -n2 proof assume A1: n1 < n2 <= 2*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) & n1 <> 2*n -n2; per cases; suppose n2 <= n; then Py(a,n1) = Py(a,n2) by A1,Th33; hence thesis by A1,Th15; end; suppose A2: n2 >n; then reconsider m=n2-n as Nat by NAT_1:21; n+n-n2 >=n2-n2 by A1,XREAL_1:9; then reconsider nm=n-m as Element of NAT by INT_1:3; A3: sgn(n2)*Py(a,|.n2.|) = Py(a,n2) & sgn(nm)*Py(a,|.nm.|) =Py(a,nm) by Th23; n2 = n+m;then sgn(n2)*Py(a,|.n2.|),sgn(nm)*Py(a,|.nm.|) are_congruent_mod Px(a,|.n.|) by Th32; then sgn(y)*Py(a,n2),sgn(y)*Py(a,nm) are_congruent_mod Px(a,n) by A3,INT_4:11; then y,sgn(y)*Py(a,nm) are_congruent_mod Px(a,n) by A1,ABSVALUE:17; then A4: x,sgn(y)*Py(a,nm) are_congruent_mod Px(a,n) by A1,INT_1:15; then A5: sgn(y)*Py(a,nm),x are_congruent_mod Px(a,n) by INT_1:14; nm = n+n-n2; then A6: nm < n+n-n by A2,XREAL_1:15; A7: n1 < nm or nm < n1 by A1,XXREAL_0:1; y <>0 by A1; then y >0 or y <0; then sgn y =1 or sgn y = -1 by ABSVALUE:def 2; then sgn(y)*Py(a,nm) = Py(a,nm) or sgn(y)*Py(a,nm) = -Py(a,nm); then A8: |.sgn(y)*Py(a,nm).| = Py(a,nm); per cases; suppose n1 <= n; then A9: Py(a,n1) = Py(a,nm) or Py(a,n1) = - Py(a,nm) by A1,A4,INT_1:14,A8,A6,A7,Th33; Py(a,n1) <> - Py(a,nm) proof assume A10: Py(a,n1) = - Py(a,nm); n1=0 & nm=0 by A10; hence thesis by A1; end; hence thesis by A9,A1,Th15; end; suppose A11: n1 > n; then reconsider k=n1-n as Nat by NAT_1:21; n+n >= n1 by A1,XXREAL_0:2; then n+n-n1 >=n1-n1 by XREAL_1:9; then reconsider nk=n-k as Element of NAT by INT_1:3; A12: sgn(n1)*Py(a,|.n1.|) = Py(a,n1)& sgn(nk)*Py(a,|.nk.|)=Py(a,nk) by Th23; n1 = n+k; then sgn(n1)*Py(a,|.n1.|),sgn(nk)*Py(a,|.nk.|) are_congruent_mod Px(a,|.n.|) by Th32; then sgn(x)*Py(a,n1),sgn(x)*Py(a,nk) are_congruent_mod Px(a,n) by A12,INT_4:11; then x,sgn(x)*Py(a,nk) are_congruent_mod Px(a,n) by A1,ABSVALUE:17; then A13: sgn(y)*Py(a,nm),sgn(x)*Py(a,nk) are_congruent_mod Px(a,n) by A5,INT_1:15; nk = n+n-n1; then A14: nk < n+n-n by A11,XREAL_1:15; A15: nk<>nm by A1; then A16: nk < nm or nm < nk by XXREAL_0:1; x <>0 by A1,A11; then x >0 or x <0; then sgn x =1 or sgn x = -1 by ABSVALUE:def 2; then sgn(x)*Py(a,nk) = Py(a,nk) or sgn(x)*Py(a,nk) = -Py(a,nk); then A17: |.sgn(x)*Py(a,nk).|= Py(a,nk); A18: Py(a,nk) = Py(a,nm) or Py(a,nk) = -Py(a,nm) by Th33,A16,A14,A6,A13,INT_1:14,A8,A17; Py(a,nk) <> - Py(a,nm) proof assume A19: Py(a,nk) = - Py(a,nm); nk=0 & nm=0 by A19; hence thesis by A1; end; hence thesis by A18,A15,Th15; end; end; end; theorem Th34: n1 <= 2*n & n2 <= 2*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n proof assume that A1: n1 <= 2*n & n2 <= 2*n and A2: |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n); n1=n2 or n1>n2 or n1 2*n-2*n & n2 >0 by XREAL_1:9,A1; then A4: sgn(m1) = 1 & sgn(n2) = 1 by ABSVALUE:def 2; y <>0 by A2,A1; then y >0 or y < 0; then sgn y = 1 or sgn y = -1 by ABSVALUE:def 2; then A5: |.sgn(y)*(-Py(a,m1)).| = Py(a,m1); 2*n+m1 = n2; then sgn(n2)*Py(a,|.n2.|),-sgn(m1)*Py(a,|.m1.|) are_congruent_mod Px(a,|.n.|) by Th30; then sgn(y)*Py(a,|.n2.|),sgn(y)*(-Py(a,m1)) are_congruent_mod Px(a,n) by A4,INT_4:11; then y, sgn(y)*(-Py(a,m1)) are_congruent_mod Px(a,n) by ABSVALUE:17,A2; then A6: x, sgn(y)*(-Py(a,m1)) are_congruent_mod Px(a,n) by INT_1:15,A2; per cases by XXREAL_0:1; suppose n1 < m1 or n1 >m1; then n1 = 2*n -m1 or m1 = 2*n -n1 by A6,INT_1:14,A1,A2,A5,A3,Lm9; then n1 -- n2 = 2*(2*n); hence thesis by INT_1:def 5; end; suppose n1=m1; then n1-n2 = (-1)*(2*n); hence thesis by INT_1:def 5; end; end; Lm11: 2*n < n1 <= 4*n & 2*n < n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n proof assume that A1: 2*n < n1 <= 4*n & 2*n < n2 <= 4*n and A2: |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n); reconsider m2=n2-2*n as Nat by A1,NAT_1:21; A3: m2 <= 4*n -2*n by A1,XREAL_1:9; m2 > 2*n-2*n & n2 >0 by XREAL_1:9,A1; then A4: sgn(m2) = 1 & sgn(n2) = 1 by ABSVALUE:def 2; y <>0 by A2,A1; then y >0 or y < 0; then sgn y = 1 or sgn y = -1 by ABSVALUE:def 2; then A5: |.sgn(y)*(-Py(a,m2)).| = Py(a,m2); reconsider m1=n1-2*n as Nat by A1,NAT_1:21; A6: m1 <= 4*n -2*n by A1,XREAL_1:9; m1 > 2*n-2*n & n1 >0 by XREAL_1:9,A1; then A7: sgn(m1) = 1 & sgn(n1) = 1 by ABSVALUE:def 2; x <>0 by A2,A1; then x >0 or x < 0; then sgn x = 1 or sgn x = -1 by ABSVALUE:def 2; then A8: |.sgn(x)*(-Py(a,m1)).| = Py(a,m1); 2*n+m1 = n1; then sgn(n1)*Py(a,|.n1.|),-sgn(m1)*Py(a,|.m1.|) are_congruent_mod Px(a,|.n.|) by Th30; then sgn(x)*Py(a,|.n1.|),sgn(x)*(-Py(a,m1)) are_congruent_mod Px(a,n) by A7,INT_4:11; then x, sgn(x)*(-Py(a,m1)) are_congruent_mod Px(a,n) by ABSVALUE:17,A2; then sgn(x)*(-Py(a,m1)),x are_congruent_mod Px(a,n) by INT_1:14; then A9: sgn(x)*(-Py(a,m1)),y are_congruent_mod Px(a,n) by INT_1:15,A2; 2*n+m2 = n2; then sgn(n2)*Py(a,|.n2.|),-sgn(m2)*Py(a,|.m2.|) are_congruent_mod Px(a,|.n.|) by Th30; then sgn(y)*Py(a,|.n2.|),sgn(y)*(-Py(a,m2)) are_congruent_mod Px(a,n) by A4,INT_4:11; then y, sgn(y)*(-Py(a,m2)) are_congruent_mod Px(a,n) by ABSVALUE:17,A2; then A10: sgn(x)*(-Py(a,m1)),sgn(y)*(-Py(a,m2)) are_congruent_mod Px(a,n) by A9,INT_1:15; per cases by XXREAL_0:1; suppose m1 < m2 or m1 >m2; then m1 = 2*n -m2 or m2 = 2*n -m1 by A10,INT_1:14,A5,A3,A6,A8,Lm9; then n1 -- n2 = 3*(2*n); hence thesis by INT_1:def 5; end; suppose m1=m2; then n1-n2 = 0*(2*n); hence thesis by INT_1:def 5; end; end; theorem Th35: n1 <= 4*n & n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n proof assume A1: n1 <= 4*n & n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n); then A2: y,x are_congruent_mod Px(a,n) by INT_1:14; per cases; suppose n1 <= 2*n & n2 <= 2*n or n1 > 2*n & n2 > 2*n or n1 <= 2*n < n2; hence thesis by A1,Th34,Lm10,Lm11; end; suppose n2 <=2*n 0 implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n proof assume that A1: Py(a,n1),Py(a,n2) are_congruent_mod Px(a,n) and A2: n>0; reconsider m1 = n1 mod 4*n , d1= n1 div 4*n as Element of NAT; A3: n1 - d1*(4*n) = m1 by A2,INT_1:def 10; then sgn(4*d1*n+m1)*Py(a,|.4*d1*n+m1.|),sgn(m1)*Py(a,|.m1.|) are_congruent_mod Px(a,|.n.|) by Th31; then Py(a,n1),sgn(m1)*Py(a,|.m1.|) are_congruent_mod Px(a,|.n.|) by A3,Th23; then Py(a,n1),Py(a,m1) are_congruent_mod Px(a,n) by Th23; then A4: Py(a,m1),Py(a,n1) are_congruent_mod Px(a,n) by INT_1:14; reconsider m2 = n2 mod 4*n , d2= n2 div 4*n as Element of NAT; A5: m1 <= 4*n & m2 <=4*n by A2,INT_1:58; A6: |.Py(a,m1).| = Py(a,m1) & |.Py(a,m2).| = Py(a,m2); A7: n2 - d2*(4*n) = m2 by A2,INT_1:def 10; then sgn(4*d2*n+m2)*Py(a,|.4*d2*n+m2.|),sgn(m2)*Py(a,|.m2.|) are_congruent_mod Px(a,|.n.|) by Th31; then Py(a,n2),sgn(m2)*Py(a,|.m2.|) are_congruent_mod Px(a,|.n.|) by A7,Th23; then Py(a,n2),Py(a,m2) are_congruent_mod Px(a,n) by Th23; then Py(a,n1),Py(a,m2) are_congruent_mod Px(a,n) by A1,INT_1:15; then Py(a,m1),Py(a,m2) are_congruent_mod Px(a,n) by A4,INT_1:15; then A8: m1,m2 are_congruent_mod 2*n or m1,-m2 are_congruent_mod 2*n by A6,A5,Th35; n1-m1 = (2*d1)*(2*n) by A3; then n1,m1 are_congruent_mod 2*n by INT_1:def 5; then A9:n1,m2 are_congruent_mod 2*n or n1,-m2 are_congruent_mod 2*n by A8,INT_1:15; m2-n2 = (-2*d2)*(2*n) & -m2--n2 = (2*d2)*(2*n) by A7; then m2,n2 are_congruent_mod 2*n & -m2,-n2 are_congruent_mod 2*n by INT_1:def 5; hence thesis by A9,INT_1:15; end; begin :: Solutions of Pell's Equation - Divisibility theorem Th37: Py(a,n) divides Py(a,n*k) proof defpred P[Nat] means Py(a,n) divides Py(a,n*\$1); Py(a,n) * 0 = Py(a,n*0) by Th6; then A1: P[0] by INT_1:def 3; A2: for k holds P[k] implies P[k+1] proof let k; assume A3: P[k]; A4: Py(a,n*k+n) = sgn(n*k+n)*Py(a,|.n*k+n.|) & sgn(n)*Py(a,|.n.|) = Py(a,n) & sgn(n*k)*Py(a,|.n*k.|)= Py(a,n*k) by Th23; then A5: Py(a,|.n*k+n.|) = Px(a,|.n*k.|)*sgn(n)*Py(a,|.n.|) + sgn(n*k)*Py(a,|.n*k.|)*Px(a,|.n.|) by Th25 .= Px(a,n*k) * Py(a,n) + Py(a,n*k)*Px(a,n) by A4; A6: Py(a,n) divides Py(a,n*k)*Px(a,n) by A3,INT_2:2; Py(a,n) divides Px(a,n*k) * Py(a,n) by NAT_D:9; hence thesis by A5,A6,NAT_D:8; end; for k holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th38: Py(a,n*k), k * (Px(a,n) |^ (k-'1)) *Py(a,n) are_congruent_mod Py(a,n)^2 proof set m=min_Pell's_solution_of (a^2-'1); set x = Px(a,n),y=Py(a,n),s = sqrt (a^2-'1),ys= y*s; per cases; suppose n=0 or k=0; then (y=0 or k=0) & Py(a,n*k)=0 by Th6; hence thesis by INT_1:11; end; suppose A1: n>0 & k >0; set I=(x,ys) In_Power k; A2: x+ys = (m`1 + m`2 *s) |^n by Def2; A3: Px(a,n*k)+Py(a,n*k)*s = (m`1 + m`2 *s) |^(n*k) by Def2 .= (x+ys) |^ k by A2,NEWTON:9 .= Sum I by NEWTON:30; consider e,o be complex-valued FinSequence such that A4: len e = [\len I/2/] & len o = [/len I/2 \] and A5: Sum I = Sum e + Sum o and A6: for n holds e.n = I.(2*n) & o.n = I.(2*n-1) by Th2; A7: len I = k+1 by NEWTON:def 4; s|^(1+1) = s* s|^1 by NEWTON:6 .= s^2 .= (a^2-'1) by SQUARE_1:def 2; then A8: ys|^2 = (y |^ 2) * (a^2-'1) by NEWTON:7; rng o c= NAT proof let w be object;assume w in rng o; then consider z be object such that A9: z in dom o & o.z=w by FUNCT_1:def 3; reconsider z as Nat by A9;set Z=2*z-1; A10: w = I.Z by A6,A9; A11: 1<= z <= len o by A9,FINSEQ_3:25; A12: 2*z >=2*1 by XREAL_1:64,A9,FINSEQ_3:25; then A13: Z >= 2-1 by XREAL_1:9; reconsider zz=Z,m = Z-1 as Nat by A12; A14: len I/2+1 = (len I+2)/2; len o < len I/2 +1 by A4,INT_1:def 7; then z < len I/2+1 by A11,XXREAL_0:2; then 2*z < k+1+2 & k+1+2 = k+2+1 by A7,A14,XREAL_1:79; then A15: 2*z <= k+1+1 by NAT_1:13; then A16: Z <= k+1 by XREAL_1:20; reconsider l = k+1-zz as Nat by NAT_1:21,XREAL_1:20,A15; A17: Z in dom I by A16,A7,A13,FINSEQ_3:25; l = k-m; then A18: I.Z = (k choose m) * x|^l *ys|^m by A17,NEWTON:def 4; reconsider z1=z-1 as Nat by A11; m = 2*z1; then ys|^m = ((y |^ 2) * (a^2-'1)) |^z1 by A8,NEWTON:9; hence thesis by A10,A18,ORDINAL1:def 12; end; then reconsider o as FinSequence of NAT by FINSEQ_1:def 4; defpred E[object,object] means \$2 in NAT & for n be Nat st n=\$2 holds e.\$1 = s * n & for N be Nat st N=\$1 holds N-1 is Nat & 2*N-1 is Nat & k+1-2*N is Nat & for n1,m,l be Nat st n1=N-1 & m= 2*N-1 & l=k+1-2*N holds \$2 =(k choose m) * x|^l *(((y |^ 2) * (a^2-'1)) |^ n1 * y); A19:for n st n in Seg len e ex x be object st E[n,x] proof let n such that A20: n in Seg len e; set N=2*n; A21: 1<= n <= len e by A20,FINSEQ_1:1; then N >=2*1 by XREAL_1:64; then A22: N >= 1 by XXREAL_0:2; reconsider m = N-1,n1=n-1 as Nat by A21; len e <= len I/2 by A4,INT_1:def 6; then n <= len I/2 by A21,XXREAL_0:2; then A23: N <= k+1 by A7,XREAL_1:83; then reconsider l = k+1-N as Nat by NAT_1:21; take U= (k choose m) * x|^l *(((y |^ 2) * (a^2-'1)) |^ n1 * y); thus U in NAT by ORDINAL1:def 12; let u be Nat such that A24: u=U; A25: N in dom I by A23,A7,A22,FINSEQ_3:25; l = k-m; then A26: I.N = (k choose m) * x|^l *ys|^m by A25,NEWTON:def 4; m = 2*n1+1; then ys|^m = (ys |^(2*n1)) * ys by NEWTON:6 .= ((y |^ 2) * (a^2-'1)) |^ n1 * ys by A8,NEWTON:9; hence e.n = s * u by A6,A26,A24; let nn be Nat such that A27: n=nn; nn-1 =n1 & 2*nn-1 = m & k+1-2*nn = l by A27; hence thesis; end; consider p be FinSequence such that A28: dom p = Seg len e & for n st n in Seg len e holds E[n,p.n] from FINSEQ_1:sch 1(A19); rng p c= NAT proof let w be object;assume w in rng p; then ex n be object st n in dom p & p.n=w by FUNCT_1:def 3; hence thesis by A28; end; then reconsider p as FinSequence of NAT by FINSEQ_1:def 4; A29: dom (s*p) = dom p & dom p = dom e by A28,VALUED_1:def 5,FINSEQ_1:def 3; A30: len p=len e by A28,FINSEQ_1:def 3; for n st n in dom p holds e.n = (s*p).n proof let n; assume n in dom p; hence e.n = s * (p.n) by A28 .= (s*p).n by VALUED_1:6; end; then e = s*p by A29,FINSEQ_1:13; then Sum I = Sum o+s * Sum p by A5,RVSUM_1:87; then A31: Py(a,n*k) = Sum p by A3,PELLS_EQ:3; A32: Sum p is Nat by TARSKI:1; A33: y|^(1+1) = y* y|^1 by NEWTON:6 .= y*y; for n st 1 < n <= len p holds (p.n) mod y^2 =0 proof let n; assume A34: 1 < n <= len p; then A35: n in Seg len e by A28,FINSEQ_3:25; then E[n,p.n] by A28; then reconsider n1=n-1, m=2*n-1, l= k+1-2*n as Nat; A36: p.n = (k choose m) * x|^l *(((y |^ 2) * (a^2-'1)) |^ n1 * y) by A35,A28; A37: n-1 > 1-1 by A34,XREAL_1:9; y^2 divides ((y |^ 2) * (a^2-'1)) |^ n1 by A37,NEWTON02:14,A33,INT_1:def 3; then y^2 divides ((y |^ 2) * (a^2-'1)) |^ n1 * y by NAT_D:9; then y^2 divides p.n by A36, NAT_D:9; hence thesis by INT_1:62,A1; end; then Sum p mod y^2 = p.1 mod y^2 by Th1; then ((Sum p) - (p.1)) mod (y^2) =0 by A32,INT_4:22,A1; then y^2 divides Sum p - p.1 by INT_1:62,A1; then A38: Sum p, p.1 are_congruent_mod y^2 by INT_1:def 4; len I >= 1+1 & 1+1= 2*1 by XREAL_1:6,A7,A1,NAT_1:14; then len I/2 >= 1 by XREAL_1:77; then len p >= 1 by INT_1:54,A30,A4; then A39: 1 in Seg len e by A28,FINSEQ_3:25; then E[1,p.1] by A28; then reconsider l= k+1-2*1 as Nat; A40: k choose 1 = k by NEWTON:23,A1,NAT_1:14; A41: ((y |^ 2) * (a^2-'1)) |^ 0 = 1 by NEWTON:4; A42: l=k-1; 1-1=0 & 2*1-1=1;then p.1 = k * x|^l *(1 * y) by A39,A28,A40,A41; hence thesis by A42,A31,A38,XREAL_0:def 2; end; end; theorem Th39: k >0 & Py(a,k) divides Py(a,n) implies k divides n proof set Pk=Py(a,k),Pn=Py(a,n); set r=n mod k,q = n div k; assume A1: k>0 & Pk divides Pn; reconsider r,q as Element of NAT; A2: r = n - q*k by A1,INT_1:def 10; then n = r+q*k; then sgn(n)*Py(a,|.n.|) = Px(a,|.r.|)*sgn(q*k)*Py(a,|.q*k.|) + sgn(r)*Py(a,|.r.|)*Px(a,|.q*k.|) by Th25; then A3:Py(a,n) = Px(a,|.r.|)*(sgn(q*k)*Py(a,|.q*k.|)) + sgn(r)*Py(a,|.r.|)*Px(a,|.q*k.|) by Th23 .= Px(a,|.r.|)*Py(a,q*k) + sgn(r)*Py(a,|.r.|)*Px(a,|.q*k.|) by Th23 .= Px(a,r)*Py(a,q*k) + Py(a,r)*Px(a,q*k) by Th23; A4: Pk divides Py(a,q*k) by Th37; Pk divides Px(a,r)*Py(a,q*k) by Th37,INT_2:2; then A5: Pk divides Py(a,r)*Px(a,q*k) by INT_2:1,A1,A3; A6: Pk,Px(a,k*q) are_coprime proof Pk gcd Px(a,k*q) divides Py(a,k) by INT_2:def 2; then A7: Py(a,k) gcd Px(a,k*q) divides Py(a,q*k) by A4, INT_2:9; Pk gcd Px(a,k*q) divides Px(a,k*q) by INT_2:def 2; then Pk gcd Px(a,k*q) divides Py(a,q*k) gcd Px(a,k*q) by A7,INT_2:22; then Pk gcd Px(a,k*q) divides 1 by Th26,INT_2:def 3; then Pk gcd Px(a,k*q) = 1 by INT_2:13; hence thesis by INT_2:def 3; end; r=0 proof assume r<>0; then |.Pk.| <= |.Py(a,r).| by A6,INT_4:6,A5,INT_2:25; hence thesis by Th14,INT_1:58,A1; end; hence thesis by A2,INT_1:def 3; end; theorem Th40: Py(a,k)^2 divides Py(a,n) implies Py(a,k) divides n proof assume A1: Py(a,k)^2 divides Py(a,n); per cases; suppose k=0; then Py(a,k)=0 by Th6; then ex i be Integer st 0*i = Py(a,n) by A1,INT_1:def 3; then Py(a,k)*0 = n; hence thesis by INT_1:def 3; end; suppose A2:k>0; Py(a,k) divides Py(a,k)^2 by INT_1:def 3; then Py(a,k) divides Py(a,n) by A1,INT_2:9; then consider w be Nat such that A3: k*w = n by NAT_D:def 3,Th39,A2; A4: w divides n by A3,NAT_D:def 3; Py(a,k)^2 divides Py(a,n)-0 by A1; then A5: 0,Py(a,n) are_congruent_mod Py(a,k)^2 by INT_1:14,def 4; Py(a,n), w * (Px(a,k) |^ (w-'1)) *Py(a,k) are_congruent_mod Py(a,k)^2 by Th38,A3; then A6: 0*(Px(a,k) |^ (w-'1)),(w* Py(a,k))*(Px(a,k) |^ (w-'1)) are_congruent_mod Py(a,k)^2 by A5,INT_1:15; A7: Py(a,k) in NAT & w in NAT by ORDINAL1:def 12; A8: Py(a,k)^2 = Py(a,k) * Py(a,k) |^1 .= Py(a,k) |^(1+1) by NEWTON:6; Py(a,k),Px(a,k) are_coprime by Th26; then Py(a,k) |^2,Px(a,k) are_coprime by WSIERP_1:10; then 0,w* Py(a,k) are_congruent_mod Py(a,k)^2 by A6,A8,INT_4:9,WSIERP_1:10; then Py(a,k)^2 divides w* Py(a,k)-0 by INT_1:def 4,14; then Py(a,k) divides w or Py(a,k) = 0 by A7,PYTHTRIP:7; hence thesis by A4,A2,INT_2:9; end; end; begin :: Special Case of Pell's Equation is Diophantin theorem for y,z,a be Nat holds y = Py(a,z) & a > 1 iff ex x,x1,y1,A,x2,y2 be Nat st a>1 & [x,y] is Pell's_solution of (a^2-'1) & [x1,y1] is Pell's_solution of (a^2-'1)& y1>=y & A > y & y >= z & [x2,y2] is Pell's_solution of (A^2-'1) & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2*y & A,1 are_congruent_mod 2*y & y1,0 are_congruent_mod y^2 proof let y,z,a be Nat; thus y = Py(a,z) & a > 1 implies ex x,x1,y1,A,x2,y2 be Nat st a>1 & [x,y] is Pell's_solution of (a^2-'1) & [x1,y1] is Pell's_solution of (a^2-'1)& y1>=y & A>y & y >= z & [x2,y2] is Pell's_solution of (A^2-'1) & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2*y & A,1 are_congruent_mod 2*y & y1,0 are_congruent_mod y^2 proof assume A1: y=Py(a,z) & a >1; then A2:a is non trivial by NAT_2:28; set x= Px(a,z); A3: a>=1+1 by NAT_1:13,A1; A4: a^2-'1 = a^2-1 by XREAL_1:233,NAT_1:14,A1; x^2 - (a^2-'1) *y^2 =1 by A1,Th10,A2; then A5: [x,y] is Pell's_solution of (a^2-'1) & a > 1 by A1,Lm3; A6: y >= z by Th16,A1,A2; per cases; suppose A7: y=0; then A8: z=0 by A1,A2; then A9: x=1 by Th6,A2; set x1=x,y1=y,y2=y, A =1; A^2-'1 = 1-1 by XREAL_1:233; then A10: 1^2-(A^2-'1)*y2^2 = 1; 1 in INT & 0 in INT by INT_1:def 2; then A11: [1,0] in [:INT,INT:] by ZFMISC_1:87; [1,0]`1 = 1 & [1,0]`2=0; then A12: [1,y2] is Pell's_solution of (A^2-'1) by A10,A11,A7,PELLS_EQ:def 1; A13: y2,y are_congruent_mod x1 by INT_1:11; A14: A,a are_congruent_mod x1 by INT_1:13,A9; A15: A,1 are_congruent_mod 2*y by INT_1:11; y1,0 are_congruent_mod y^2 by A7,INT_1:11; hence thesis by A5,A12,A13,A14,A8,A7,A15; end; suppose A16: y>0; reconsider B=(a^2-'1)*((2*y^2)^2) as non square Nat by A2,A16; set M = min_Pell's_solution_of B; set x1=M`1,Y1=M`2; A17: x1^2-B*Y1^2=1 by PELLS_EQ:def 1; set y1=2*y^2*Y1; A18: x1=[x1,y1]`1 & y1=[x1,y1]`2; x1 in INT & y1 in INT by INT_1:def 2; then A19: [x1,y1] in [:INT,INT:] by ZFMISC_1:87; A20: x1^2 - (a^2-'1)*y1^2= 1+B*Y1^2 - (a^2-'1)*y1^2 by PELLS_EQ:def 1 .=1; then A21: [x1,y1] is Pell's_solution of (a^2-'1) by A18,A19,PELLS_EQ:def 1; 2*Y1*y >=1*1 by A16,NAT_1:14; then A22: 2*Y1*y*y >= 1*y by XREAL_1:66; A23: y1 >0 by A22; then A24: y1^2 >=1 & y1 >=1 by NAT_1:14; y1= y^2*(2*Y1) & y1 = (2*y)*(y*Y1); then A25: y^2 divides y1-0 & 2*y divides y1 by INT_1:def 3; then A26: y1,0 are_congruent_mod y^2 by INT_1:def 4; a^2 >= 2*a & a+a > a+1 by A2,A1,NAT_2:29,XREAL_1:8,64; then a^2 > a+1 by XXREAL_0:2; then A27: a^2-'1>a by A4,XREAL_1:20; then A28: B > a *1 by A16,NAT_1:14, XREAL_1:97; Y1^2 >= 1^2 by NAT_1:14; then 1+B*Y1^2 > a by NAT_1:13,A28, XREAL_1:66; then x1^2-a >=a-a by A17,XREAL_1:9; then reconsider x1a=x1^2-a as Element of NAT by INT_1:3; set A = a+x1^2*x1a; A >=2+0 by A3,XREAL_1:7; then A <>1 & A is non empty; then reconsider A as non trivial Nat by NAT_2:28; A-a = x1*(x1*x1a); then A29: A,a are_congruent_mod x1 by INT_1:def 4,def 3; A = a+(1+(a^2-'1)*y1^2)*(1+(a^2-'1)*y1^2-a) by A20; then A30: A-1 = y1*(y1*( (a^2-'1) + (1+(a^2-'1)*y1^2)*(a^2-'1) -a * (a^2-'1))); then A31: y1 divides A-1 by INT_1:def 3; then A32: 2*y divides A-1 by A25,INT_2:9; A33: A,1 are_congruent_mod 2*y by A31,A25,INT_2:9,INT_1:def 4; (a^2-'1)*(y1^2) >= a*1 by A27,A24,XREAL_1:66; then 2+ (a^2-'1)*(y1^2) > a*1+0 by XREAL_1:8; then 2+(a^2-'1)*y1^2-a >a-a by XREAL_1:9; then y1* ((a^2-'1)*(2+(a^2-'1)*y1^2-a)) >= 1*1 by A2,A23,NAT_1:14; then A-1 >=1*y1 & A-0 > A-1 by A30,XREAL_1:66,10; then A > y1 by XXREAL_0:2; then A34: A > y by A22, XXREAL_0:2; set x2 = Px(A,z),y2 = Py(A,z); x2^2 - (A^2-'1) *y2^2 =1 by Th10; then A35: [x2,y2] is Pell's_solution of (A^2-'1) by Lm3; A-1 divides y2-z by Th27,INT_1:def 4; then y2,z are_congruent_mod 2*y by INT_1:def 4,A32,INT_2:9; hence thesis by A5,A21,A6,A35,A2,A1,Th29,A29,A33,A26,A22,A34; end; end; given x,x1,y1,A,x2,y2 be Nat such that A36: a>1 and A37: [x,y] is Pell's_solution of (a^2-'1) and A38: [x1,y1] is Pell's_solution of (a^2-'1) and A39: y1 >=y & A > y and A40: y >= z and A41: [x2,y2] is Pell's_solution of (A^2-'1) and A42: y2,y are_congruent_mod x1 and A43: A,a are_congruent_mod x1 and A44: y2,z are_congruent_mod 2*y and A45: A,1 are_congruent_mod 2*y and A46: y1,0 are_congruent_mod y^2; A47: a is non trivial by NAT_2:28,A36; per cases; suppose A48: y=0; then z=0 by A40; hence thesis by A36,A47,Th6,A48; end; suppose A49: y >0; then y >=1 by NAT_1:14; then reconsider A as non trivial Nat by A39,NAT_2:28; consider w be Nat such that A50: x = Px(a,w) & y = Py(a,w) by A47,A37,Th7; consider u be Nat such that A51: x1 = Px(a,u) & y1 = Py(a,u) by A47,A38,Th7; consider v be Nat such that A52: x2 = Px(A,v) & y2 = Py(A,v) by A41,Th7; A53: y2,Py(a,v) are_congruent_mod x1 by A47,A43,A52,Th29; y,y2 are_congruent_mod x1 by A42,INT_1:14; then A54: y,Py(a,v) are_congruent_mod Px(a,u) by A51,A53,INT_1:15; A55: u<>0 by Th6,A51,A49,A39,A47; Py(A,v), v are_congruent_mod 2*y proof A56: 2*y divides A-1 by A45,INT_1:def 4; A-1 divides Py(A,v)-v by Th27,INT_1:def 4; hence thesis by INT_1:def 4,A56,INT_2:9; end; then v,y2 are_congruent_mod 2*y by A52,INT_1:14; then A57: v,z are_congruent_mod 2*y by A44,INT_1:15; A58: y^2 divides y1-0 by A46,INT_1:def 4; A59: z,v are_congruent_mod 2*y by A57,INT_1:14; A60: Py(a,v),Py(a,w) are_congruent_mod Px(a,u) by A54,A50,INT_1:14; consider r be Integer such that A61: y*r = u by A58,A51,A50,Th40,INT_1:def 3,A47; A62: y >= w by A47,A50,Th16; A63: 0-y <= z-w <= y-0 by A40,A62,XREAL_1:13; y +0 < y+y & -y-y < -y -0 by A49,XREAL_1:6,XREAL_1:15; then A64: (-1)*(2*y) < z-w < 1*(2*y) by A63,XXREAL_0:2; A65: 0+0 <= z+w <= y+y by A40,A62,XREAL_1:7; per cases by A60,A55,Th36,A47; suppose v,w are_congruent_mod 2*u; then consider t be Integer such that A66: v-w = (2*u)*t by INT_1:def 5; v-w = (2*y)*(t*r) by A66,A61; then v,w are_congruent_mod 2*y by INT_1:def 5; then consider i be Integer such that A67: z-w = (2*y)*i by INT_1:def 5,A59,INT_1:15; -1 < i <0+ 1 by A67,A64,XREAL_1:64; then -1+1<= i & i <= 0 by INT_1:7; then z-w=0 by A67; hence y = Py(a,z) & a > 1 by A36,A50; end; suppose v,-w are_congruent_mod 2*u; then consider t be Integer such that A68: v--w = (2*u)*t by INT_1:def 5; v--w = (2*y)*(t*r) by A61,A68; then v,-w are_congruent_mod 2*y by INT_1:def 5; then consider i be Integer such that A69: z--w = (2*y)*i by INT_1:def 5,A59,INT_1:15; (2*y)* 0 <= (2*y)*i <= (2*y)*1 by A69,A65; then A70: 0 <= i <= 1 by A49,XREAL_1:68; i <1 or i=1 by A70,XXREAL_0:1; then A71: i = 0 or i=1 by A70,NAT_1:14; per cases by A71,A69; suppose z+w=0; then z=0=w; hence thesis by A36,A50; end; suppose A72: z+w = 2*y; A73: z=y proof assume z<>y; then z < y by A40,XXREAL_0:1; then z+w y; then w < y by A62,XXREAL_0:1; then z+w 0) or (x = 1 & y = 1 & z > 0) or (x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) & (0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2)) proof let x,y,z be Nat; thus y = x|^z implies ( y = 1 & z = 0) or (x = 0 & y = 0 & z > 0) or (x = 1 & y = 1 & z > 0) or (x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) & (0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2)) proof assume A1: y=x|^z; per cases; suppose z=0; hence thesis by A1,NEWTON:4; end; suppose A2: z>0; per cases by NAT_1:53; suppose x=0 or x=1; hence thesis by A1,A2,NAT_1:14,NEWTON:11; end; suppose A3: x>1; then reconsider x1=x as non trivial Nat by NAT_2:28; ex y1,y2,y3,K be Nat st y1 = Py(x1,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x1,z+1) & (0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2) proof set y1 = Py(x1,z+1),K=2*z*y1+1,y2=Py(K,z+1), y3 = Py(K*x1,z+1); reconsider K as non trivial Nat by A2; take y1,y2,y3,K; x1+(x1-1) > x1+0 by XREAL_1:6; then A4: (x1+(x1-1)) to_power z > x1 to_power z by A2,POWER:37; (2*x1-1)|^z <=y1 by Th20; then y1 >= x1|^z by A4,XXREAL_0:2; then K > 2*z*(x1|^z) by NAT_1:13,XREAL_1:64; then A5: y - 1/2 < y3/y2 < y + 1/2 by A1,Th22; y-y3/y2 >=0 or -(y-y3/y2)>= -0; hence thesis by NAT_1:13,XREAL_1:19,XREAL_1:11,A5; end; hence thesis by A3,A2; end; end; end; assume A6: (y = 1 & z = 0) or (x = 0 & y = 0 & z > 0) or (x = 1 & y = 1 & z > 0) or (x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) & (0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2)); per cases by A6; suppose y=1 & z=0; hence thesis by NEWTON:4; end; suppose x = 0 & y = 0 & z > 0; hence thesis by NAT_1:14,NEWTON:11; end; suppose x = 1 & y = 1 & z > 0; hence thesis; end; suppose A7: x > 1 & z > 0 & ex y1,y2,y3,K be Nat st y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) & (0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2); reconsider x1=x as non trivial Nat by A7,NAT_2:28; consider y1,y2,y3,K be Nat such that A8: y1 = Py(x1,z+1) and A9: K > 2*z*y1 and A10: y2 = Py(K,z+1) and A11: y3 = Py(K*x1,z+1) and A12: 0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2 by A7; 2*z*y1 >=1 by NAT_1:14,A8,A7; then reconsider K as non trivial Nat by NAT_2:28,A9; x1+(x1-1) > x1+0 by XREAL_1:6; then A13: (x1+(x1-1)) to_power z > x1 to_power z by A7,POWER:37; (2*x1-1)|^z <=y1 by A8,Th20; then y1 >= x1|^z by A13,XXREAL_0:2; then y1*(2*z) >= (x1|^z)*(2*z) by XREAL_1:64; then K > 2*z*(x1|^z) by A9,XXREAL_0:2; then A14: x1|^z - 1/2 < y3/y2 < x1|^z + 1/2 by Th22,A10,A11; per cases by A12; suppose 0 <= y-y3/y2 <1/2; then A15: x1|^z - 1/2+0 < y-y3/y2+y3/y2< 1/2+(x1|^z + 1/2) by A14,XREAL_1:8; then y < (x1|^z)+1; then A16: y <= x1|^z by INT_1:7; x1|^z - 1 < x1|^z - 1/2 by XREAL_1:10; then x1|^z -1 < y by A15,XXREAL_0:2; then x1|^z-1+1 <=y by INT_1:7; hence thesis by A16,XXREAL_0:1; end; suppose 0 <= y3/y2 -y < 1/2; then A17: x1|^z - 1/2 -1/2 < y3/y2 -(y3/y2 -y) < x1|^z + 1/2 -0 by A14,XREAL_1:14; then A18: x1|^z -1+1 <= y by INT_1:7; x1|^z +1/2 < x1|^z +1 by XREAL_1:6; then y < x1|^z +1 by A17,XXREAL_0:2; then y <= x1|^z by INT_1:7; hence thesis by A18,XXREAL_0:1; end; end; end;