:: Simple Continued Fractions and Their Convergents
::  by Bo Li , Yan Zhang and Artur Korni{\l}owicz
::
:: Received August 18, 2006
:: Copyright (c) 2006-2012 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, NAT_1, INT_1, XREAL_0, ORDINAL1, RAT_1, XCMPLX_0,
      FUNCT_1, XXREAL_0, ARYTM_1, ARYTM_3, CARD_1, RELAT_1, SUBSET_1, SEQ_1,
      FUNCOP_1, TARSKI, IRRAT_1, REAL_1, INT_2, FIB_NUM, NEWTON, SQUARE_1,
      COMPLEX1, POWER, VALUED_1, REAL_3;
 notations TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, VALUED_0, XCMPLX_0,
      COMPLEX1, REAL_1, XXREAL_0, XREAL_0, RAT_1, SQUARE_1, INT_1, NAT_1,
      NAT_D, RELAT_1, RELSET_1, FUNCOP_1, VALUED_1, SEQ_1, FUNCT_2, NEWTON,
      FIB_NUM, POWER, IRRAT_1;
 constructors REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_1, NEWTON, POWER, BINARITH,
      FIB_NUM, VALUED_1, PARTFUN1, RELSET_1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
      SQUARE_1, NAT_1, INT_1, RAT_1, MEMBERED, NEWTON, VALUED_0, VALUED_1,
      FUNCT_2;
 requirements BOOLE, REAL, SUBSET, NUMERALS, ARITHM;
 definitions TARSKI, VALUED_1, SQUARE_1, FUNCT_2, INT_1, VALUED_0, XCMPLX_0;
 theorems INT_1, XREAL_0, ORDINAL1, XCMPLX_0, FUNCT_2, XCMPLX_1, FUNCT_1,
      NAT_1, RAT_1, NAT_2, FUNCOP_1, XREAL_1, NEWTON, SEQ_1, TARSKI, ABSVALUE,
      COMPLEX1, PREPOWER, WSIERP_1, SQUARE_1, EULER_1, FIB_NUM, POWER,
      SERIES_1, XXREAL_0, NAT_D, VALUED_1, RELSET_1, RELAT_1;
 schemes NAT_1, RECDEF_1, RECDEF_2, FIB_NUM, FUNCT_2;

begin :: Preliminaries

reserve a, b, k, n, m for Nat,
  i for Integer,
  r for real number,
  p for rational number,
  c for complex number,
  x for set,
  f for Function;

Lm1: now
  let n;
  assume n > 1;
  then n-1 > 1-1 by XREAL_1:14;
  then n-1 in NAT by INT_1:3;
  hence n-1 is Nat;
end;

Lm2: for a,b,c,d being real number st a/b-c <> 0 & d <> 0 & b <> 0 & a = b*c +
d holds 1 / (a/b-c) = b/d
proof
  let a,b,c,d be real number;
  assume that
A1: a/b-c <> 0 & d <> 0 and
A2: b <> 0;
  assume a = b*c + d;
  then d = b*((a - b*c)/b) by A2,XCMPLX_1:87
    .= b*(a/b - b*c/b);
  then 1*d = b*(a/b-c) by A2,XCMPLX_1:89;
  hence thesis by A1,XCMPLX_1:94;
end;

registration
  let n;
  cluster n div 0 -> zero;
  coherence by NAT_D:def 1;
  cluster n mod 0 -> zero;
  coherence by NAT_D:def 2;
  cluster 0 div n -> zero;
  coherence by NAT_2:2;
  cluster 0 mod n -> zero;
  coherence by NAT_D:26;
end;

registration
  let c;
  cluster c-c -> zero;
  coherence by XCMPLX_1:14;
  cluster c/0 -> zero;
  coherence;
end;

registration
  cluster [\ 0 /] -> zero;
  coherence by INT_1:25;
end;

theorem Th1:
  0 < r & r < 1 implies 1 < 1/r
proof
  assume that
A1: 0 < r and
A2: r < 1;
  1*r" > r*r" by A1,A2,XREAL_1:68;
  hence thesis by A1,XCMPLX_0:def 7;
end;

theorem Th2:
  i <= r & r < i+1 implies [\ r /] = i
proof
  assume
A1: i <= r;
  assume r < i+1;
  then r - 1 < i+1 - 1 by XREAL_1:14;
  hence thesis by A1,INT_1:def 6;
end;

theorem
  [\ m/n /] = m div n;

theorem Th4:
  m mod n = 0 implies m / n = m div n
proof
  reconsider i = m as Integer;
  assume
A1: m mod n = 0;
  per cases;
  suppose
A2: n = 0;
    hence m / n = 0 .= m div n by A2;
  end;
  suppose
A3: n <> 0;
    then i - (i div n) * n = 0 by A1,INT_1:def 10;
    hence thesis by A3,XCMPLX_1:89;
  end;
end;

theorem Th5:
  m / n = m div n implies m mod n = 0
proof
  assume
A1: m / n = m div n;
  per cases;
  suppose
    n = 0;
    hence thesis;
  end;
  suppose
A2: n > 0;
    then m + 0 = n * (m/n) + (m mod n) by A1,NAT_D:2;
    then m mod n - 0 = m - n * (m/n);
    hence m mod n = m - m by A2,XCMPLX_1:87
      .= 0;
  end;
end;

theorem Th6:
  frac(m/n) = (m mod n) / n
proof
  per cases;
  suppose
A1: n = 0;
    hence frac(m/n) = frac(0) .= (m mod n) / n by A1;
  end;
  suppose
A2: n > 0;
    then m = n * (m div n) + (m mod n) by NAT_D:2;
    then m/n + 0 = (m div n) + (m mod n) / n by A2,XCMPLX_1:113;
    hence thesis;
  end;
end;

theorem Th7:
  p >= 0 implies ex m,n being Nat st n <> 0 & p = m/n
proof
  consider m being Integer, k being Element of NAT such that
A1: k <> 0 & p = m/k by RAT_1:8;
  assume p >= 0;
  then k>0 & m>=0 or k<0 & m<=0 by A1,XREAL_1:141;
  then reconsider m as Element of NAT by INT_1:3;
  take m,k;
  thus thesis by A1;
end;

registration
  cluster INT-valued for Real_Sequence;
  existence
  proof
    set s = NAT --> 1;
    dom s = NAT & for n being Element of NAT holds s.n is real by FUNCOP_1:13;
    then reconsider s as Real_Sequence by SEQ_1:2;
    take s;
    thus thesis;
  end;
end;

definition
  mode Integer_Sequence is INT-valued Real_Sequence;
end;

theorem Th8:
  f is Integer_Sequence iff dom f=NAT & for x st x in NAT holds f.x is integer
proof
  thus f is Integer_Sequence implies dom f=NAT & for x st x in NAT holds f.x
  is integer by SEQ_1:1;
  assume that
A1: dom f= NAT and
A2: for x st x in NAT holds f.x is integer;
  now
    let y be set;
    assume y in rng f;
    then consider x such that
A3: x in dom f and
A4: y=f.x by FUNCT_1:def 3;
    f.x is integer by A1,A2,A3;
    hence y in INT by A4,INT_1:def 2;
  end;
  then
A5: rng f c=INT by TARSKI:def 3;
  for x st x in NAT holds f.x is real
  proof
    let x;
    assume x in NAT;
    then f.x is integer by A2;
    hence thesis;
  end;
  hence thesis by A1,A5,SEQ_1:1,RELAT_1:def 19;
end;

theorem Th9:
  f is Function of NAT,INT iff f is Integer_Sequence
proof
  hereby
    assume f is Function of NAT,INT;
    then reconsider g = f as Function of NAT,INT;
    dom g = NAT & for x st x in NAT holds g.x is integer by FUNCT_2:def 1;
    hence f is Integer_Sequence by Th8;
  end;
  assume f is Integer_Sequence;
  then dom f = NAT & rng f c= INT by FUNCT_2:def 1,RELAT_1:def 19;
  hence thesis by FUNCT_2:2;
end;

theorem
  f is sequence of NAT iff dom f=NAT & for x st x in NAT holds f.x is natural
proof
  thus f is sequence of NAT implies dom f=NAT & for x st x in NAT holds f.x is
  natural by FUNCT_2:def 1;
  assume that
A1: dom f= NAT and
A2: for x st x in NAT holds f.x is natural;
  rng f c= NAT
  proof
    let x;
    assume x in rng f;
    then ex y being set st y in NAT & x = f.y by A1,FUNCT_1:def 3;
    then x is natural by A2;
    hence thesis by ORDINAL1:def 12;
  end;
  hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;

theorem
  f is Function of NAT,NAT iff f is sequence of NAT;

begin :: On the Euclidean algorithm

definition
  deffunc F(Nat,Element of NAT,Element of NAT) = $2 mod $3;

  let m, n be Nat;
  set a = m mod n;
  set b = n mod (m mod n);
  func modSeq(m,n) -> sequence of NAT means
  :Def1:
  it.0 = m mod n & it.1 = n
  mod (m mod n) & for k being Nat holds it.(k+2) = it.k mod it.(k+1);
  existence
  proof
    consider f being Function of NAT,NAT such that
A1: f.0 = a & f.1 = b and
A2: for n being Element of NAT holds f.(n+2) = F(n,(f.n) qua Element
    of NAT,(f.(n+1)) qua Element of NAT) from RECDEF_2:sch 5;
    reconsider f as sequence of NAT;
    take f;
    thus f.0 = a & f.1 = b by A1;
    let k be Nat;
    k in NAT by ORDINAL1:def 12;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let f,g be sequence of NAT such that
A3: f.0 = a & f.1 = b and
A4: for n being Nat holds f.(n+2) = f.n mod f.(n+1) and
A5: g.0 = a & g.1 = b and
A6: for n being Nat holds g.(n+2) = g.n mod g.(n+1);
    reconsider f, g as Function of NAT,NAT;
A7: g.0 = a & g.1 = b by A5;
A8: for n being Element of NAT holds g.(n+2) = F(n,(g.n) qua Element of
    NAT,(g.(n+1)) qua Element of NAT) by A6;
A9: for n being Element of NAT holds f.(n+2) = F(n,(f.n) qua Element of
    NAT,(f.(n+1)) qua Element of NAT) by A4;
A10: f.0 = a & f.1 = b by A3;
    f = g from RECDEF_2:sch 7(A10,A9,A7,A8);
    hence thesis;
  end;
end;

definition
  let m, n be Nat;
  set a = m div n;
  set b = n div (m mod n);
  deffunc F(Nat,Element of NAT,Element of NAT) = modSeq(m,n).$1 div modSeq(m,n
  ).($1+1);
  func divSeq(m,n) -> sequence of NAT means
  :Def2:
  it.0 = m div n & it.1 = n
div (m mod n) & for k being Nat holds it.(k+2) = modSeq(m,n).k div modSeq(m,n).
  (k+1);
  existence
  proof
    consider f being Function of NAT,NAT such that
A1: f.0 = a & f.1 = b and
A2: for n being Element of NAT holds f.(n+2) = F(n,(f.n) qua Element
    of NAT,(f.(n+1)) qua Element of NAT) from RECDEF_2:sch 5;
    reconsider f as sequence of NAT;
    take f;
    thus f.0 = a & f.1 = b by A1;
    let k be Nat;
    k in NAT by ORDINAL1:def 12;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let f,g be sequence of NAT such that
A3: f.0 = a & f.1 = b and
A4: for k being Nat holds f.(k+2) = modSeq(m,n).k div modSeq(m,n).(k+1 ) and
A5: g.0 = a & g.1 = b and
A6: for k being Nat holds g.(k+2) = modSeq(m,n).k div modSeq(m,n).(k+1 );
    reconsider f, g as Function of NAT,NAT;
A7: g.0 = a & g.1 = b by A5;
A8: for n being Element of NAT holds g.(n+2) = F(n,(g.n) qua Element of
    NAT,(g.(n+1)) qua Element of NAT) by A6;
A9: for n being Element of NAT holds f.(n+2) = F(n,(f.n) qua Element of
    NAT,(f.(n+1)) qua Element of NAT) by A4;
A10: f.0 = a & f.1 = b by A3;
    f = g from RECDEF_2:sch 7(A10,A9,A7,A8);
    hence thesis;
  end;
end;

theorem Th12:
  divSeq(m,n).1 = n div modSeq(m,n).0
proof
  thus divSeq(m,n).1 = n div (m mod n) by Def2
    .= n div modSeq(m,n).0 by Def1;
end;

theorem Th13:
  modSeq(m,n).1 = n mod modSeq(m,n).0
proof
  thus modSeq(m,n).1 = n mod (m mod n) by Def1
    .= n mod modSeq(m,n).0 by Def1;
end;

theorem Th14:
  a <= b & modSeq(m,n).a = 0 implies modSeq(m,n).b = 0
proof
  set fm = modSeq(m,n);
  assume that
A1: a <= b and
A2: fm.a = 0;
A3: a < b or a = b by A1,XXREAL_0:1;
  defpred P[Nat] means a < $1 implies fm.$1 = 0;
A4: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A5: P[k];
    assume
A6: a < k+1;
    then
A7: a <= k by NAT_1:13;
    per cases by NAT_1:25;
    suppose
A8:   k = 0;
      then
A9:   a = 0 by A6,NAT_1:13;
      thus fm.(k+1) = n mod fm.0 by A8,Th13
        .= 0 by A2,A9;
    end;
    suppose
A10:  k = 1;
      then
A11:  a = 0 or a = 1 by A7,NAT_1:25;
      2 = 2+0;
      hence fm.(k+1) = fm.0 mod fm.(0+1) by A10,Def1
        .= 0 by A2,A11;
    end;
    suppose
      k > 1;
      then reconsider k1 = k-1 as Nat by Lm1;
      per cases by A7,XXREAL_0:1;
      suppose
A12:    a = k;
        thus fm.(k+1) = fm.(k1+2) .= fm.k1 mod fm.(k1+1) by Def1
          .= 0 by A2,A12;
      end;
      suppose
A13:    a < k;
        thus fm.(k+1) = fm.(k1+2) .= fm.k1 mod fm.(k1+1) by Def1
          .= 0 by A5,A13;
      end;
    end;
  end;
A14: P[0];
  for k being Nat holds P[k] from NAT_1:sch 2(A14,A4);
  hence thesis by A2,A3;
end;

Lm3: modSeq(m,n).a > modSeq(m,n).(a+1) or modSeq(m,n).a = 0
proof
  set fm = modSeq(m,n);
    per cases by NAT_1:25;
    suppose
A1:   a = 0;
      fm.(0+1) = n mod (m mod n) & fm.0 = m mod n by Def1;
      hence thesis by A1,NAT_D:1;
    end;
    suppose
A2:   a = 1;
      fm.(0+2) = fm.0 mod fm.(0+1) by Def1;
      hence thesis by A2,NAT_D:1;
    end;
    suppose
      a > 1;
      then reconsider a1 = a-1 as Nat by Lm1;
      fm.(a+1) = fm.(a1+(1+1)) .= fm.a1 mod fm.(a1+1) by Def1;
      hence thesis by NAT_D:1;
    end;
end;

theorem Th15:
  a < b implies modSeq(m,n).a > modSeq(m,n).b or modSeq(m,n).a = 0
proof
  set fm = modSeq(m,n);
  assume
A1: a < b;
  per cases;
  suppose
    fm.a = 0;
    hence thesis;
  end;
  suppose
A2: fm.a > 0;
    defpred P[Nat] means a < $1 implies fm.a > fm.$1;
A3: for x being Nat st P[x] holds P[x+1]
    proof
      let x be Nat such that
A4:   P[x];
      assume a < x+1;
      then
A5:   a <= x by NAT_1:13;
      per cases by A5,XXREAL_0:1;
      suppose
        a = x;
        hence fm.a > fm.(x+1) by A2,Lm3;
      end;
      suppose
A6:     a < x;
        thus fm.a > fm.(x+1)
        proof
          per cases by Lm3;
          suppose
            fm.x > fm.(x+1);
            hence thesis by A4,A6,XXREAL_0:2;
          end;
          suppose
            fm.x = 0;
            hence thesis by A2,Th14,NAT_1:11;
          end;
        end;
      end;
    end;
A7: P[0];
    for x being Nat holds P[x] from NAT_1:sch 2(A7,A3);
    hence thesis by A1;
  end;
end;

theorem Th16:
  divSeq(m,n).(a+1) = 0 implies modSeq(m,n).a = 0
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  defpred P[Nat] means fd.($1+1) = 0 implies fm.$1 = 0;
A1: P[b] implies P[b+1]
  proof
    assume P[b];
    set x = fm.(b+1);
    assume fd.(b+1+1) = 0;
    then fd.(b+(1+1)) = 0;
    then
A2: fm.b div fm.(b+1) = 0 by Def2;
    assume
A3: fm.(b+1) <> 0;
    then fm.b = x * (fm.b div x) + (fm.b mod x) by NAT_D:2;
    then
A4: fm.b < x by A2,A3,NAT_D:1;
A5: b+0 < b+1 by XREAL_1:6;
    then fm.b <> 0 by A3,Th14;
    hence thesis by A4,A5,Th15;
  end;
A6: P[0]
  proof
    set x = m mod n;
    assume fd.(0+1) = 0;
    then
A7: n div fm.0 = 0 by Th12;
    assume
A8: fm.0 <> 0;
    then m mod n <> 0 by Def1;
    then
A9: n <> 0;
A10: fm.0 = x by Def1;
    then n = x * (n div x) + (n mod x) by A8,NAT_D:2;
    then n < x by A7,A10,A8,NAT_D:1;
    hence thesis by A9,NAT_D:1;
  end;
  P[b] from NAT_1:sch 2(A6,A1);
  hence thesis;
end;

Lm4: modSeq(m,n).a = 0 implies divSeq(m,n).(a+1) = 0
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  defpred P[Nat] means fm.$1 = 0 implies fd.($1+1) = 0;
A1: P[b] implies P[b+1]
  proof
    assume that
    P[b] and
A2: fm.(b+1) = 0;
    thus fd.(b+1+1) = fd.(b+(1+1)) .= fm.b div fm.(b+1) by Def2
      .= 0 by A2;
  end;
A3: P[0]
  proof
    assume
A4: fm.0 = 0;
    thus fd.(0+1) = n div fm.0 by Th12
      .= 0 by A4;
  end;
  P[b] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem Th17:
  a <> 0 & a <= b & divSeq(m,n).a = 0 implies divSeq(m,n).b = 0
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  assume that
A1: a <> 0 and
A2: a <= b and
A3: fd.a = 0;
A4: a < b or a = b by A2,XXREAL_0:1;
  defpred P[Nat] means a < $1 implies fd.$1 = 0 & fm.$1 = 0;
A5: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A6: P[k];
    assume
A7: a < k+1;
    then
A8: a <= k by NAT_1:13;
    per cases by NAT_1:25;
    suppose
      k = 0;
      hence thesis by A1,A7,NAT_1:13;
    end;
    suppose
A9:   k = 1;
      then fd.(0+1) = 0 by A1,A3,A8,NAT_1:25;
      then
A10:  fm.0 = 0 by Th16;
A11:  2 = 2+0;
      hence fd.(k+1) = fm.0 div fm.(0+1) by A9,Def2
        .= 0 by A10;
      thus fm.(k+1) = fm.0 mod fm.(0+1) by A9,A11,Def1
        .= 0 by A10;
    end;
    suppose
      k > 1;
      then reconsider k1 = k-1 as Nat by Lm1;
A12:  k = k1+1;
      per cases by A8,XXREAL_0:1;
      suppose
        a = k;
        then
A13:    fm.k1 = 0 by A3,A12,Th16;
        thus fd.(k+1) = fd.(k1+2) .= fm.k1 div fm.(k1+1) by Def2
          .= 0 by A13;
        thus fm.(k+1) = fm.(k1+2) .= fm.k1 mod fm.(k1+1) by Def1
          .= 0 by A13;
      end;
      suppose
A14:    a < k;
        thus fd.(k+1) = fd.(k1+2) .= fm.k1 div fm.(k1+1) by Def2
          .= 0 by A6,A14;
        thus fm.(k+1) = fm.(k1+2) .= fm.k1 mod fm.(k1+1) by Def1
          .= 0 by A6,A14;
      end;
    end;
  end;
A15: P[0];
  for k being Nat holds P[k] from NAT_1:sch 2(A15,A5);
  hence thesis by A3,A4;
end;

theorem Th18:
  a < b & modSeq(m,n).a = 0 implies divSeq(m,n).b = 0
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  assume a < b;
  then
A1: a+1 <= b by NAT_1:13;
  assume fm.a = 0;
  then fd.(a+1) = 0 by Lm4;
  hence thesis by A1,Th17;
end;

theorem Th19:
  n <> 0 implies m = divSeq(m,n).0 * n + modSeq(m,n).0
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  assume
A1: n <> 0;
  fd.0 = m div n & fm.0 = m mod n by Def1,Def2;
  hence thesis by A1,NAT_D:2;
end;

theorem
  n <> 0 implies m / n = divSeq(m,n).0 + 1 / (n / modSeq(m,n).0)
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  assume
A1: n <> 0;
  hence m/n = (fd.0 * n + fm.0)/n by Th19
    .= fm.0 / n + fd.0 by A1,XCMPLX_1:113
    .= fd.0 + 1 / (n / fm.0) by XCMPLX_1:57;
end;

set g = NAT --> 0;

Lm5: dom g = NAT by FUNCOP_1:13;

theorem Th21:
  divSeq(m,0) = NAT --> 0
proof
  set g = NAT --> 0;
  set fd = divSeq(m,0);
A1: for x being set st x in dom fd holds fd.x = g.x
  proof
    defpred P[Nat] means fd.$1 = 0;
    let x be set;
    assume x in dom fd;
    then reconsider x as Element of NAT;
A2: for n being Nat holds P[n] implies P[n+1]
    proof
      let n be Nat;
      assume
A3:   P[n];
      per cases;
      suppose
A4:     n = 0;
        fd.1 = 0 div (m mod 0) by Def2
          .= 0;
        hence thesis by A4;
      end;
      suppose
        0 <> n;
        hence thesis by A3,Th17,NAT_1:11;
      end;
    end;
    fd.0 = m div 0 by Def2
      .= 0;
    then
A5: P[0];
    for n being Nat holds P[n] from NAT_1:sch 2(A5,A2);
    then fd.x = 0;
    hence thesis by FUNCOP_1:7;
  end;
  dom fd = NAT by FUNCT_2:def 1;
  hence thesis by A1,Lm5,FUNCT_1:2;
end;

theorem Th22:
  modSeq(m,0) = NAT --> 0
proof
  set fm = modSeq(m,0);
A1: for x being set st x in dom fm holds fm.x = g.x
  proof
    defpred P[Nat] means fm.$1 = 0;
    let x be set;
    assume x in dom fm;
    then reconsider x as Element of NAT;
    fm.0 = m mod 0 by Def1
      .= 0;
    then
A2: P[0];
A3: for n being Nat holds P[n] implies P[n+1] by Th14,NAT_1:11;
    for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
    then fm.x = 0;
    hence thesis by FUNCOP_1:7;
  end;
  dom fm = NAT by FUNCT_2:def 1;
  hence thesis by A1,Lm5,FUNCT_1:2;
end;

theorem
  divSeq(0,n) = NAT --> 0
proof
  set fd = divSeq(0,n);
A1: for x being set st x in dom fd holds fd.x = g.x
  proof
    defpred P[Nat] means fd.$1 = 0;
    let x be set;
    assume x in dom fd;
    then reconsider x as Element of NAT;
A2: for x being Nat holds P[x] implies P[x+1]
    proof
      let x be Nat;
      assume
A3:   P[x];
      per cases;
      suppose
A4:     x = 0;
        fd.1 = n div (0 mod n) by Def2
          .= n div 0;
        hence thesis by A4;
      end;
      suppose
        0 <> x;
        hence thesis by A3,Th17,NAT_1:11;
      end;
    end;
    fd.0 = 0 div n by Def2
      .= 0;
    then
A5: P[0];
    for n being Nat holds P[n] from NAT_1:sch 2(A5,A2);
    then fd.x = 0;
    hence thesis by FUNCOP_1:7;
  end;
  dom fd = NAT by FUNCT_2:def 1;
  hence thesis by A1,Lm5,FUNCT_1:2;
end;

theorem
  modSeq(0,n) = NAT --> 0
proof
  set fm = modSeq(0,n);
A1: for x being set st x in dom fm holds fm.x = g.x
  proof
    defpred P[Nat] means fm.$1 = 0;
    let x be set;
    assume x in dom fm;
    then reconsider x as Element of NAT;
    fm.0 = 0 mod n by Def1
      .= 0;
    then
A2: P[0];
A3: for x being Nat holds P[x] implies P[x+1] by Th14,NAT_1:11;
    for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
    then fm.x = 0;
    hence thesis by FUNCOP_1:7;
  end;
  dom fm = NAT by FUNCT_2:def 1;
  hence thesis by A1,Lm5,FUNCT_1:2;
end;

Lm6: ex k st modSeq(m,n).k = 0
proof
  set f = modSeq(m,n);
  defpred P[Nat] means ex k st f.k = $1;
A1: for a being Nat st a <> 0 & P[a] ex w being Nat st w < a & P[w]
  proof
    let a be Nat such that
A2: a <> 0;
    given k such that
A3: f.k = a;
    take w = f.(k+1);
    k+0 < k+1 by XREAL_1:6;
    hence w < a by A2,A3,Th15;
    thus thesis;
  end;
A4: ex a being Nat st P[a]
  proof
    take f.0, 0;
    thus thesis;
  end;
  thus P[0] from NAT_1:sch 7(A4,A1);
end;

theorem Th25:
  ex k being Nat st divSeq(m,n).k = 0 & modSeq(m,n).k = 0
proof
  set f = modSeq(m,n);
  consider k such that
A1: f.k = 0 by Lm6;
  take k+1;
A2: k+0 < k+1 by XREAL_1:6;
  hence divSeq(m,n).(k+1) = 0 by A1,Th18;
  thus f.(k+1) = 0 by A1,A2,Th14;
end;

begin :: Simple continued fractions

defpred P[set,Element of REAL,set] means $3 = 1 / frac($2);

definition
  let r be real number;
  func remainders_for_scf r -> Real_Sequence means
  :Def3:
  it.0 = r & for n being Nat holds it.(n+1) = 1 / frac(it.n);
  existence
  proof
    reconsider r1 = r as Element of REAL by XREAL_0:def 1;
A1: for n being Element of NAT for x being Element of REAL ex y being
    Element of REAL st P[n,x,y];
    consider f being Function of NAT,REAL such that
A2: f.0 = r1 and
A3: for n being Element of NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:
    sch 2( A1);
    take f;
    thus f.0 = r by A2;
    let n;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A3;
  end;
  uniqueness
  proof
A4: for n being Nat,x,y1,y2 being Element of REAL st P[n,x,y1] & P[n,x,y2]
    holds y1=y2;
    reconsider r1 = r as Element of REAL by XREAL_0:def 1;
    let g1, g2 be Real_Sequence such that
A5: g1.0 = r and
A6: for n being Nat holds g1.(n+1) = 1/frac(g1.n) and
A7: g2.0 = r and
A8: for n being Nat holds g2.(n+1) = 1/frac(g2.n);
A9: for n being Nat holds P[n,g1.n,g1.(n+1)] by A6;
A10: for n being Nat holds P[n,g2.n,g2.(n+1)] by A8;
A11: g2.0 = r1 by A7;
A12: g1.0 = r1 by A5;
    thus g1 = g2 from NAT_1:sch 14(A12,A9,A11,A10,A4);
  end;
end;

notation
  let r be real number;
  synonym rfs r for remainders_for_scf r;
end;

definition
  let r be real number;
  func SimpleContinuedFraction r -> Integer_Sequence means
  :Def4:
  for n being Nat holds it.n = [\ rfs(r).n /];
  existence
  proof
    defpred P[set,set] means $2 = [\ rfs(r).$1 /];
A1: for x being Element of NAT ex y being Element of INT st P[x,y]
    proof
      let x be Element of NAT;
      reconsider y = [\ rfs(r).x /] as Element of INT by INT_1:def 2;
      take y;
      thus thesis;
    end;
    consider f being Function of NAT,INT such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
    reconsider f as Integer_Sequence by Th9;
    take f;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let f1, f2 be Integer_Sequence such that
A3: for n being Nat holds f1.n = [\ rfs(r).n /] and
A4: for n being Nat holds f2.n = [\ rfs(r).n /];
    let n be Element of NAT;
    thus f1.n = [\ rfs(r).n /] by A3
      .= f2.n by A4;
  end;
end;

notation
  let r be real number;
  synonym scf r for SimpleContinuedFraction r;
end;

theorem Th26:
  rfs(r).(n+1) = 1 / (rfs(r).n-scf(r).n)
proof
  thus rfs(r).(n+1) = 1/frac(rfs(r).n) by Def3
    .= 1/(rfs(r).n-scf(r).n) by Def4;
end;

theorem Th27:
  rfs(r).n = 0 & n <= m implies rfs(r).m = 0
proof
  assume that
A1: rfs(r).n = 0 and
A2: n <= m;
  per cases by A2,XXREAL_0:1;
  suppose
    n = m;
    hence thesis by A1;
  end;
  suppose
A3: n < m;
    defpred P[Nat] means n < $1 implies rfs(r).$1 = 0;
A4: for a being Nat st P[a] holds P[a+1]
    proof
      let a be Nat;
      assume
A5:   P[a];
      assume n < a+1;
      then
A6:   n <= a by NAT_1:13;
      per cases by A6,XXREAL_0:1;
      suppose
A7:     n = a;
        thus rfs(r).(a+1) = 1 / frac(rfs(r).a) by Def3
          .= 1 / (rfs(r).a - rfs(r).a) by A1,A7
          .= 0;
      end;
      suppose
A8:     n < a;
        thus rfs(r).(a+1) = 1 / frac(rfs(r).a) by Def3
          .= 1 / (rfs(r).a - rfs(r).a) by A5,A8
          .= 0;
      end;
    end;
A9: P[0];
    for a being Nat holds P[a] from NAT_1:sch 2(A9,A4);
    hence thesis by A3;
  end;
end;

theorem
  rfs(r).n = 0 & n <= m implies scf(r).m = 0
proof
  assume
A1: rfs(r).n = 0 & n <= m;
  thus scf(r).m = [\rfs(r).m/] by Def4
    .= [\0/] by A1,Th27
    .= 0;
end;

theorem Th29:
  rfs(i).(n+1) = 0
proof
  defpred P[Nat] means rfs(i).($1+1) = 0;
A1: rfs(i).0 = i by Def3;
A2: for n st P[n] holds P[n+1]
  proof
    let n such that
A3: P[n];
    thus rfs(i).(n+1+1) = 1 / frac(rfs(i).(n+1)) by Def3
      .= 1/(0-0) by A3
      .= 0;
  end;
  rfs(i).(0+1) = 1 / frac(rfs(i).0) by Def3
    .= 1/(i-i) by A1,INT_1:25
    .= 0;
  then
A4: P[0];
  for n holds P[n] from NAT_1:sch 2(A4,A2);
  hence thesis;
end;

theorem Th30:
  scf(i).0 = i & scf(i).(n+1) = 0
proof
  defpred P[Nat] means rfs(i).($1+1) = 0 & scf(i).($1+1) = 0;
  thus scf(i).0 = [\ rfs(i).0 /] by Def4
    .= [\ i /] by Def3
    .= i by INT_1:25;
A1: for n st P[n] holds P[n+1]
  proof
    let n such that
A2: P[n];
    thus rfs(i).(n+1+1) = 1 / frac(rfs(i).(n+1)) by Def3
      .= 1 / (0 - 0) by A2
      .= 0;
    thus scf(i).(n+1+1) = [\ rfs(i).(n+1+1) /] by Def4
      .= [\ 0 /] by Th29
      .= 0;
  end;
  scf(i).(0+1) = [\ rfs(i).(0+1) /] by Def4
    .= [\ 0 /] by Th29
    .= 0;
  then
A3: P[0] by Th29;
  for n holds P[n] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

Lm7: i > 1 implies rfs(1/i).1 = i & rfs(1/i).(n+2) = 0 & scf(1/i).0 = 0 & scf(
1/i).1 = i & scf(1/i).(n+2) = 0
proof
  set r = 1/i;
  defpred P[Nat] means rfs(r).($1+2) = 0 & scf(r).($1+2) = 0;
  assume
A1: i > 1;
  then
A2: r < 0+1 by XREAL_1:189;
A3: [\rfs(r).0/] = [\r/] by Def3
    .= 0 by A1,A2,Th2;
  thus
A4: rfs(r).1 = rfs(r).(0+1) .= 1/frac(rfs(r).0) by Def3
    .= 1/(r-0) by A3,Def3
    .= i;
  then
A5: scf(r).1 = [\i/] by Def4;
A6: for n st P[n] holds P[n+1]
  proof
    let n such that
A7: P[n];
    thus rfs(r).(n+1+2) = rfs(r).(n+2+1) .= 1/frac(rfs(r).(n+2)) by Def3
      .= 1/(0-0) by A7
      .= 0;
    hence scf(r).(n+1+2) = [\0/] by Def4
      .= 0;
  end;
A8: rfs(r).(0+2) = rfs(r).(1+1) .= 1/frac(rfs(r).1) by Def3
    .= 1/(i-i) by A4,INT_1:25
    .= 0;
  then scf(r).(0+2) = [\0/] by Def4
    .= 0;
  then
A9: P[0] by A8;
A10: for n holds P[n] from NAT_1:sch 2(A9,A6);
  scf(r).0 = [\rfs(r).0/] by Def4
    .= [\r/] by Def3
    .= 0 by A1,A2,Th2;
  hence thesis by A5,A10,INT_1:25;
end;

theorem
  i > 1 implies rfs(1/i).1 = i & rfs(1/i).(n+2) = 0 by Lm7;

theorem
  i > 1 implies scf(1/i).0 = 0 & scf(1/i).1 = i & scf(1/i).(n+2) = 0 by Lm7;

theorem Th33:
  (for n holds scf(r).n = 0) implies rfs(r).n = 0
proof
  assume that
A1: for n holds scf(r).n = 0 and
A2: rfs(r).n <> 0;
A3: scf(r).n = 0 by A1;
  set x = rfs(r).n;
A4: scf(r).n = [\x/] by Def4;
  per cases by A2;
  suppose
    x < 0;
    hence thesis by A3,A4,INT_1:def 6;
  end;
  suppose
    x >= 1;
    hence thesis by A3,A4,INT_1:54;
  end;
  suppose
    0 < x & x < 1;
    then
A5: 1/x > 1 by Th1;
A6: scf(r).(n+1) = 0 & scf(r).(n+1) = [\ rfs(r).(n+1) /] by A1,Def4;
    rfs(r).(n+1) = 1 / frac(x) by Def3
      .= 1/(x-scf(r).n) by Def4
      .= 1/(x-0) by A1
      .= 1/x;
    hence thesis by A5,A6,INT_1:54;
  end;
end;

theorem Th34:
  (for n holds scf(r).n = 0) implies r = 0
proof
  assume for n holds scf(r).n = 0;
  then rfs(r).0 = 0 by Th33;
  hence thesis by Def3;
end;

Lm8: rfs(1 / (r - scf(r).0)).n = rfs(r).(n+1) & scf(1 / (r - scf(r).0)).n =
scf(r).(n+1)
proof
  set x = r - scf(r).0;
  defpred P[Nat] means rfs(1/x).$1 = rfs(r).($1+1) & scf(1/x).$1 = scf(r).($1+
  1);
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume P[n];
    hence rfs(1/x).(n+1) = 1/frac(rfs(r).(n+1)) by Def3
      .= rfs(r).(n+1+1) by Def3;
    hence scf(1/x).(n+1) = [\ rfs(r).(n+1+1) /] by Def4
      .= scf(r).(n+1+1) by Def4;
  end;
A2: rfs(1/x).0 = 1/x by Def3
    .= 1/(rfs(r).0-scf(r).0) by Def3
    .= 1/frac(rfs(r).0) by Def4
    .= rfs(r).(0+1) by Def3;
  then scf(1/x).0 = [\ rfs(r).1 /] by Def4
    .= scf(r).(0+1) by Def4;
  then
A3: P[0] by A2;
  for n holds P[n] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem Th35:
  frac(r) = r - scf(r).0
proof
  thus frac(r) = r - [\ rfs(r).0 /] by Def3
    .= r - scf(r).0 by Def4;
end;

theorem
  rfs(r).(n+1) = rfs(1/frac(r)).n
proof
  frac(r) = r - scf(r).0 by Th35;
  hence thesis by Lm8;
end;

theorem Th37:
  scf(r).(n+1) = scf(1/frac(r)).n
proof
  frac(r) = r - scf(r).0 by Th35;
  hence thesis by Lm8;
end;

theorem Th38:
  n >= 1 implies scf(r).n >= 0
proof
  defpred P[Nat] means scf(r).$1 >= 0;
  [\ r /] <= r by INT_1:def 6;
  then frac(r) >=0 by XREAL_1:48;
  then
A1: 1/frac(r) -1 >= 0 -1 by XREAL_1:9;
A2: for n being Nat st n>=1 holds P[n] implies P[n+1]
  proof
    let n be Nat;
    assume n>=1;
    [\ rfs(r).n /] <= rfs(r).n by INT_1:def 6;
    then frac(rfs(r).n) >=0 by XREAL_1:48;
    then
A3: 1/frac(rfs(r).n) -1 >= 0 -1 by XREAL_1:9;
    scf(r).(n+1) = [\ rfs(r).(n+1) /] by Def4
      .= [\ 1/frac(rfs(r).n) /] by Def3;
    then scf(r).(n+1) > 1/(rfs(r).n - [\ rfs(r).n /]) -1 by INT_1:def 6;
    then
    scf(r).(n+1) -(-1) > (1/frac(rfs(r).n) -1) - (1/frac(rfs(r).n) -1) by A3,
XREAL_1:14;
    hence thesis by INT_1:7;
  end;
  scf(r).1 = [\ rfs(r).(0+1) /] by Def4
    .= [\ 1/frac(rfs(r).0) /] by Def3
    .= [\ 1/frac(r) /] by Def3;
  then scf(r).1 > 1/frac(r) -1 by INT_1:def 6;
  then scf(r).1 -(-1) > (1/frac(r) -1) - (1/frac(r) -1) by A1,XREAL_1:14;
  then
A4: P[1] by INT_1:7;
  for n being Nat st n>=1 holds P[n] from NAT_1:sch 8(A4,A2);
  hence thesis;
end;

theorem
  n >= 1 implies scf(r).n in NAT by Th38,INT_1:3;

theorem Th40:
  n >= 1 & scf(r).n <> 0 implies scf(r).n >= 1
proof
  assume n>=1 & scf(r).n <>0;
  then scf(r).n>0 by Th38;
  then scf(r).n>=0+1 by INT_1:7;
  hence thesis;
end;

theorem Th41:
  scf(m/n).k = divSeq(m,n).k & rfs(m/n).1 = n / modSeq(m,n).0 &
  rfs(m/n).(k+2) = (modSeq(m,n).k) / (modSeq(m,n).(k+1))
proof
  set fd = divSeq(m,n);
  set fm = modSeq(m,n);
  set r = m/n;
A1: scf(r).0 = [\ rfs(r).0 /] by Def4
    .= m div n by Def3;
  per cases;
  suppose
A2: n = 0;
    then
A3: fm = NAT --> 0 by Th22;
A4: fd = NAT --> 0 by A2,Th21;
A5: k in NAT by ORDINAL1:def 12;
    k = 0 or ex x being Nat st k = x + 1 by NAT_1:6;
    hence scf(r).k = 0 by A2,Th30
      .= fd.k by A4,A5,FUNCOP_1:7;
    thus rfs(m/n).1 = rfs(r).(0+1) .= n / fm.0 by A2,Th29;
    thus rfs(m/n).(k+2) = rfs(r).(k+1+1) .= 0 / fm.(k+1) by A2,Th29
      .= fm.k / fm.(k+1) by A3,A5,FUNCOP_1:7;
  end;
  suppose
A6: 0 < n;
    then m = n * (m div n) + (m mod n) by NAT_D:2;
    then
A7: r = (m div n) + (m mod n) / n by A6,XCMPLX_1:113;
    defpred P[Nat] means (for i being Nat st i <= $1 holds scf(r).i = fd.i) &
    for i being Nat st i+1 <= $1 holds rfs(r).(i+2) = fm.i / fm.(i+1);
A8: rfs(r).(0+1) = 1/frac(rfs(r).0) by Def3
      .= 1/(rfs(r).0-scf(r).0) by Def4
      .= 1/(r-(m div n)) by A1,Def3
      .= n / (m mod n) by A7,XCMPLX_1:57
      .= n / fm.0 by Def1;
A9: P[0]
    proof
      hereby
        let i be Nat;
        assume i <= 0;
        then i = 0;
        hence scf(r).i = fd.i by A1,Def2;
      end;
      let i be Nat;
      assume i+1 <= 0;
      hence thesis;
    end;
A10: for a being Nat st P[a] holds P[a+1]
    proof
      let a be Nat such that
A11:  P[a];
      per cases;
      suppose
A12:    a = 0;
        set x = m mod n;
A13:    scf(r).(0+1) = scf(1/frac(r)).0 by Th37
          .= [\ rfs(1/frac(r)).0 /] by Def4
          .= [\ 1 / frac(r) /] by Def3
          .= [\ 1 / ((m mod n) / n )/] by Th6
          .= n div (m mod n) by XCMPLX_1:57
          .= n div fm.0 by Def1
          .= fd.1 by Th12;
        hereby
          let i be Nat;
          assume i <= a+1;
          then i = 0 or i = 1 by A12,NAT_1:25;
          hence scf(r).i = fd.i by A9,A13;
        end;
        let i be Nat;
        assume i+1 <= a+1;
        then
A14:    i+1 = 0 or i+1 = 0+1 by A12,NAT_1:25;
        per cases;
        suppose
A15:      x = 0;
          thus rfs(r).(i+2) = rfs(r).(1+1) by A14
            .= 1/frac(rfs(r).1) by Def3
            .= 1/(n/fm.0-fd.1) by A8,A13,Def4
            .= 1/(n/x-fd.1) by Def1
            .= 1/(n/x-(n div x)) by Def2
            .= 1 / (0 - (n div x)) by A15
            .= 1 / (0 - 0) by A15
            .= fm.i / 0
            .= fm.i / (n mod x) by A15
            .= fm.i / fm.(i+1) by A14,Def1;
        end;
        suppose
A16:      0 < x;
          then
A17:      n + 0 = x * (n div x) + (n mod x) by NAT_D:2;
          per cases;
          suppose
A18:        n mod x = 0;
            then
A19:        n div x = n / x by Th4;
            thus rfs(r).(i+2) = rfs(r).(1+1) by A14
              .= 1/frac(rfs(r).1) by Def3
              .= 1/(n/fm.0-fd.1) by A8,A13,Def4
              .= 1/(n/x-fd.1) by Def1
              .= 1/(n/x-(n div x)) by Def2
              .= 1 / 0 by A19
              .= fm.i / (n mod x) by A18
              .= fm.i / fm.(i+1) by A14,Def1;
          end;
          suppose
A20:        n mod x <> 0;
            then
A21:        n/x - (n div x) <> 0 by Th5;
            thus rfs(r).(i+2) = rfs(r).(1+1) by A14
              .= 1/frac(rfs(r).1) by Def3
              .= 1/(n/fm.0-fd.1) by A8,A13,Def4
              .= 1/(n/x-fd.1) by Def1
              .= 1/(n/x-(n div x)) by Def2
              .= x / (n mod x) by A16,A17,A20,A21,Lm2
              .= fm.i / (n mod x) by A14,Def1
              .= fm.i / fm.(i+1) by A14,Def1;
          end;
        end;
      end;
      suppose
        a > 0;
        then
A22:    0+1 <= a by NAT_1:13;
        thus
A23:    now
          let b be Nat;
          assume b <= a+1;
          then
A24:      b < a+1 or b = a+1 by XXREAL_0:1;
          per cases by A24,NAT_1:13;
          suppose
            b <= a;
            hence scf(r).b = fd.b by A11;
          end;
          suppose
A25:        b-1 = a;
            reconsider a2 = a-1 as Element of NAT by A22,INT_1:5;
A26:        b = a-1+2 by A25;
            thus scf(r).b = [\ rfs(r).b /] by Def4
              .= fm.a2 div fm.(a2+1) by A11,A26
              .= fd.b by A26,Def2;
          end;
        end;
        let b be Nat;
        assume
A27:    b+1 <= a+1;
        per cases by A27,XXREAL_0:1;
        suppose
          b+1 < a+1;
          then b+1 <= a by NAT_1:13;
          hence thesis by A11;
        end;
        suppose
A28:      b+1 = a+1;
          then reconsider b1 = b-1 as Element of NAT by A22,INT_1:5;
A29:      b+1 = b1+(1+1);
A30:      b1+2 = b1+1+1;
A31:      b+2 = b+1+1;
          per cases;
          suppose
A32:        0 = fm.(b1+1);
            thus rfs(r).(b+2) = 1 / (rfs(r).(b+1)-scf(r).(b+1)) by A31,Th26
              .= 1/(rfs(r).(b+1)-fd.(b+1)) by A23,A28
              .= 1 / (fm.b1 / fm.(b1+1) - fd.(b1+1+1)) by A11,A28,A29
              .= 1 / (fm.b1 / 0 - (fm.b1 div 0)) by A30,A32,Def2
              .= fm.b / fm.(b+1) by A32;
          end;
          suppose
A33:        0 < fm.(b1+1);
            then
A34:        fm.b1 + 0 = fm.(b1+1) * (fm.b1 div fm.(b1+1)) + (fm.b1 mod fm
            .(b1+1)) by NAT_D:2;
            per cases;
            suppose
A35:          fm.b1 mod fm.(b1+1) = 0;
              then fm.b1 / fm.(b1+1) = fm.b1 div fm.(b1+1) by Th4;
              then
A36:          fm.b1 / fm.(b1+1) - (fm.b1 div fm.(b1+1)) = 0;
              thus rfs(r).(b+2) = 1 / (rfs(r).(b+1)-scf(r).(b+1)) by A31,Th26
                .= 1/(rfs(r).(b+1)-(fd.(b+1))) by A23,A28
                .= 1 / (fm.b1 / fm.(b1+1) - fd.(b1+1+1)) by A11,A28,A29
                .= 1 / 0 by A30,A36,Def2
                .= fm.(b1+1) / (fm.b1 mod fm.(b1+1)) by A35
                .= fm.b / fm.(b+1) by A30,Def1;
            end;
            suppose
A37:          fm.b1 mod fm.(b1+1) <> 0;
              then
A38:          fm.b1 / fm.(b1+1) - (fm.b1 div fm.(b1+1)) <> 0 by Th5;
              thus rfs(r).(b+2) = 1 / (rfs(r).(b+1)-scf(r).(b+1)) by A31,Th26
                .= 1 / (rfs(r).(b+1)-fd.(b+1)) by A23,A28
                .= 1 / (fm.b1 / fm.(b1+1) - fd.(b1+1+1)) by A11,A28,A29
                .= 1 / (fm.b1 / fm.(b1+1) - (fm.b1 div fm.(b1+1))) by A30,Def2
                .= fm.(b1+1) / (fm.b1 mod fm.(b1+1)) by A33,A34,A37,A38,Lm2
                .= fm.b / fm.(b+1) by A30,Def1;
            end;
          end;
        end;
      end;
    end;
    for a being Nat holds P[a] from NAT_1:sch 2(A9,A10);
    hence thesis by A8;
  end;
end;

theorem Th42:
  r is rational iff ex n st for m st m >= n holds scf(r).m = 0
proof
  defpred A[Nat] means for s being real number st for m st m >= $1 holds scf(s
  ).m = 0 holds s is rational;
A1: for m st A[m] holds A[m+1]
  proof
    let m;
    assume
A2: A[m];
    let s be real number such that
A3: for n st n >= m+1 holds scf(s).n = 0;
    set B = 1 / (s - scf(s).0);
    for n st n >= m holds scf(B).n = 0
    proof
      let n;
      assume n >= m;
      then
A4:   n+1 >= m+1 by XREAL_1:6;
      thus scf(B).n = scf(s).(n+1) by Lm8
        .= 0 by A3,A4;
    end;
    then reconsider B as rational number by A2;
    scf(s).0 + 1 / B is rational;
    hence thesis;
  end;
  thus r is rational implies ex n st for m st m >= n holds scf(r).m = 0
  proof
    assume r is rational;
    then reconsider r as rational number;
    consider m, n being Nat such that
A5: n <> 0 and
A6: frac(r) = m/n by Th7,INT_1:43;
    frac(r) < 1 by INT_1:43;
    then
A7: m < n by A5,A6,XREAL_1:181;
    set fm = modSeq(n,m);
    set fd = divSeq(n,m);
    per cases;
    suppose
A8:   m = 0;
      take 1;
      let a;
      assume a >= 1;
      then ex x being Nat st a = x+1 by NAT_1:6;
      hence thesis by A6,A8,Th30;
    end;
    suppose
A9:   m <> 0;
      consider k such that
A10:  fd.k = 0 and
      fm.k = 0 by Th25;
A11:  now
        assume
A12:    k = 0;
        m <= 0 or n div m <> 0 by A7,NAT_2:12;
        hence contradiction by A9,A10,A12,Def2;
      end;
      take k+1;
      let a;
      assume
A13:  a >= k+1;
      1 <= k+1 by NAT_1:11;
      then reconsider a1 = a-1 as Element of NAT by A13,INT_1:5,XXREAL_0:2;
A14:  a = a1+1;
      k+0 < k+1 by XREAL_1:6;
      then k < a by A13,XXREAL_0:2;
      then
A15:  k <= a1 by A14,NAT_1:13;
      scf(r).a = scf(1/frac(r)).a1 by A14,Th37
        .= scf(n/m).a1 by A6,XCMPLX_1:57
        .= fd.a1 by Th41
        .= 0 by A10,A11,A15,Th17;
      hence thesis;
    end;
  end;
  given n such that
A16: for m st m >= n holds scf(r).m = 0;
A17: A[0]
  proof
    let s be real number;
    assume for m st m >= 0 holds scf(s).m = 0;
    then for m holds scf(s).m = 0;
    hence thesis by Th34;
  end;
  for n holds A[n] from NAT_1:sch 2(A17,A1);
  hence thesis by A16;
end;

theorem
  (for n holds scf(r).n <> 0) implies r is irrational
proof
  assume
A1: for n holds scf(r).n <> 0;
  not ex n st for m st m >= n holds scf(r).m = 0
  proof
    let n;
    take n;
    thus thesis by A1;
  end;
  hence thesis by Th42;
end;

begin :: Convergents of simple continued fractions

reserve l, n1, n2 for Nat;
reserve s1, s2 for Real_Sequence;

definition
  let r be real number;
  func convergent_numerators(r) -> Real_Sequence means
  :Def5:
  it.0 = scf(r).0
& it.1 = scf(r).1 * scf(r).0 + 1 & for n being Nat holds it.(n+2) = scf(r).(n+2
  ) * it.(n+1) + it.n;
  existence
  proof
    set s = scf(r);
    deffunc U(Nat,Real,Real) = s.($1+2) * $3 + $2;
    consider f being Real_Sequence such that
A1: f.0 = s.0 & f.1 = s.1 * s.0 + 1 and
A2: for n being Element of NAT holds f.(n+2) = U(n,f.n,f.(n+1)) from
    RECDEF_2:sch 5;
    take f;
    thus f.0 = s.0 & f.1 = s.1 * s.0 + 1 by A1;
    let n;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A2;
  end;
  uniqueness
  proof
    set s = scf(r);
    deffunc U(Nat,Real,Real) = s.($1+2) * $3 + $2;
    let f,g be Real_Sequence such that
A3: f.0 = s.0 & f.1 = s.1 * s.0 +1 and
A4: for k being Nat holds f.(k+2) = s.(k+2) * f.(k+1) + f.k and
A5: g.0 = s.0 & g.1 = s.1 * s.0 +1 and
A6: for k being Nat holds g.(k+2) = s.(k+2) * g.(k+1) + g.k;
A7: g.0 = s.0 & g.1 = s.1 * s.0 + 1 by A5;
A8: for k being Element of NAT holds g.(k+2) = U(k,g.k,g.(k+1)) by A6;
A9: for k being Element of NAT holds f.(k+2) = U(k,f.k,f.(k+1)) by A4;
A10: f.0 = s.0 & f.1 = s.1 * s.0 + 1 by A3;
    f = g from RECDEF_2:sch 7(A10,A9,A7,A8);
    hence thesis;
  end;
end;

definition
  let r be real number;
  set s = scf(r);
  func convergent_denominators(r) -> Real_Sequence means
  :Def6:
  it.0 = 1 & it.
1 = scf(r).1 & for n being Nat holds it.(n+2) = scf(r).(n+2) * it.(n+1) + it.n;
  existence
  proof
    deffunc U(Nat,Real,Real) = s.($1+2) * $3 + $2;
    consider f being Real_Sequence such that
A1: f.0 = 1 & f.1 = s.1 and
A2: for n being Element of NAT holds f.(n+2) = U(n,f.n,f.(n+1)) from
    RECDEF_2:sch 5;
    take f;
    thus f.0 = 1 & f.1 = scf(r).1 by A1;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A2;
  end;
  uniqueness
  proof
    deffunc U(Nat,Real,Real) = s.($1+2) * $3 + $2;
    let f, g be Real_Sequence such that
A3: f.0 = 1 & f.1 = s.1 and
A4: for k being Nat holds f.(k+2) = s.(k+2) * f.(k+1) + f.k and
A5: g.0 = 1 & g.1 = s.1 and
A6: for k being Nat holds g.(k+2) = s.(k+2) * g.(k+1) + g.k;
A7: g.0 = 1 & g.1 = s.1 by A5;
A8: for k being Element of NAT holds g.(k+2) = U(k,g.k,g.(k+1)) by A6;
A9: for k being Element of NAT holds f.(k+2) = U(k,f.k,f.(k+1)) by A4;
A10: f.0 = 1 & f.1 = s.1 by A3;
    f = g from RECDEF_2:sch 7(A10,A9,A7,A8);
    hence thesis;
  end;
end;

notation
  let r be real number;
  synonym c_n(r) for convergent_numerators(r);
  synonym c_d(r) for convergent_denominators(r);
end;

theorem Th44:
  scf(r).0 > 0 implies for n holds c_n(r).n in NAT
proof
  set s1=c_n(r);
  set s=scf(r);
  defpred P[Nat] means s1.$1 in NAT;
A1: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A2: s1.n in NAT and
A3: s1.(n+1) in NAT;
    reconsider n2=s1.(n+1) as Element of NAT by A3;
    reconsider n1=s1.n as Element of NAT by A2;
    n+2 >= 0+1 by XREAL_1:7;
    then reconsider n3=s.(n+2) as Element of NAT by Th38,INT_1:3;
    n3*n2+n1 in NAT;
    hence thesis by Def5;
  end;
  assume
A4: scf(r).0 > 0;
A5: P[1]
  proof
    reconsider n2=s.0 as Element of NAT by A4,INT_1:3;
    reconsider n1=s.1 as Element of NAT by Th38,INT_1:3;
    n1*n2+1 in NAT;
    hence thesis by Def5;
  end;
  let n;
  s.0 in NAT by A4,INT_1:3;
  then
A6: P[0] by Def5;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A6,A5,A1);
  hence thesis;
end;

theorem Th45:
  scf(r).0 > 0 implies for n holds c_n(r).n > 0
proof
  assume
A1: scf(r).0>0;
  set s1=c_n(r);
  set s=scf(r);
  defpred P[Nat] means s1.$1>0;
  s1.1 = s.1 * s.0 +1 & s.1 >=0 by Def5,Th38;
  then
A2: P[1] by A1;
  let n;
A3: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume
A4: s1.n>0 & s1.(n+1)>0;
    n+2>1+0 by XREAL_1:8;
    then
A5: s.(n+2) >=0 by Th38;
    s1.(n+2)=s.(n+2) * s1.(n+1) + s1.n by Def5;
    hence thesis by A5,A4;
  end;
A6: P[0] by A1,Def5;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A6,A2,A3);
  hence thesis;
end;

theorem
  scf(r).0 > 0 implies for n holds c_n(r).(n+2) > scf(r).(n+2) * c_n(r). (n+1)
proof
  assume
A1: scf(r).0 > 0;
  let n;
  set s=scf(r);
  set s1=c_n(r);
  set m=s.(n+2)*s1.(n+1);
  s1.(n+2)-m=m+s1.n-m by Def5;
  then s1.(n+2)-s.(n+2) * s1.(n+1)>0 by A1,Th45;
  then s1.(n+2)-m+m>0+m by XREAL_1:6;
  hence thesis;
end;

theorem
  scf(r).0 > 0 implies for n st n1=c_n(r).(n+1) & n2=c_n(r).n holds n1
  gcd n2 = 1
proof
  set s1=c_n(r);
  set s=scf(r);
  defpred X[Nat] means for n1,n2 st n1=s1.($1+1) & n2=s1.$1 holds n1 gcd n2 =
  1;
  assume
A1: scf(r).0 > 0;
A2: for k st X[k] holds X[k+1]
  proof
    let k;
    reconsider n3 = s1.(k+2) as Element of NAT by A1,Th44;
    reconsider n2=s1.k as Element of NAT by A1,Th44;
    k+2 >= 0+1 by XREAL_1:7;
    then reconsider n4 = s.(k+2) as Element of NAT by Th38,INT_1:3;
    reconsider n1=s1.(k+1) as Element of NAT by A1,Th44;
    assume for n1,n2 st n1=s1.(k+1) & n2=s1.k holds n1 gcd n2 = 1;
    then
A3: n1 gcd n2 = 1;
    n3 = n4 * n1 + n2 by Def5;
    hence thesis by A3,EULER_1:8;
  end;
A4: X[0]
  proof
    reconsider u = s.1 as Element of NAT by Th38,INT_1:3;
    let n1,n2 such that
A5: n1=s1.(0+1) and
A6: n2=s1.0;
    n1 =u * s.0 +1 by A5,Def5;
    then
A7: n1 =u * n2 +1 by A6,Def5;
    1 gcd n2 = 1 by NEWTON:51;
    hence thesis by A7,EULER_1:8;
  end;
  for n holds X[n] from NAT_1:sch 2(A4,A2);
  hence thesis;
end;

theorem
  scf(r).0 > 0 & (for n holds scf(r).n <> 0) implies for n holds c_n(r).
  n >= tau |^ n
proof
  assume that
A1: scf(r).0 > 0 and
A2: for n holds scf(r).n <>0;
  set s=scf(r);
A3: s.0 >= 0+1 by A1,INT_1:7;
  set s1=c_n(r);
  defpred P[Nat] means s1.$1 >= tau |^$1;
A4: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A5: s1.n >= tau|^n and
A6: s1.(n+1) >= tau|^(n+1);
A7: tau|^(n+1)+tau|^n =((1+sqrt 5)/2)|^n * ((1+sqrt 5)/2) +((1+sqrt 5)/2)
    |^n by FIB_NUM:def 1,NEWTON:6
      .=((1+sqrt 5)/2)|^n * ((6+2*sqrt 5)/4);
    sqrt 5 >=0 by SQUARE_1:def 2;
    then (1+sqrt 5)/2 > 0 by XREAL_1:139;
    then
A8: tau|^(n+1) > 0 by FIB_NUM:def 1,PREPOWER:6;
A9: tau|^(n+2) =((1+sqrt 5)/2)|^n * ((1+sqrt 5)/2)|^2 by FIB_NUM:def 1,NEWTON:8
      .=((1+sqrt 5)/2)|^n * ((1+sqrt 5)/2)^2 by WSIERP_1:1
      .=((1+sqrt 5)/2)|^n * ((1^2+2*1*sqrt 5+(sqrt 5)^2)/ 4)
      .=((1+sqrt 5)/2)|^n * ((1+2*sqrt 5+5)/ 4) by SQUARE_1:def 2
      .=((1+sqrt 5)/2)|^n * ((6+2*sqrt 5)/ 4);
A10: s1.(n+1+1) = s.(n+2)*s1.(n+1)+s1.n by Def5;
    n+2 >= 0+1 by XREAL_1:7;
    then s.(n+2) >= 1 by A2,Th40;
    then s.(n+2)*s1.(n+1) >= 1*(tau|^(n+1)) by A6,A8,XREAL_1:66;
    hence thesis by A5,A10,A7,A9,XREAL_1:7;
  end;
  s1.0 = s.0 by Def5;
  then
A11: P[0] by A3,NEWTON:4;
  s.1>=1 by A2,Th40;
  then s.1*s.0 >= 1 by A3,XREAL_1:159;
  then
A12: s.1*s.0+1 >= 1+1 by XREAL_1:6;
  let n;
  sqrt 5 < sqrt 3^2 by SQUARE_1:27;
  then sqrt 5 < 3 by SQUARE_1:22;
  then 1+sqrt 5 < 1+3 by XREAL_1:8;
  then
A13: (1+sqrt 5)/2 < 4/2 by XREAL_1:74;
  s1.1 = s.1*s.0+1 & ((1+sqrt 5)/2)|^1 = (1+sqrt 5)/2 by Def5,NEWTON:5;
  then
A14: P[1] by A12,A13,FIB_NUM:def 1,XXREAL_0:2;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A11,A14,A4);
  hence thesis;
end;

theorem
  scf(r).0 > 0 & (for n holds scf(r).n <= b) implies for n holds c_n(r).
  n <= ((b+sqrt (b^2+4))/2)|^(n+1)
proof
  assume that
A1: scf(r).0 > 0 and
A2: for n holds scf(r).n <= b;
  set s1=c_n(r);
  set s=scf(r);
A3: s.0 <= b by A2;
  defpred P[Nat] means s1.$1 <= ((b+sqrt (b^2+4))/2)|^($1+1);
A4: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A5: s1.n <= ((b+sqrt (b^2+4))/2)|^(n+1) and
A6: s1.(n+1) <= ((b+sqrt (b^2+4))/2)|^(n+1+1);
    n+2 >= 0+1 by XREAL_1:7;
    then
A7: s.(n+2) >= 0 by Th38;
    s.(n+2) <= b & s1.(n+1) > 0 by A1,A2,Th45;
    then
A8: s.(n+2)*s1.(n+1) <= b*((b+sqrt (b^2+4))/2)|^(n+1+1) by A6,A7,XREAL_1:66;
A9: b*((b+sqrt (b^2+4))/2)|^(n+1+1)+((b+sqrt (b^2+4))/2)|^(n+1) =b*(((b+
sqrt (b^2+4))/2)|^(n+1) * ((b+sqrt (b^2+4))/2)) + ((b+sqrt (b^2+4))/2)|^(n+1)
    by NEWTON:6
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+b*sqrt (b^2+4)+2)/2);
A10: ((b+sqrt (b^2+4))/2)|^(n+2+1) =((b+sqrt (b^2+4))/2)|^(n+1+2)
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b+sqrt (b^2+4))/2)|^2 by NEWTON:8
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b+sqrt (b^2+4))/2)^2 by WSIERP_1:1
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+2*b*sqrt (b^2+4)+(sqrt (b^2+4))
    ^2)/(2*2))
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+2*b*sqrt (b^2+4)+(b^2+4))/(2*2))
    by SQUARE_1:def 2
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+b*sqrt (b^2+4)+2)/2);
    s1.(n+1+1) = s.(n+2)*s1.(n+1)+s1.n by Def5;
    hence thesis by A5,A8,A9,A10,XREAL_1:7;
  end;
  let n;
  b^2+4 > b^2 by XREAL_1:39;
  then sqrt (b^2+4) > sqrt b^2 by SQUARE_1:27;
  then
A11: sqrt (b^2+4) > b by SQUARE_1:22;
  then b+sqrt (b^2+4) > b+b by XREAL_1:8;
  then (b+sqrt (b^2+4))/2 > (2*b)/2 by XREAL_1:74;
  then
A12: ((b+sqrt (b^2+4))/2)|^(0+1) > b by NEWTON:5;
A13: s.1 >= 0 by Th38;
A14: s1.1 = s.1*s.0+1 by Def5;
  s.1 <= b by A2;
  then s.1*s.0 <= b^2 by A1,A3,A13,XREAL_1:66;
  then
A15: s1.1 <= b^2+1 by A14,XREAL_1:6;
  b*sqrt (b^2+4) >= b*b by A11,XREAL_1:64;
  then b^2+b*sqrt (b^2+4) >= b^2+b*b by XREAL_1:6;
  then b^2+b*sqrt (b^2+4)+2 >= b^2+b^2+2 by XREAL_1:6;
  then
A16: (b^2+b*sqrt (b^2+4)+2)/2 >= (2*(b^2+1))/2 by XREAL_1:72;
  ((b+sqrt (b^2+4))/2)|^(1+1) =((b+sqrt (b^2+4))/2)^2 by WSIERP_1:1
    .=(b^2+2*b*sqrt (b^2+4)+(sqrt (b^2+4))^2)/(2*2)
    .=(b^2+2*b*sqrt (b^2+4)+(b^2+4))/(2*2) by SQUARE_1:def 2
    .=(b^2+b*sqrt (b^2+4)+2)/2;
  then
A17: P[1] by A15,A16,XXREAL_0:2;
  s1.0=s.0 by Def5;
  then
A18: P[0] by A3,A12,XXREAL_0:2;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A18,A17,A4);
  hence thesis;
end;

theorem Th50:
  c_d(r).n in NAT
proof
  set s=scf(r);
  set s2=c_d(r);
  defpred P[Nat] means s2.$1 in NAT;
  s2.0 = 1 by Def6;
  then
A1: P[0];
A2: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A3: s2.n in NAT and
A4: s2.(n+1) in NAT;
    reconsider n2=s2.(n+1) as Element of NAT by A4;
    reconsider n1=s2.n as Element of NAT by A3;
    n+2>=0+1 by XREAL_1:7;
    then reconsider n3=s.(n+2) as Element of NAT by Th38,INT_1:3;
    n3*n2+n1 in NAT;
    hence thesis by Def6;
  end;
  s2.1=s.1 by Def6;
  then
A5: P[1] by Th38,INT_1:3;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A1,A5,A2);
  hence thesis;
end;

theorem Th51:
  c_d(r).n >= 0
proof
  set s=scf(r);
  set s1=c_d(r);
  defpred P[Nat] means s1.$1>=0;
A1: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume
A2: s1.n>=0;
A3: s1.(n+2)=s.(n+2) * s1.(n+1) + s1.n by Def6;
    n+2>1+0 by XREAL_1:8;
    then
A4: s.(n+2) >=0 by Th38;
    assume s1.(n+1)>=0;
    hence thesis by A4,A3,A2;
  end;
  s.1>=0 by Th38;
  then
A5: P[1] by Def6;
A6: P[0] by Def6;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A6,A5,A1);
  hence thesis;
end;

theorem Th52:
  scf(r).1 > 0 implies for n holds c_d(r).n > 0
proof
  set s=scf(r);
  set s1=c_d(r);
  defpred P[Nat] means s1.$1>0;
  assume scf(r).1 > 0;
  then
A1: P[1] by Def6;
  let n;
A2: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume
A3: s1.n>0;
A4: s1.(n+2)=s.(n+2) * s1.(n+1) + s1.n by Def6;
    n+2>1+0 by XREAL_1:8;
    then
A5: s.(n+2) >=0 by Th38;
    assume s1.(n+1)>0;
    hence thesis by A5,A4,A3;
  end;
A6: P[0] by Def6;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A6,A1,A2);
  hence thesis;
end;

theorem
  c_d(r).(n+2) >= scf(r).(n+2) * c_d(r).(n+1)
proof
  set s=scf(r);
  set s1=c_d(r);
  set m=s.(n+2)*s1.(n+1);
  s1.(n+2)-s.(n+2)*s1.(n+1)=s.(n+2)*s1.(n+1)+s1.n-s.(n+2)*s1.(n+1) by Def6;
  then s1.(n+2)-s.(n+2)*s1.(n+1)>=0 by Th51;
  then s1.(n+2)-m+m>=0+m by XREAL_1:6;
  hence thesis;
end;

theorem
  scf(r).1 > 0 implies for n holds c_d(r).(n+2) > scf(r).(n+2) * c_d(r). (n+1)
proof
  assume
A1: scf(r).1 > 0;
  let n;
  set s1=c_d(r);
  set s=scf(r);
  set m=s.(n+2)*s1.(n+1);
  s1.(n+2)-s.(n+2)*s1.(n+1)=s.(n+2)*s1.(n+1)+s1.n-s.(n+2)*s1.(n+1) by Def6;
  then s1.(n+2)-s.(n+2)*s1.(n+1)>0 by A1,Th52;
  then s1.(n+2)-m+m>0+m by XREAL_1:6;
  hence thesis;
end;

theorem
  (for n holds scf(r).n>0) implies for n st n>=1 holds 1 / (c_d(r).n*c_d
  (r).(n+1)) < 1 / (scf(r).(n+1)*(c_d(r).n)^2)
proof
  set s=scf(r),s2=c_d(r);
  defpred X[Nat] means 1/(s2.$1*s2.($1+1))<1/(s.($1+1)*(s2.$1)^2);
  assume
A1: for n holds scf(r).n>0;
  then
A2: s.2>0;
A3: scf(r).1>0 by A1;
A4: for n being Nat st n>=1 & X[n] holds X[n+1]
  proof
    let n be Nat;
    assume that
    n>=1 and
    1/(s2.n*s2.(n+1))<1/(scf(r).(n+1)*(s2.n)^2);
A5: s2.(n+1)>0 by A3,Th52;
    then
A6: (s2.(n+1))^2>0 by SQUARE_1:12;
    s.(n+2)>0 by A1;
    then
A7: s.(n+2)*(s2.(n+1))^2>0 by A6,XREAL_1:129;
    s2.n>0 by A3,Th52;
    then
A8: s2.(n+1)*s2.n>0 by A5,XREAL_1:129;
    s2.(n+1)*s2.(n+1+1) =s2.(n+1)*(s.(n+2)*s2.(n+1)+s2.n) by Def6
      .=s.(n+2)*(s2.(n+1))^2+s2.(n+1)*s2.n;
    hence thesis by A8,A7,XREAL_1:29,76;
  end;
A9: s.1>0 by A1;
  then (s.1)^2>0 by SQUARE_1:12;
  then s.2*(s.1)^2>0 by A2,XREAL_1:129;
  then
A10: 1/(s.2*(s.1)^2+s.1)<1/(s.2*(s.1)^2) by A9,XREAL_1:29,76;
  let n;
  1/(s2.1*s2.(1+1)) =1/(s2.1*(s.(0+2)*s2.(0+1)+s2.0)) by Def6
    .=1/(s2.1*(s.2*s.1+s2.0)) by Def6
    .=1/(s.1*(s.2*s.1+s2.0)) by Def6
    .=1/(s.1*(s.2*s.1+1)) by Def6
    .=1/(s.2*(s.1)^2+s.1);
  then
A11: X[1] by A10,Def6;
  for n being Nat st n>=1 holds X[n] from NAT_1:sch 8(A11,A4);
  hence thesis;
end;

theorem
  (for n holds scf(r).n <= b) implies for n holds c_d(r).(n+1) <= ((b+
  sqrt (b^2+4))/2)|^(n+1)
proof
  set s=scf(r);
  set s2=c_d(r);
  defpred P[Nat] means s2.($1+1) <= ((b+sqrt (b^2+4))/2)|^($1+1);
  assume
A1: for n holds scf(r).n <= b;
  then
A2: s.1 <= b;
A3: s.2 <= b by A1;
  s.2 >= 0 & s.1 >= 0 by Th38;
  then
A4: s.2*s.1 <= b^2 by A2,A3,XREAL_1:66;
  s2.(1+1)=s.(0+2)*s2.(0+1)+s2.0 by Def6
    .=s.2*s2.1+1 by Def6
    .=s.2*s.1+1 by Def6;
  then
A5: s2.(1+1) <= b^2+1 by A4,XREAL_1:6;
  let n;
  b^2+4 > b^2 by XREAL_1:39;
  then sqrt (b^2+4) > sqrt b^2 by SQUARE_1:27;
  then
A6: sqrt (b^2+4) > b by SQUARE_1:22;
  then b+sqrt (b^2+4) > b+b by XREAL_1:8;
  then (b+sqrt (b^2+4))/2 > (2*b)/2 by XREAL_1:74;
  then
A7: ((b+sqrt (b^2+4))/2)|^(0+1) > b by NEWTON:5;
A8: for n be Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A9: s2.(n+1) <= ((b+sqrt (b^2+4))/2)|^(n+1) and
A10: s2.(n+1+1) <= ((b+sqrt (b^2+4))/2)|^(n+1+1);
A11: b*((b+sqrt (b^2+4))/2)|^(n+1+1)+((b+sqrt (b^2+4))/2)|^(n+1) =b*(((b+
sqrt (b^2+4))/2)|^(n+1) * ((b+sqrt (b^2+4))/2)) + ((b+sqrt (b^2+4))/2)|^(n+1)
    by NEWTON:6
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+b*sqrt (b^2+4)+2)/2);
    n+3 >=0+1 by XREAL_1:7;
    then
A12: s.(n+3) >= 0 by Th38;
A13: ((b+sqrt (b^2+4))/2)|^(n+2+1) =((b+sqrt (b^2+4))/2)|^(n+1+2)
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b+sqrt (b^2+4))/2)|^2 by NEWTON:8
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b+sqrt (b^2+4))/2)^2 by WSIERP_1:1
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+2*b*sqrt (b^2+4)+(sqrt (b^2+4))
    ^2)/(2*2))
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+2*b*sqrt (b^2+4)+(b^2+4))/(2*2))
    by SQUARE_1:def 2
      .=((b+sqrt (b^2+4))/2)|^(n+1) * ((b^2+b*sqrt (b^2+4)+2)/2);
A14: s2.(n+2+1) =s.(n+1+2)*s2.(n+1+1)+s2.(n+1) by Def6
      .=s.(n+3)*s2.(n+1+1)+s2.(n+1);
    s.(n+3) <= b & s2.(n+1+1) >= 0 by A1,Th51;
    then s.(n+3)*s2.(n+1+1) <= b*((b+sqrt (b^2+4))/2)|^(n+1+1) by A10,A12,
XREAL_1:66;
    hence thesis by A9,A14,A11,A13,XREAL_1:7;
  end;
  b*sqrt (b^2+4) >= b*b by A6,XREAL_1:64;
  then b^2+b*sqrt (b^2+4) >= b^2+b*b by XREAL_1:6;
  then b^2+b*sqrt (b^2+4)+2 >= b^2+b^2+2 by XREAL_1:6;
  then
A15: (b^2+b*sqrt (b^2+4)+2)/2 >= (2*(b^2+1))/2 by XREAL_1:72;
  ((b+sqrt (b^2+4))/2)|^(1+1) =((b+sqrt (b^2+4))/2)^2 by WSIERP_1:1
    .=(b^2+2*b*sqrt (b^2+4)+(sqrt (b^2+4))^2)/(2*2)
    .=(b^2+2*b*sqrt (b^2+4)+(b^2+4))/(2*2) by SQUARE_1:def 2
    .=(b^2+b*sqrt (b^2+4)+2)/2;
  then
A16: P[1] by A5,A15,XXREAL_0:2;
  s2.(0+1)=s.1 by Def6;
  then
A17: P[0] by A2,A7,XXREAL_0:2;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A17,A16,A8);
  hence thesis;
end;

theorem
  n1=c_d(r).(n+1) & n2=c_d(r).n implies n1 gcd n2 = 1
proof
  set s=scf(r);
  set s2=c_d(r);
  defpred X[Nat] means for n1,n2 st n1=s2.($1+1) & n2=s2.$1 holds n1 gcd n2 =
  1;
A1: for k st X[k] holds X[k+1]
  proof
    let k;
    k+2>=0+1 by XREAL_1:7;
    then reconsider n4 = s.(k+2) as Element of NAT by Th38,INT_1:3;
    reconsider n3 = s2.(k+2) as Element of NAT by Th50;
    reconsider n2=s2.k as Element of NAT by Th50;
    reconsider n1=s2.(k+1) as Element of NAT by Th50;
    assume for n1,n2 st n1=s2.(k+1) & n2=s2.k holds n1 gcd n2 = 1;
    then
A2: n1 gcd n2 = 1;
    n3 = n4 * n1 + n2 by Def6;
    hence thesis by A2,EULER_1:8;
  end;
A3: X[0]
  proof
    let n1,n2 such that
    n1=s2.(0+1) and
A4: n2=s2.0;
    n1 gcd 1 = 1 by NEWTON:51;
    hence thesis by A4,Def6;
  end;
  for n holds X[n] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem Th58:
  (for n holds scf(r).n > 0) implies for n holds c_d(r).(n+1)/c_d(
  r).n >= 1/scf(r).(n+2)
proof
  set s=scf(r);
  set s1=c_d(r);
  defpred X[Nat] means s1.($1+1)/s1.$1 >= 1/s.($1+2);
  assume
A1: for n holds scf(r).n > 0;
  then
A2: scf(r).1<>0;
A3: for n st X[n] holds X[n+1]
  proof
    let n;
    assume s1.(n+1)/s1.n >= 1/s.(n+2);
    set r=s1.(n+1);
A4: s.1 > 0 by A1;
    then
A5: s1.(n+1)>0 by Th52;
    n+3>=0+1 & s.(n+3) <>0 by A1,XREAL_1:7;
    then s.(n+3)>=1 by Th40;
    then
A6: 1/s.(n+3)<=1/1 by XREAL_1:118;
    n+2>=0+1 & s.(n+2) <>0 by A1,XREAL_1:7;
    then
A7: s.(n+2)>=1 by Th40;
A8: s1.n>0 by A4,Th52;
    s1.(n+2)/s1.(n+1)=(s.(n+2) * r + s1.n)/r by Def6
      .=(s.(n+2) * r)/r + s1.n/r
      .=s.(n+2)* (r/r) + s1.n/r
      .=s.(n+2)+ s1.n/r by A5,XCMPLX_1:88;
    then s1.(n+2)/s1.(n+1)>=1+0 by A5,A8,A7,XREAL_1:7;
    hence thesis by A6,XXREAL_0:2;
  end;
  scf(r).2<>0 by A1;
  then s.(0+2)>=1 by Th40;
  then
A9: 1/s.(0+2)<=1/1 by XREAL_1:118;
  s1.0 = 1 & s1.1 = s.1 by Def6;
  then s1.(0+1)/s1.0>=1 by A2,Th40;
  then
A10: X[0] by A9,XXREAL_0:2;
  for n holds X[n] from NAT_1:sch 2(A10,A3);
  hence thesis;
end;

theorem
  (for n holds scf(r).n > 0) implies for n holds c_d(r).(n+2) <= 2*scf(r
  ).(n+2) * c_d(r).(n+1)
proof
  assume
A1: for n holds scf(r).n > 0;
  let n;
  set s=scf(r);
  set s1=c_d(r);
A2: s.(n+2) > 0 by A1;
  s.1 > 0 by A1;
  then
A3: s1.n > 0 by Th52;
A4: s1.(n+1)/s1.n >= 1/s.(n+2) by A1,Th58;
  s1.(n+1)/s1.n * s1.n =s1.n / s1.n * s1.(n+1) .=s1.(n+1) by A3,XCMPLX_1:88;
  then
A5: s1.(n+1) >= s1.n / s.(n+2) by A4,A3,XREAL_1:64;
  s1.n / s.(n+2) * s.(n+2) =s.(n+2) /s.(n+2) * s1.n .= s1.n by A2,XCMPLX_1:88;
  then s1.(n+1) * s.(n+2) >= s1.n by A5,A2,XREAL_1:64;
  then s1.(n+1) * s.(n+2) + s1.(n+1) * s.(n+2)>= s1.n+s1.(n+1) * s.(n+2) by
XREAL_1:6;
  hence thesis by Def6;
end;

theorem
  (for n holds scf(r).n<>0) implies for n holds 1/(scf(r).(n+1)*(c_d(r).
  n)^2) <= 1/(c_d(r).n)^2
proof
  assume
A1: for n holds scf(r).n <>0;
  let n;
  set s=scf(r);
  set s2=c_d(r);
  s.1 <>0 by A1;
  then s.1>0 by Th38;
  then
A2: s2.n>0 by Th52;
  n+1>=1+0 & s.(n+1) <>0 by A1,XREAL_1:7;
  then s.(n+1)*(s2.n)^2 >= 1*(s2.n)^2 by A2,Th40,XREAL_1:64;
  hence thesis by A2,SQUARE_1:12,XREAL_1:118;
end;

theorem
  (for n holds scf(r).n<>0) implies for n holds c_d(r).(n+1) >= tau |^ n
proof
  set s2=c_d(r);
  set s=scf(r);
  defpred P[Nat] means s2.($1+1) >= tau |^$1;
  sqrt 5 < sqrt 3^2 by SQUARE_1:27;
  then sqrt 5 < 3 by SQUARE_1:22;
  then 1+sqrt 5 < 1+3 by XREAL_1:8;
  then
A1: ((1+sqrt 5)/2)|^1 = (1+sqrt 5)/2 & (1+sqrt 5)/2 < 4/2 by NEWTON:5
,XREAL_1:74;
  assume
A2: for n holds scf(r).n <>0;
  then
A3: s.1>=1 by Th40;
  then s2.(0+1)>=1 by Def6;
  then
A4: P[0] by NEWTON:4;
  let n;
A5: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A6: s2.(n+1) >= tau|^n and
A7: s2.(n+1+1) >= tau|^(n+1);
A8: tau|^(n+1)+tau|^n =((1+sqrt 5)/2)|^n * ((1+sqrt 5)/2) +((1+sqrt 5)/2)
    |^n by FIB_NUM:def 1,NEWTON:6
      .=((1+sqrt 5)/2)|^n * ((6+2*sqrt 5)/4);
    sqrt 5 >=0 by SQUARE_1:def 2;
    then (1+sqrt 5)/2 > 0 by XREAL_1:139;
    then
A9: tau|^(n+1) > 0 by FIB_NUM:def 1,PREPOWER:6;
A10: tau|^(n+2) =((1+sqrt 5)/2)|^n * ((1+sqrt 5)/2)|^2 by FIB_NUM:def 1
,NEWTON:8
      .=((1+sqrt 5)/2)|^n * ((1+sqrt 5)/2)^2 by WSIERP_1:1
      .=((1+sqrt 5)/2)|^n * ((1^2+2*1*sqrt 5+(sqrt 5)^2)/ 4)
      .=((1+sqrt 5)/2)|^n * ((1+2*sqrt 5+5)/ 4) by SQUARE_1:def 2
      .=((1+sqrt 5)/2)|^n * ((6+2*sqrt 5)/ 4);
A11: s2.(n+2+1) = s.(n+1+2)*s2.(n+1+1)+s2.(n+1) by Def6
      .=s.(n+3)*s2.(n+1+1)+s2.(n+1);
    n+3 >= 0+1 by XREAL_1:7;
    then s.(n+3) >= 1 by A2,Th40;
    then s.(n+3)*s2.(n+1+1) >= 1*(tau|^(n+1)) by A7,A9,XREAL_1:66;
    hence thesis by A6,A11,A8,A10,XREAL_1:7;
  end;
  s.2>=1 by A2,Th40;
  then s.2*s.1 >= 1 by A3,XREAL_1:159;
  then
A12: s.2*s.1+1 >= 1+1 by XREAL_1:6;
  s2.(1+1) = s.(0+2) * s2.(0+1) + s2.0 by Def6
    .=s.2 * s2.1 + 1 by Def6
    .=s.2 * s.1 + 1 by Def6;
  then
A13: P[1] by A12,A1,FIB_NUM:def 1,XXREAL_0:2;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A4,A13,A5);
  hence thesis;
end;

theorem
  a > 0 & (for n holds scf(r).n >= a) implies for n holds c_d(r).(n+1)
  >= ((a+sqrt (a^2+4))/2)|^n
proof
  assume that
A1: a > 0 and
A2: for n holds scf(r).n >= a;
  set s=scf(r);
  set s2=c_d(r);
  defpred P[Nat] means s2.($1+1) >= ((a+sqrt (a^2+4))/2)|^$1;
A3: s.1>0 by A1,A2;
  then s.1>=1 by Th40;
  then s2.(0+1)>=1 by Def6;
  then
A4: P[0] by NEWTON:4;
  s.2>0 by A1,A2;
  then s.2*s.1 >= 1*s.1 by A3,Th40,XREAL_1:64;
  then
A5: s.2*s.1+1 >= s.1+1 by XREAL_1:6;
  s.1 >= a by A2;
  then s.1+1 >= a+1 by XREAL_1:6;
  then
A6: s.2*s.1+1 >= a+1 by A5,XXREAL_0:2;
  4*a > 0 by A1,XREAL_1:129;
  then a^2+4 < a^2+4 + 4*a by XREAL_1:39;
  then sqrt (a^2+4) < sqrt (a+2)^2 by SQUARE_1:27;
  then sqrt (a^2+4) < a+2 by SQUARE_1:22;
  then a+sqrt (a^2+4) < a+(a+2) by XREAL_1:8;
  then
A7: ((a+sqrt (a^2+4))/2)|^1 = (a+sqrt (a^2+4))/2 & (a+sqrt (a^2+4))/2 < (2*
  a+2*1 )/2 by NEWTON:5,XREAL_1:74;
  let n;
A8: for n being Nat st P[n] & P[n+1] holds P[n+2]
  proof
    let n be Nat;
    assume that
A9: s2.(n+1) >= ((a+sqrt (a^2+4))/2)|^n and
A10: s2.(n+1+1) >= ((a+sqrt (a^2+4))/2)|^(n+1);
A11: a*((a+sqrt (a^2+4))/2)|^(n+1)+((a+sqrt (a^2+4))/2)|^n =a*(((a+sqrt (a
    ^2+4))/2)|^n * ((a+sqrt (a^2+4))/2)) + ((a+sqrt (a^2+4))/2)|^n by NEWTON:6
      .=((a+sqrt (a^2+4))/2)|^n * ((a^2+a*sqrt (a^2+4)+2)/2);
    sqrt (a^2+4) > 0 by SQUARE_1:25;
    then (a+sqrt (a^2+4))/2 > 0 by XREAL_1:139;
    then
A12: ((a+sqrt (a^2+4))/2)|^(n+1) > 0 by PREPOWER:6;
A13: ((a+sqrt (a^2+4))/2)|^(n+2) =((a+sqrt (a^2+4))/2)|^n * ((a+sqrt (a^2+
    4))/2)|^2 by NEWTON:8
      .=((a+sqrt (a^2+4))/2)|^n * ((a+sqrt (a^2+4))/2)^2 by WSIERP_1:1
      .=((a+sqrt (a^2+4))/2)|^n * ((a^2+2*a*sqrt (a^2+4)+(sqrt (a^2+4))^2)/(
    2*2))
      .=((a+sqrt (a^2+4))/2)|^n * ((a^2+2*a*sqrt (a^2+4)+(a^2+4))/(2*2)) by
SQUARE_1:def 2
      .=((a+sqrt (a^2+4))/2)|^n * ((a^2+a*sqrt (a^2+4)+2)/2);
A14: s2.(n+2+1) =s.(n+1+2)*s2.(n+1+1)+s2.(n+1) by Def6
      .=s.(n+3)*s2.(n+1+1)+s2.(n+1);
    s.(n+3) >= a by A2;
    then s.(n+3)*s2.(n+1+1) >= a*((a+sqrt (a^2+4))/2)|^(n+1) by A10,A12,
XREAL_1:66;
    hence thesis by A9,A14,A11,A13,XREAL_1:7;
  end;
  s2.(1+1) =s.(0+2)*s2.(0+1)+s2.0 by Def6
    .=s.2*s2.1+1 by Def6
    .=s.2*s.1+1 by Def6;
  then
A15: P[1] by A6,A7,XXREAL_0:2;
  for n being Nat holds P[n] from FIB_NUM:sch 1(A4,A15,A8);
  hence thesis;
end;

theorem
  c_n(r).(n+2) / c_d(r).(n+2) = (scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n)
  / (scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n)
proof
  c_n(r).(n+2) = scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n by Def5;
  hence thesis by Def6;
end;

theorem Th64:
  c_n(r).(n+1)*c_d(r).n - c_n(r).n*c_d(r).(n+1) = (-1)|^n
proof
  set s=scf(r), s1=c_n(r),s2=c_d(r);
  defpred G[Nat] means s1.($1+1)*s2.$1-s1.$1*s2.($1+1)=(-1)|^$1;
A1: s2.0 = 1 & s2.1 = s.1 by Def6;
A2: for n st G[n] holds G[n+1]
  proof
    let l;
    assume
A3: s1.(l+1)*s2.l-s1.l*s2.(l+1)=(-1)|^l;
    s1.(l+2)*s2.(l+1)-s1.(l+1)*s2.(l+2) =(s.(l+2) * s1.(l+1) + s1.l)*s2.(l
    +1)-s1.(l+1)*s2.(l+2) by Def5
      .=(s.(l+2) * s1.(l+1)*s2.(l+1) + s1.l*s2.(l+1)) -s1.(l+1)*(s.(l+2) *
    s2.(l+1) + s2.l) by Def6
      .=(-1)*(s1.(l+1)*s2.l-s1.l*s2.(l+1))
      .=(-1)|^(l+1) by A3,NEWTON:6;
    hence thesis;
  end;
  s1.0 = s.0 & s1.1 = s.1 * s.0 + 1 by Def5;
  then
A4: G[0] by A1,NEWTON:4;
  for n holds G[n] from NAT_1:sch 2(A4,A2);
  hence thesis;
end;

theorem Th65:
  (for n holds c_d(r).n<>0) implies c_n(r).(n+1)/c_d(r).(n+1) -
  c_n(r).n/c_d(r).n = (-1)|^n / (c_d(r).(n+1)*c_d(r).n)
proof
  set s1=c_n(r), s2=c_d(r);
  assume for n holds s2.n<>0;
  then s2.n<>0 & s2.(n+1)<>0;
  then
  s1.(n+1)/s2.(n+1)-s1.n/s2.n =(s1.(n+1)*s2.n-s1.n*s2.(n+1))/(s2.(n+1)*s2.
  n) by XCMPLX_1:130
    .=(-1)|^n /(s2.(n+1)*s2.n) by Th64;
  hence thesis;
end;

theorem Th66:
  c_n(r).(n+2)*c_d(r).n - c_n(r).n*c_d(r).(n+2) = (-1)|^n * scf(r) .(n+2)
proof
  set s1=c_n(r), s2=c_d(r), s=scf(r);
  s1.(n+2)*s2.n-s1.n*s2.(n+2) =(s.(n+2)*s1.(n+1)+s1.n)*s2.n-s1.n*s2.(n+2)
  by Def5
    .=(s.(n+2)*s1.(n+1)+s1.n)*s2.n-s1.n*(s.(n+2)*s2.(n+1)+s2.n) by Def6
    .=s.(n+2)*(s1.(n+1)*s2.n-s1.n*s2.(n+1))
    .=(-1)|^n * s.(n+2) by Th64;
  hence thesis;
end;

theorem
  (for n holds c_d(r).n<>0) implies c_n(r).(n+2)/c_d(r).(n+2) - c_n(r).n
  /c_d(r).n = (-1)|^n * scf(r).(n+2) / (c_d(r).(n+2) * c_d(r).n)
proof
  set s1=c_n(r), s2=c_d(r), s=scf(r);
  assume for n holds s2.n<>0;
  then s2.n<>0 & s2.(n+2)<>0;
  then
  s1.(n+2)/s2.(n+2) - s1.n/s2.n =(s1.(n+2) * s2.n - s1.n * s2.(n+2))/(s2.(
  n+2) * s2.n) by XCMPLX_1:130
    .=(-1)|^n * s.(n+2)/(s2.(n+2) * s2.n) by Th66;
  hence thesis;
end;

theorem
  (for n holds scf(r).n<>0) implies for n st n >= 1 holds c_n(r).n / c_d
  (r).n = (c_n(r).(n+1)-c_n(r).(n-1)) / (c_d(r).(n+1)-c_d(r).(n-1))
proof
  set s1=c_n(r), s2=c_d(r);
  set s=scf(r);
  defpred P[Nat] means s1.$1/s2.$1=(s1.($1+1)-s1.($1-1))/(s2.($1+1)-s2.($1-1));
  assume
A1: for n holds scf(r).n<>0;
A2: for n being Nat st n>=1 holds P[n] implies P[n+1]
  proof
    let n be Nat;
    assume that
    n>=1 and
    s1.n/s2.n=(s1.(n+1)-s1.(n-1))/(s2.(n+1)-s2.(n-1));
    s.(n+2) * s1.(n+1) + s1.n - s1.n = s1.(n+2) - s1.n & s2.(n+2) - s2.n =
    s.(n+ 2) * s2.(n+1) + s2.n - s2.n by Def5,Def6;
    hence thesis by A1,XCMPLX_1:91;
  end;
  let n;
  (s1.(1+1)-s1.(1-1))/(s2.(1+1)-s2.(1-1)) =(s.(2+0) * s1.(0+1) + s1.0-s1.0
  )/(s2.(2+0)-s2.0) by Def5
    .=(s.2 * s1.1 + s1.0-s1.0)/(s.2 * s2.1 + s2.0-s2.0) by Def6
    .=s1.1/s2.1 by A1,XCMPLX_1:91;
  then
A3: P[1];
  for n being Nat st n>=1 holds P[n] from NAT_1:sch 8(A3,A2);
  hence thesis;
end;

theorem
  (for n holds c_d(r).n<>0) implies for n holds abs (c_n(r).(n+1)/c_d(r)
  .(n+1) - c_n(r).n/c_d(r).n) = 1 / abs (c_d(r).(n+1)*c_d(r).n)
proof
  set s1=c_n(r), s2=c_d(r);
  assume
A1: for n holds s2.n<>0;
  let n;
  reconsider n as Element of NAT by ORDINAL1:def 12;
  abs (s1.(n+1)/s2.(n+1)-s1.n/s2.n) =abs ( (-1) |^n / (s2.(n+1)*s2.n) ) by A1
,Th65
    .=abs ( (-1) |^n ) / abs (s2.(n+1)*s2.n) by COMPLEX1:67
    .=abs ( (-1) to_power n ) / abs (s2.(n+1)*s2.n) by POWER:41
    .=((abs(-1)) to_power n) / abs (s2.(n+1)*s2.n) by SERIES_1:2
    .=((-(-1)) to_power n) / abs (s2.(n+1)*s2.n) by ABSVALUE:def 1
    .=1 / abs (s2.(n+1)*s2.n) by POWER:26;
  hence thesis;
end;

theorem
  scf(r).1 > 0 implies for n holds c_n(r).(2*n+1) / c_d(r).(2*n+1) > c_n
  (r).(2*n) / c_d(r).(2*n)
proof
  set s1=c_n(r), s2=c_d(r), s=scf(r);
  defpred X[Nat] means s1.(2*$1+1)/s2.(2*$1+1)>s1.(2*$1)/s2.(2*$1);
A1: s1.(2*0)/s2.(2*0) =s.0/s2.0 by Def5
    .=s.0/1 by Def6
    .=s.0;
  assume
A2: scf(r).1>0;
A3: for n st X[n] holds X[n+1]
  proof
    let n;
    assume s1.(2*n+1)/s2.(2*n+1)>s1.(2*n)/s2.(2*n);
    reconsider n as Element of NAT by ORDINAL1:def 12;
    s1.(2*(n+1)+1)*s2.(2*(n+1))-s1.(2*(n+1))*s2.(2*(n+1)+1) =(-1)|^(2*(n+1
    )) by Th64
      .=(1|^(2*(n+1))) by WSIERP_1:2
      .=1 by NEWTON:10;
    then
A4: s1.(2*(n+1)+1)*s2.(2*(n+1))>s1.(2*(n+1))*s2.(2*(n+1)+1) by XREAL_1:47;
    s2.(2*(n+1)+1)>0 & s2.(2*(n+1))>0 by A2,Th52;
    hence thesis by A4,XREAL_1:106;
  end;
  s1.(2*0+1)/s2.(2*0+1) =(s.1 * s.0 +1) / s2.1 by Def5
    .=(s.1 * s.0 +1) / s.1 by Def6
    .=s.0 +1 / s.1 by A2,XCMPLX_1:113;
  then
A5: X[0] by A2,A1,XREAL_1:29;
  for n holds X[n] from NAT_1:sch 2(A5,A3);
  hence thesis;
end;

definition
  let r be real number;
::$N Convergents of continued fraction
  func convergents_of_continued_fractions(r) -> Real_Sequence equals
  c_n(r) /"
  c_d(r);
  coherence;
end;

notation
  let r be real number;
  synonym cocf(r) for convergents_of_continued_fractions(r);
end;

theorem
  cocf(r).0 = scf(r).0
proof
  thus cocf(r).0 = c_n(r).0 * ((c_d(r))").0 by SEQ_1:8
    .=c_n(r).0 * (c_d(r).0)" by VALUED_1:10
    .=c_n(r).0 *(1/c_d(r).0)
    .=c_n(r).0 /c_d(r).0
    .=(scf(r)).0 / c_d(r).0 by Def5
    .=(scf(r)).0 / 1 by Def6
    .=scf(r).0;
end;

theorem Th72:
  scf(r).1 <> 0 implies cocf(r).1 = scf(r).0 + 1 / scf(r).1
proof
  set s=scf(r);
  assume
A1: scf(r).1<>0;
  thus cocf(r).1 = c_n(r).1 * ((c_d(r))").1 by SEQ_1:8
    .=c_n(r).1 * (c_d(r).1)" by VALUED_1:10
    .=c_n(r).1 *(1/c_d(r).1)
    .=c_n(r).1 /c_d(r).1
    .=(s.1 * s.0 +1) / c_d(r).1 by Def5
    .=(s.1 * s.0 +1) / s.1 by Def6
    .=s.0 +1 / s.1 by A1,XCMPLX_1:113;
end;

theorem Th73:
  (for n holds scf(r).n>0) implies cocf(r).2 = scf(r).0 + 1 / (scf
  (r).1 + 1/scf(r).2)
proof
  set s=scf(r);
A1: cocf(r).2 =c_n(r).2 * ((c_d(r))").2 by SEQ_1:8
    .=c_n(r).2 * (c_d(r).2)" by VALUED_1:10
    .=c_n(r).2 *(1/c_d(r).2)
    .=c_n(r).2 /c_d(r).2;
  assume
A2: for n holds scf(r).n>0;
  then
A3: s.1>0;
A4: c_d(r).2 =s.(0+2)*c_d(r).(0+1) + c_d(r).0 by Def6
    .=s.2*s.1+c_d(r).0 by Def6
    .=s.2*s.1+1 by Def6;
A5: c_n(r).2 =s.(0+2) * c_n(r).(0+1) + c_n(r).0 by Def5
    .=s.2*(s.1 * s.0 +1) +c_n(r).0 by Def5
    .=s.2 * s.1 * s.0 +s.2 +s.0 by Def5;
A6: s.2>0 by A2;
  then s.0 + 1/(s.1+1/s.2) =s.0+1/((s.1 * s.2 +1)/ s.2) by XCMPLX_1:113
    .=s.0 + s.2/(s.1 * s.2 +1) by XCMPLX_1:57
    .=(s.0 * (s.1 * s.2 +1) + s.2)/(s.1 * s.2 +1) by A3,A6,XCMPLX_1:113
    .=cocf(r).2 by A1,A5,A4;
  hence thesis;
end;

theorem Th74:
  (for n holds scf(r).n>0) implies cocf(r).3 = scf(r).0 + 1/(scf(r
  ).1 + 1/(scf(r).2 + 1/scf(r).3))
proof
  set s=scf(r);
A1: cocf(r).3 =c_n(r).3 * ((c_d(r))").3 by SEQ_1:8
    .=c_n(r).3 * (c_d(r).3)" by VALUED_1:10
    .=c_n(r).3 *(1/c_d(r).3)
    .=c_n(r).3 /c_d(r).3;
  assume
A2: for n holds scf(r).n>0;
  then
A3: s.1>0;
A4: c_d(r).2 =s.(0+2)*c_d(r).(0+1) + c_d(r).0 by Def6
    .=s.2*s.1+c_d(r).0 by Def6
    .=s.2*s.1+1 by Def6;
A5: c_d(r).3 =s.(1+2)*c_d(r).(1+1) + c_d(r).1 by Def6
    .=s.3*(s.2*s.1+1)+s.1 by A4,Def6
    .=s.1*(s.2*s.3 +1)+s.3;
A6: c_n(r).2 =s.(0+2) * c_n(r).(0+1) + c_n(r).0 by Def5
    .=s.2*(s.1 * s.0 +1) +c_n(r).0 by Def5
    .=s.2 * s.1 * s.0 +s.2 +s.0 by Def5;
A7: c_n(r).3 =s.(1+2) * c_n(r).(1+1) + c_n(r).1 by Def5
    .=s.3*(s.2 * s.1 * s.0 +s.2 +s.0) +(s.1 * s.0 +1) by A6,Def5
    .=(s.3*s.2 * s.1 * s.0) +s.3*s.2 +s.3*s.0 +s.1 * s.0 +1;
A8: s.2>0 by A2;
A9: s.3>0 by A2;
  then s.0 + 1/(s.1 + 1/(s.2 + 1/s.3)) =s.0 + 1/(s.1 + 1/((s.2*s.3 + 1)/s.3))
  by XCMPLX_1:113
    .=s.0 + 1/(s.1 + s.3/(s.2*s.3 + 1)) by XCMPLX_1:57
    .=s.0 + 1/((s.1*(s.2*s.3 + 1) + s.3)/(s.2*s.3 + 1)) by A8,A9,XCMPLX_1:113
    .=s.0 +(s.2*s.3 + 1)/(s.1*(s.2*s.3 + 1) + s.3) by XCMPLX_1:57
    .=(s.0*(s.1*(s.2*s.3 + 1) + s.3)+(s.2*s.3 + 1))/(s.1*(s.2*s.3 + 1) + s.3
  ) by A3,A8,A9,XCMPLX_1:113;
  hence thesis by A1,A7,A5;
end;

theorem
  (for n holds scf(r).n>0) implies for n st n>=1 holds c_n(r).(2*n+1) /
  c_d(r).(2*n+1) < c_n(r).(2*n-1) / c_d(r).(2*n-1)
proof
  set s=scf(r), s1=c_n(r), s2=c_d(r);
  defpred X[Nat] means s1.(2*$1+1)/s2.(2*$1+1)<s1.(2*$1-1)/s2.(2*$1-1);
  assume
A1: for n holds scf(r).n>0;
  then
A2: s.3>0;
  cocf(r).3 = c_n(r).3 * ((c_d(r))").3 by SEQ_1:8
    .= c_n(r).3 * (c_d(r).3)" by VALUED_1:10
    .= c_n(r).3 *(1/c_d(r).3)
    .= c_n(r).3 /c_d(r).3;
  then
A3: s1.(2*1+1)/s2.(2*1+1) = s.0 + 1/(s.1 + 1/(s.2 + 1/s.3)) by A1,Th74
    .= s.0 + 1/(s.1 + 1/((s.2*s.3 + 1)/s.3)) by A2,XCMPLX_1:113
    .= s.0 + 1/(s.1 + s.3/(s.2*s.3 + 1)) by XCMPLX_1:57;
  let n;
A4: s.1>0 by A1;
A5: scf(r).1 > 0 by A1;
A6: for n being Nat st n>=1 & X[n] holds X[n+1]
  proof
    let n be Nat;
    assume that
    n>=1 and
    s1.(2*n+1)/s2.(2*n+1)<s1.(2*n-1)/s2.(2*n-1);
    s1.(2*(n+1)+1)*s2.(2*(n+1)-1)-s1.(2*(n+1)-1)*s2.(2*(n+1)+1) =(s.(2*n+
    1+2) * s1.(2*n+1+1) + s1.(2*n+1))*s2.(2*n+1)-s1.(2*n+1)*s2.(2*n+3) by Def5
      .=(s.(2*n+1+2) * s1.(2*n+1+1) + s1.(2*n+1))*s2.(2*n+1) -s1.(2*n+1)*(s.
    (2*n+1+2) * s2.(2*n+1+1) + s2.(2*n+1)) by Def6
      .=s.(2*n+1+2)*(s1.(2*n+1+1)*s2.(2*n+1)-s1.(2*n+1)*s2.(2*n+1+1))
      .=s.(2*n+1+2) * (-1)|^(2*n+1) by Th64
      .=s.(2*n+1+2) * (-1|^(2*n+1)) by WSIERP_1:2
      .=s.(2*n+1+2) * (-1) by NEWTON:10;
    then s1.(2*(n+1)+1)*s2.(2*(n+1)-1)-s1.(2*(n+1)-1)*s2.(2*(n+1)+1)<0 by A1,
XREAL_1:132;
    then
A7: s1.(2*(n+1)+1)*s2.(2*(n+1)-1)<s1.(2*(n+1)-1)*s2.(2*(n+1)+1) by XREAL_1:48;
    s2.(2*n+1)>0 & s2.(2*n+3)>0 by A5,Th52;
    hence thesis by A7,XREAL_1:106;
  end;
  s.2>0 by A1;
  then s.3/(s.2*s.3 + 1)>0 by A2,XREAL_1:139;
  then
A8: 1/(s.1 +s.3/(s.2*s.3 + 1))<1/s.1 by A4,XREAL_1:29,76;
  s1.(2*1-1)/s2.(2*1-1) = (s.1 * s.0 +1)/s2.1 by Def5
    .= (s.1 * s.0 +1)/s.1 by Def6
    .= s.0 +1 / s.1 by A4,XCMPLX_1:113;
  then
A9: X[1] by A8,A3,XREAL_1:8;
  for n being Nat st n>=1 holds X[n] from NAT_1:sch 8(A9,A6);
  hence thesis;
end;

theorem
  (for n holds scf(r).n>0) implies for n st n>=1 holds c_n(r).(2*n) /
  c_d(r).(2*n) > c_n(r).(2*n-2) / c_d(r).(2*n-2)
proof
  set s=scf(r), s1=c_n(r), s2=c_d(r);
  defpred X[Nat] means s1.(2*$1)/s2.(2*$1)>s1.(2*$1-2)/s2.(2*$1-2);
  assume
A1: for n holds scf(r).n>0;
  then
A2: s.1>0;
A3: scf(r).1 > 0 by A1;
A4: for n being Nat st n>=1 & X[n] holds X[n+1]
  proof
    let n be Nat;
    assume that
    n>=1 and
    s1.(2*n)/s2.(2*n)>s1.(2*n-2)/s2.(2*n-2);
    s1.(2*(n+1))*s2.(2*(n+1)-2)-s1.(2*(n+1)-2)*s2.(2*(n+1)) = (s.(2*n+2)
    * s1.(2*n+1) + s1.(2*n))*s2.(2*n)-s1.(2*n)*s2.(2*n+2) by Def5
      .= (s.(2*n+2) * s1.(2*n+1) + s1.(2*n))*s2.(2*n) -s1.(2*n)*(s.(2*n+2) *
    s2.(2*n+1) + s2.(2*n)) by Def6
      .= s.(2*n+2) * (s1.(2*n+1) *s2.(2*n)-s1.(2*n)* s2.(2*n+1))
      .= s.(2*n+2) * (-1)|^(2*n) by Th64
      .= s.(2*n+2) * (1|^(2*n)) by WSIERP_1:2
      .= s.(2*n+2) * 1 by NEWTON:10
      .= s.(2*n+2);
    then
A5: s1.(2*(n+1))*s2.(2*(n+1)-2)>s1.(2*(n+1)-2)*s2.(2*(n+1)) by A1,XREAL_1:47;
    s2.(2*n)>0 & s2.(2*n+2)>0 by A3,Th52;
    hence thesis by A5,XREAL_1:106;
  end;
  let n;
A6: s1.(2*1-2)/s2.(2*1-2) = s.0/s2.0 by Def5
    .=s.0/1 by Def6
    .=s.0;
A7: s.2>0 by A1;
  cocf(r).2 = c_n(r).2 * ((c_d(r))").2 by SEQ_1:8
    .= c_n(r).2 * (c_d(r).2)" by VALUED_1:10
    .= c_n(r).2 *(1/c_d(r).2)
    .= c_n(r).2 /c_d(r).2;
  then s1.(2*1)/s2.(2*1) = s.0 + 1/(s.1 + 1/s.2) by A1,Th73
    .= s.0+1/((s.1 * s.2 +1)/ s.2) by A7,XCMPLX_1:113
    .= s.0 + s.2/(s.1 * s.2 +1) by XCMPLX_1:57;
  then
A8: X[1] by A2,A7,A6,XREAL_1:29,139;
  for n being Nat st n>=1 holds X[n] from NAT_1:sch 8(A8,A4);
  hence thesis;
end;

theorem
  (for n holds scf(r).n>0) implies for n st n>=1 holds c_n(r).(2*n) /
  c_d(r).(2*n) < c_n(r).(2*n-1) / c_d(r).(2*n-1)
proof
  set s=scf(r), s1=c_n(r), s2=c_d(r);
  defpred X[Nat] means s1.(2*$1)/s2.(2*$1)<s1.(2*$1-1)/s2.(2*$1-1);
  assume
A1: for n holds scf(r).n>0;
  then s.1>0 & s.2>0;
  then
A2: 1/(s.1 + 1/s.2) < 1/s.1 by XREAL_1:29,76;
  let n;
A3: scf(r).1>0 by A1;
A4: for n being Nat st n>=1 & X[n] holds X[n+1]
  proof
    let n be Nat;
    assume that
    n>=1 and
    s1.(2*n)/s2.(2*n)<s1.(2*n-1)/s2.(2*n-1);
    s1.(2*(n+1))*s2.(2*(n+1)-1)-s1.(2*(n+1)-1)*s2.(2*(n+1)) =s1.(2*n+1+1)
    *s2.(2*n+1)-s1.(2*n+1)*s2.(2*n+1+1)
      .=(-1)|^(2*n+1) by Th64
      .=(-1|^(2*n+1)) by WSIERP_1:2
      .=-1 by NEWTON:10;
    then
A5: s1.(2*(n+1))*s2.(2*(n+1)-1)<s1.(2*(n+1)-1)*s2.(2*(n+1)) by XREAL_1:48;
    s2.(2*n+1)>0 & s2.(2*n+2)>0 by A3,Th52;
    hence thesis by A5,XREAL_1:106;
  end;
  cocf(r).1 = c_n(r).1 * ((c_d(r))").1 by SEQ_1:8
    .= c_n(r).1 * (c_d(r).1)" by VALUED_1:10
    .= c_n(r).1 *(1/c_d(r).1)
    .= s1.(2*1-1)/s2.(2*1-1);
  then
A6: s1.(2*1-1)/s2.(2*1-1) = s.0 + 1/s.1 by A3,Th72;
  cocf(r).2 = c_n(r).2 * ((c_d(r))").2 by SEQ_1:8
    .= c_n(r).2 * (c_d(r).2)" by VALUED_1:10
    .= c_n(r).2 *(1/c_d(r).2)
    .= s1.(2*1)/s2.(2*1);
  then s1.(2*1)/s2.(2*1) = s.0 + 1/(s.1 + 1/s.2) by A1,Th73;
  then
A7: X[1] by A6,A2,XREAL_1:8;
  for n being Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A4);
  hence thesis;
end;

definition
  let r be real number;
  set s=scf(r);
  func backContinued_fraction r -> Real_Sequence means
  :Def8:
  it.0 = scf(r).0 & for n being Nat holds it.(n+1) = 1/it.n + scf(r).(n+1);
  existence
  proof
    deffunc U(Nat,Real) = 1/$2 + s.($1+1);
    consider f being Real_Sequence such that
A1: f.0 = s.0 and
A2: for n being Nat holds f.(n+1) = U(n,(f.n)) from NAT_1:sch 12;
    take f;
    thus f.0 = scf(r).0 by A1;
    let n;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let s1,s2;
    assume that
A3: s1.0=s.0 and
A4: for n holds s1.(n+1)=1/s1.n + s.(n+1) and
A5: s2.0=s.0 and
A6: for n holds s2.(n+1)=1/s2.n + s.(n+1);
    defpred X[Nat] means s1.$1 = s2.$1;
A7: for k st X[k] holds X[k+1]
    proof
      let k;
      assume s1.k =s2.k;
      hence s1.(k+1) = 1/s2.k + s.(k+1) by A4
        .= s2.(k+1) by A6;
    end;
    let x be Element of NAT;
A8: X[0] by A3,A5;
    for n holds X[n] from NAT_1:sch 2(A8,A7);
    hence s1.x = s2.x;
  end;
end;

notation
  let r be real number;
  synonym bcf r for backContinued_fraction r;
end;

theorem
  scf(r).0 > 0 implies for n holds bcf(r).(n+1)=c_n(r).(n+1)/c_n(r).n
proof
  set s1=c_n(r);
  set s=scf(r);
  defpred X[Nat] means bcf(r).($1+1)=s1.($1+1)/s1.$1;
  set s3=bcf(r);
  assume
A1: scf(r).0 > 0;
A2: for n st X[n] holds X[n+1]
  proof
    let n;
    assume
A3: bcf(r).(n+1)=s1.(n+1)/s1.n;
A4: s1.(n+1)>0 by A1,Th45;
    bcf(r).(n+1+1) = 1/s3.(n+1) + s.(n+1+1) by Def8
      .=s1.n/s1.(n+1)+ s.(n+1+1) by A3,XCMPLX_1:57
      .=(s1.n+ s.(n+2)*s1.(n+1))/s1.(n+1) by A4,XCMPLX_1:113
      .=s1.(n+2)/s1.(n+1) by Def5;
    hence thesis;
  end;
  bcf(r).(0+1) = 1/s3.0 + s.(0+1) by Def8
    .=1/s.0 + s.1 by Def8
    .=(1+s.0 * s.1)/s.0 by A1,XCMPLX_1:113
    .=s1.1/s.0 by Def5
    .=s1.(0+1)/s1.0 by Def5;
  then
A5: X[0];
  for n holds X[n] from NAT_1:sch 2(A5,A2);
  hence thesis;
end;