:: Simple Continued Fractions and Their Convergents
:: by Bo Li , Yan Zhang and Artur Korni{\l}owicz
::
:: Received August 18, 2006
:: Copyright (c) 2006-2026 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, FUNCT_7;
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_D,
RELAT_1, RELSET_1, FUNCOP_1, VALUED_1, SEQ_1, FUNCT_2, NEWTON, NAT_1,
FIB_NUM, POWER, IRRAT_1;
constructors REAL_1, SQUARE_1, NAT_1, NAT_D, NEWTON, POWER, FUNCOP_1,
BINARITH, FIB_NUM, VALUED_1, PARTFUN1, RELSET_1, NUMBERS;
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, FUNCT_2;
equalities VALUED_1, SQUARE_1, INT_1, XCMPLX_0;
expansions TARSKI, FUNCT_2, INT_1;
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, 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,
p for Rational,
c for Complex,
x for object,
f for Function;
Lm1: for a,b,c,d being Real 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;
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;
cluster n mod 0 -> zero;
coherence;
cluster 0 div n -> zero;
coherence;
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;
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:
for m,n being Integer holds
frac (m/n) = (m mod n) / n & m mod n = n * frac (m/n)
proof
let m,n be Integer;
per cases;
suppose
A1: n = 0; then
T1: frac(m/n) = frac(0) .= (m mod n) / n by A1;
frac(m/n) * n = n * (m mod n) / n by A1;
thus thesis by A1,T1;
end;
suppose
A2: n > 0;
set a = m, b = n;
reconsider b as non zero Integer by A2;
a mod b = a - b*(a div b) by INT_1:def 10
.= (a/b)*b - b*(a div b) by XCMPLX_1:87
.= ([\a/b/] + frac(a/b))*b - b*(a div b)
.= b*[\a/b/] + b*(frac (a/b)) - b*[\a/b/]
.= b*(frac (a/b));
hence thesis by XCMPLX_1:89;
end;
suppose
A2: n < 0;
set a = m, b = n;
reconsider b as non zero Integer by A2;
a mod b = a - b*(a div b) by INT_1:def 10
.= (a/b)*b - b*(a div b) by XCMPLX_1:87
.= ([\a/b/] + frac(a/b))*b - b*(a div b)
.= b*[\a/b/] + b*(frac (a/b)) - b*[\a/b/]
.= b*(frac (a/b));
hence thesis by XCMPLX_1:89;
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 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;
A1: dom s = NAT by FUNCOP_1:13;
for n being Nat holds s.n is real;
then reconsider s as Real_Sequence by SEQ_1:2,A1;
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 object;
assume y in rng f;
then consider x being object 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;
end;
then
A5: rng f c=INT;
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,RELAT_1:def 19,SEQ_1:1;
end;
theorem Th9:
f is sequence of INT iff f is Integer_Sequence
proof
hereby
assume f is sequence of INT;
then reconsider g = f as sequence of 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 be object;
assume x in rng f;
then ex y being object 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 sequence of NAT iff f is sequence of NAT;
begin :: On the Euclidean algorithm
definition
deffunc F(Nat,Nat,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 sequence of NAT such that
A1: f.0 = a & f.1 = b and
A2: for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1)) 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;
thus 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 sequence of NAT;
A7: g.0 = a & g.1 = b by A5;
A8: for n being Nat holds g.(n+2) = F(n,g.n,g.(n+1)) by A6;
A9: for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1)) 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,Nat,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 sequence of NAT such that
A1: f.0 = a & f.1 = b and
A2: for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1)) 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;
thus 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 sequence of NAT;
A7: g.0 = a & g.1 = b by A5;
A8: for n being 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 Nat holds f.(n+2) = F(n,f.n,f.(n+1)) 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;
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;
Lm2: 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;
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,Lm2;
end;
suppose
A6: a < x;
thus fm.a > fm.(x+1)
proof
per cases by Lm2;
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;
Lm3: 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;
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 Lm3;
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;
theorem Th21:
divSeq(m,0) = NAT --> 0
proof
set g = NAT --> 0;
set fd = divSeq(m,0);
A1: for x being object st x in dom fd holds fd.x = g.x
proof
defpred P[Nat] means fd.$1 = 0;
let x be object;
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;
end;
theorem Th22:
modSeq(m,0) = NAT --> 0
proof
set fm = modSeq(m,0);
A1: for x being object st x in dom fm holds fm.x = g.x
proof
defpred P[Nat] means fm.$1 = 0;
let x be object;
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;
end;
theorem
divSeq(0,n) = NAT --> 0
proof
set fd = divSeq(0,n);
A1: for x being object st x in dom fd holds fd.x = g.x
proof
defpred P[Nat] means fd.$1 = 0;
let x be object;
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;
end;
theorem
modSeq(0,n) = NAT --> 0
proof
set fm = modSeq(0,n);
A1: for x being object st x in dom fm holds fm.x = g.x
proof
defpred P[Nat] means fm.$1 = 0;
let x be object;
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;
end;
Lm4: 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 Lm4;
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,object] means $3 = 1 / frac($2);
definition
let r be Real;
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 Nat for x being Element of REAL
ex y being Element of REAL st P[n,x,y]
proof let n be Nat, x be Element of REAL;
consider y being Real such that
A2: P[n,x,y];
reconsider y as Element of REAL by XREAL_0:def 1;
take y;
thus P[n,x,y] by A2;
end;
consider f being sequence of REAL such that
A3: f.0 = r1 and
A4: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:
sch 2( A1);
take f;
thus f.0 = r by A3;
let n;
thus thesis by A4;
end;
uniqueness
proof
A5: 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
A6: g1.0 = r and
A7: for n being Nat holds g1.(n+1) = 1/frac(g1.n) and
A8: g2.0 = r and
A9: for n being Nat holds g2.(n+1) = 1/frac(g2.n);
A10: for n being Nat holds P[n,g1.n,g1.(n+1)] by A7;
A11: for n being Nat holds P[n,g2.n,g2.(n+1)] by A9;
A12: g2.0 = r1 by A8;
A13: g1.0 = r1 by A6;
thus g1 = g2 from NAT_1:sch 14(A13,A10,A12,A11,A5);
end;
end;
notation
let r be Real;
synonym rfs r for remainders_for_scf r;
end;
definition
let r be Real;
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 sequence of 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;
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
.= 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;
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;
Lm5: 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
.= 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;
end;
theorem
i > 1 implies rfs(1/i).1 = i & rfs(1/i).(n+2) = 0 by Lm5;
theorem
i > 1 implies scf(1/i).0 = 0 & scf(1/i).1 = i & scf(1/i).(n+2) = 0 by Lm5;
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;
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;
Lm6: 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 Lm6;
end;
theorem Th37:
scf(r).(n+1) = scf(1/frac(r)).n
proof
frac(r) = r - scf(r).0 by Th35;
hence thesis by Lm6;
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,Lm1
.= 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,Lm1
.= 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 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 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 Lm6
.= 0 by A3,A4;
end;
then reconsider B as Rational 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;
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;
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;
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) = In(s.($1+2) * $3 + $2,REAL);
reconsider s0 = s.0, s1 = s.1 * s.0 + 1 as Element of REAL
by XREAL_0:def 1;
consider f being Real_Sequence such that
A1: f.0 = s0 & f.1 = s1 and
A2: for n being 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;
f.(n+2) = U(n,f.n,f.(n+1)) by A2;
hence thesis;
end;
uniqueness
proof
set s = scf(r);
deffunc U(Nat,Real,Real) = In(s.($1+2) * $3 + $2,REAL);
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;
reconsider s0 = s.0, s1 = s.1 * s.0 + 1 as Element of REAL
by XREAL_0:def 1;
A7: g.0 = s0 & g.1 = s1 by A5;
A8: for k being Nat holds g.(k+2) = U(k,g.k,g.(k+1)) by A6;
A9: for k being Nat holds f.(k+2) = U(k,f.k,f.(k+1)) by A4;
A10: f.0 = s0 & f.1 = s1 by A3;
f = g from RECDEF_2:sch 7(A10,A9,A7,A8);
hence thesis;
end;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
definition
let r be Real;
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) = In(s.($1+2) * $3 + $2,REAL);
consider f being Real_Sequence such that
A1: f.0 = jj & f.1 = s.1 and
A2: for n being 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;
f.(n+2) = U(n,f.n,f.(n+1)) by A2;
hence thesis;
end;
uniqueness
proof
deffunc U(Nat,Real,Real) = In(s.($1+2) * $3 + $2,REAL);
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 = jj & g.1 = s.1 by A5;
A8: for k being Nat holds g.(k+2) = U(k,g.k,g.(k+1)) by A6;
A9: for k being Nat holds f.(k+2) = U(k,f.k,f.(k+1)) by A4;
A10: f.0 = jj & 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;
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;
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;
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;
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 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 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 |.c_n(r).(n+1)/c_d(r)
.(n+1) - c_n(r).n/c_d(r).n.| = 1 / |.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;
|.s1.(n+1)/s2.(n+1)-s1.n/s2.n.| =|. (-1) |^n / (s2.(n+1)*s2.n).| by A1
,Th65
.=|. (-1) |^n .| / |.s2.(n+1)*s2.n.| by COMPLEX1:67
.=|. (-1) to_power n .| / |.s2.(n+1)*s2.n.| by POWER:41
.=(|.-1.| to_power n) / |.s2.(n+1)*s2.n.| by SERIES_1:2
.=((-(-1)) to_power n) / |.s2.(n+1)*s2.n.| by ABSVALUE:def 1
.=1 / |.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;
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;
::$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;
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);
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
.= 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;
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;
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) = In(1/$2 + s.($1+1),REAL);
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;
f.(n+1) = U(n,(f.n)) by A2;
hence thesis;
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;
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;