:: Simple Continued Fractions and Their Convergents
:: by Bo Li , Yan Zhang and Artur Korni{\l}owicz
::
:: Received August 18, 2006
:: Copyright (c) 2006-2011 Association of Mizar Users


begin

Lm1: now
let n be Nat; :: thesis: ( n > 1 implies n - 1 is Nat )
assume n > 1 ; :: thesis: n - 1 is Nat
then n - 1 > 1 - 1 by XREAL_1:16;
then n - 1 in NAT by INT_1:16;
hence n - 1 is Nat ; :: thesis: verum
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 end;

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

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

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

theorem Th1: :: REAL_3:1
for r being real number st 0 < r & r < 1 holds
1 < 1 / r
proof end;

theorem Th2: :: REAL_3:2
for i being Integer
for r being real number st i <= r & r < i + 1 holds
[\r/] = i
proof end;

theorem :: REAL_3:3
for m, n being Nat holds [\(m / n)/] = m div n ;

theorem Th4: :: REAL_3:4
for m, n being Nat st m mod n = 0 holds
m / n = m div n
proof end;

theorem Th5: :: REAL_3:5
for m, n being Nat st m / n = m div n holds
m mod n = 0
proof end;

theorem Th6: :: REAL_3:6
for m, n being Nat holds frac (m / n) = (m mod n) / n
proof end;

theorem Th7: :: REAL_3:7
for p being rational number st p >= 0 holds
ex m, n being Nat st
( n <> 0 & p = m / n )
proof end;

notation
let R be Relation;
synonym integer-yielding R for integer-valued ;
end;

registration
cluster non zero Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V27( NAT , REAL ) complex-valued ext-real-valued real-valued integer-yielding Element of K6(K7(NAT,REAL));
existence
ex b1 being Real_Sequence st b1 is integer-yielding
proof end;
end;

definition
mode Integer_Sequence is integer-yielding Real_Sequence;
end;

theorem Th8: :: REAL_3:8
for f being Function holds
( f is Integer_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is integer ) ) )
proof end;

theorem Th9: :: REAL_3:9
for f being Function holds
( f is Function of NAT,INT iff f is Integer_Sequence )
proof end;

theorem :: REAL_3:10
for f being Function holds
( f is sequence of NAT iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is natural ) ) )
proof end;

theorem :: REAL_3:11
for f being Function holds
( f is Function of NAT,NAT iff f is sequence of NAT ) ;

begin

definition
deffunc H1( Nat, Element of NAT , Element of NAT ) -> Element of NAT = $2 mod $3;
canceled;
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 :Def2: :: REAL_3:def 2
( 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
ex b1 being sequence of NAT st
( b1 . 0 = m mod n & b1 . 1 = n mod (m mod n) & ( for k being Nat holds b1 . (k + 2) = (b1 . k) mod (b1 . (k + 1)) ) )
proof end;
uniqueness
for b1, b2 being sequence of NAT st b1 . 0 = m mod n & b1 . 1 = n mod (m mod n) & ( for k being Nat holds b1 . (k + 2) = (b1 . k) mod (b1 . (k + 1)) ) & b2 . 0 = m mod n & b2 . 1 = n mod (m mod n) & ( for k being Nat holds b2 . (k + 2) = (b2 . k) mod (b2 . (k + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem REAL_3:def 1 :
canceled;

:: deftheorem Def2 defines modSeq REAL_3:def 2 :
for m, n being Nat
for b3 being sequence of NAT holds
( b3 = modSeq (m,n) iff ( b3 . 0 = m mod n & b3 . 1 = n mod (m mod n) & ( for k being Nat holds b3 . (k + 2) = (b3 . k) mod (b3 . (k + 1)) ) ) );

definition
let m, n be Nat;
set a = m div n;
set b = n div (m mod n);
deffunc H1( Nat, Element of 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 :Def3: :: REAL_3:def 3
( 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
ex b1 being sequence of NAT st
( b1 . 0 = m div n & b1 . 1 = n div (m mod n) & ( for k being Nat holds b1 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) )
proof end;
uniqueness
for b1, b2 being sequence of NAT st b1 . 0 = m div n & b1 . 1 = n div (m mod n) & ( for k being Nat holds b1 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) & b2 . 0 = m div n & b2 . 1 = n div (m mod n) & ( for k being Nat holds b2 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines divSeq REAL_3:def 3 :
for m, n being Nat
for b3 being sequence of NAT holds
( b3 = divSeq (m,n) iff ( b3 . 0 = m div n & b3 . 1 = n div (m mod n) & ( for k being Nat holds b3 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) ) );

theorem Th12: :: REAL_3:12
for m, n being Nat holds (divSeq (m,n)) . 1 = n div ((modSeq (m,n)) . 0)
proof end;

theorem Th13: :: REAL_3:13
for m, n being Nat holds (modSeq (m,n)) . 1 = n mod ((modSeq (m,n)) . 0)
proof end;

theorem Th14: :: REAL_3:14
for a, b, m, n being Nat st a <= b & (modSeq (m,n)) . a = 0 holds
(modSeq (m,n)) . b = 0
proof end;

Lm3: for m, n, a being Nat holds
( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
proof end;

theorem Th15: :: REAL_3:15
for a, b, m, n being Nat holds
( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 )
proof end;

theorem Th16: :: REAL_3:16
for m, n, a being Nat st (divSeq (m,n)) . (a + 1) = 0 holds
(modSeq (m,n)) . a = 0
proof end;

Lm4: for m, n, a being Nat st (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . (a + 1) = 0
proof end;

theorem Th17: :: REAL_3:17
for a, b, m, n being Nat st a <> 0 & a <= b & (divSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . b = 0
proof end;

theorem Th18: :: REAL_3:18
for a, b, m, n being Nat st a < b & (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . b = 0
proof end;

theorem Th19: :: REAL_3:19
for n, m being Nat st n <> 0 holds
m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0)
proof end;

theorem :: REAL_3:20
for n, m being Nat st n <> 0 holds
m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0)))
proof end;

set g = NAT --> 0;

Lm5: dom (NAT --> 0) = NAT
by FUNCOP_1:19;

theorem Th21: :: REAL_3:21
for m being Nat holds divSeq (m,0) = NAT --> 0
proof end;

theorem Th22: :: REAL_3:22
for m being Nat holds modSeq (m,0) = NAT --> 0
proof end;

theorem :: REAL_3:23
for n being Nat holds divSeq (0,n) = NAT --> 0
proof end;

theorem :: REAL_3:24
for n being Nat holds modSeq (0,n) = NAT --> 0
proof end;

Lm6: for m, n being Nat ex k being Nat st (modSeq (m,n)) . k = 0
proof end;

theorem Th25: :: REAL_3:25
for m, n being Nat ex k being Nat st
( (divSeq (m,n)) . k = 0 & (modSeq (m,n)) . k = 0 )
proof end;

begin

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

definition
let r be real number ;
func remainders_for_scf r -> Real_Sequence means :Def4: :: REAL_3:def 4
( it . 0 = r & ( for n being Nat holds it . (n + 1) = 1 / (frac (it . n)) ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = r & ( for n being Nat holds b1 . (n + 1) = 1 / (frac (b1 . n)) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = r & ( for n being Nat holds b1 . (n + 1) = 1 / (frac (b1 . n)) ) & b2 . 0 = r & ( for n being Nat holds b2 . (n + 1) = 1 / (frac (b2 . n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines remainders_for_scf REAL_3:def 4 :
for r being real number
for b2 being Real_Sequence holds
( b2 = remainders_for_scf r iff ( b2 . 0 = r & ( for n being Nat holds b2 . (n + 1) = 1 / (frac (b2 . n)) ) ) );

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 :Def5: :: REAL_3:def 5
for n being Nat holds it . n = [\((rfs r) . n)/];
existence
ex b1 being Integer_Sequence st
for n being Nat holds b1 . n = [\((rfs r) . n)/]
proof end;
uniqueness
for b1, b2 being Integer_Sequence st ( for n being Nat holds b1 . n = [\((rfs r) . n)/] ) & ( for n being Nat holds b2 . n = [\((rfs r) . n)/] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines SimpleContinuedFraction REAL_3:def 5 :
for r being real number
for b2 being Integer_Sequence holds
( b2 = SimpleContinuedFraction r iff for n being Nat holds b2 . n = [\((rfs r) . n)/] );

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

theorem Th26: :: REAL_3:26
for n being Nat
for r being real number holds (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n))
proof end;

theorem Th27: :: REAL_3:27
for n, m being Nat
for r being real number st (rfs r) . n = 0 & n <= m holds
(rfs r) . m = 0
proof end;

theorem :: REAL_3:28
for n, m being Nat
for r being real number st (rfs r) . n = 0 & n <= m holds
(scf r) . m = 0
proof end;

theorem Th29: :: REAL_3:29
for n being Nat
for i being Integer holds (rfs i) . (n + 1) = 0
proof end;

theorem Th30: :: REAL_3:30
for n being Nat
for i being Integer holds
( (scf i) . 0 = i & (scf i) . (n + 1) = 0 )
proof end;

Lm7: for n being Nat
for i being Integer st i > 1 holds
( (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 end;

theorem :: REAL_3:31
for n being Nat
for i being Integer st i > 1 holds
( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 ) by Lm7;

theorem :: REAL_3:32
for n being Nat
for i being Integer st i > 1 holds
( (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) by Lm7;

theorem Th33: :: REAL_3:33
for n being Nat
for r being real number st ( for n being Nat holds (scf r) . n = 0 ) holds
(rfs r) . n = 0
proof end;

theorem Th34: :: REAL_3:34
for r being real number st ( for n being Nat holds (scf r) . n = 0 ) holds
r = 0
proof end;

Lm8: for n being Nat
for r being real number holds
( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) )
proof end;

theorem Th35: :: REAL_3:35
for r being real number holds frac r = r - ((scf r) . 0)
proof end;

theorem :: REAL_3:36
for n being Nat
for r being real number holds (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n
proof end;

theorem Th37: :: REAL_3:37
for n being Nat
for r being real number holds (scf r) . (n + 1) = (scf (1 / (frac r))) . n
proof end;

theorem Th38: :: REAL_3:38
for n being Nat
for r being real number st n >= 1 holds
(scf r) . n >= 0
proof end;

theorem :: REAL_3:39
for n being Nat
for r being real number st n >= 1 holds
(scf r) . n in NAT by Th38, INT_1:16;

theorem Th40: :: REAL_3:40
for n being Nat
for r being real number st n >= 1 & (scf r) . n <> 0 holds
(scf r) . n >= 1
proof end;

theorem Th41: :: REAL_3:41
for m, n, k being Nat holds
( (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 end;

theorem Th42: :: REAL_3:42
for r being real number holds
( r is rational iff ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 )
proof end;

theorem :: REAL_3:43
for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds
not r is rational
proof end;

begin

definition
let r be real number ;
func convergent_numerators r -> Real_Sequence means :Def6: :: REAL_3:def 6
( 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
ex b1 being Real_Sequence st
( b1 . 0 = (scf r) . 0 & b1 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = (scf r) . 0 & b1 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) & b2 . 0 = (scf r) . 0 & b2 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines convergent_numerators REAL_3:def 6 :
for r being real number
for b2 being Real_Sequence holds
( b2 = convergent_numerators r iff ( b2 . 0 = (scf r) . 0 & b2 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) ) );

definition
let r be real number ;
set s = scf r;
func convergent_denominators r -> Real_Sequence means :Def7: :: REAL_3:def 7
( 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
ex b1 being Real_Sequence st
( b1 . 0 = 1 & b1 . 1 = (scf r) . 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = 1 & b1 . 1 = (scf r) . 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) & b2 . 0 = 1 & b2 . 1 = (scf r) . 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines convergent_denominators REAL_3:def 7 :
for r being real number
for b2 being Real_Sequence holds
( b2 = convergent_denominators r iff ( b2 . 0 = 1 & b2 . 1 = (scf r) . 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) ) );

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: :: REAL_3:44
for r being real number st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . n in NAT
proof end;

theorem Th45: :: REAL_3:45
for r being real number st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . n > 0
proof end;

theorem :: REAL_3:46
for r being real number st (scf r) . 0 > 0 holds
for n being Nat holds (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1))
proof end;

theorem :: REAL_3:47
for r being real number
for n1, n2 being Nat st (scf r) . 0 > 0 holds
for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds
n1 gcd n2 = 1
proof end;

theorem :: REAL_3:48
for r being real number st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds (c_n r) . n >= tau |^ n
proof end;

theorem :: REAL_3:49
for b being Nat
for r being real number st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) holds
for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)
proof end;

theorem Th50: :: REAL_3:50
for n being Nat
for r being real number holds (c_d r) . n in NAT
proof end;

theorem Th51: :: REAL_3:51
for n being Nat
for r being real number holds (c_d r) . n >= 0
proof end;

theorem Th52: :: REAL_3:52
for r being real number st (scf r) . 1 > 0 holds
for n being Nat holds (c_d r) . n > 0
proof end;

theorem :: REAL_3:53
for n being Nat
for r being real number holds (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1))
proof end;

theorem :: REAL_3:54
for r being real number st (scf r) . 1 > 0 holds
for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1))
proof end;

theorem :: REAL_3:55
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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 end;

theorem :: REAL_3:56
for b being Nat
for r being real number st ( for n being Nat holds (scf r) . n <= b ) holds
for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)
proof end;

theorem :: REAL_3:57
for n being Nat
for r being real number
for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds
n1 gcd n2 = 1
proof end;

theorem Th58: :: REAL_3:58
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2))
proof end;

theorem :: REAL_3:59
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1))
proof end;

theorem :: REAL_3:60
for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2)
proof end;

theorem :: REAL_3:61
for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat holds (c_d r) . (n + 1) >= tau |^ n
proof end;

theorem :: REAL_3:62
for a being Nat
for r being real number st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds
for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n
proof end;

theorem :: REAL_3:63
for n being Nat
for r being real number holds ((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 end;

theorem Th64: :: REAL_3:64
for n being Nat
for r being real number holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n
proof end;

theorem Th65: :: REAL_3:65
for n being Nat
for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((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 end;

theorem Th66: :: REAL_3:66
for n being Nat
for r being real number holds (((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 end;

theorem :: REAL_3:67
for n being Nat
for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((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 end;

theorem :: REAL_3:68
for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds
for n being Nat 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 end;

theorem :: REAL_3:69
for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds
for n being Nat 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 end;

theorem :: REAL_3:70
for r being real number st (scf r) . 1 > 0 holds
for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n))
proof end;

definition
let r be real number ;
func convergents_of_continued_fractions r -> Real_Sequence equals :: REAL_3:def 8
(c_n r) /" (c_d r);
coherence
(c_n r) /" (c_d r) is Real_Sequence
;
end;

:: deftheorem defines convergents_of_continued_fractions REAL_3:def 8 :
for r being real number holds convergents_of_continued_fractions r = (c_n r) /" (c_d r);

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

theorem :: REAL_3:71
for r being real number holds (cocf r) . 0 = (scf r) . 0
proof end;

theorem Th72: :: REAL_3:72
for r being real number st (scf r) . 1 <> 0 holds
(cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1))
proof end;

theorem Th73: :: REAL_3:73
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
(cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2))))
proof end;

theorem Th74: :: REAL_3:74
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
(cocf r) . 3 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3))))))
proof end;

theorem :: REAL_3:75
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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 end;

theorem :: REAL_3:76
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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 end;

theorem :: REAL_3:77
for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds
for n being Nat 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 end;

definition
let r be real number ;
set s = scf r;
func backContinued_fraction r -> Real_Sequence means :Def9: :: REAL_3:def 9
( it . 0 = (scf r) . 0 & ( for n being Nat holds it . (n + 1) = (1 / (it . n)) + ((scf r) . (n + 1)) ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = (scf r) . 0 & ( for n being Nat holds b1 . (n + 1) = (1 / (b1 . n)) + ((scf r) . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = (scf r) . 0 & ( for n being Nat holds b1 . (n + 1) = (1 / (b1 . n)) + ((scf r) . (n + 1)) ) & b2 . 0 = (scf r) . 0 & ( for n being Nat holds b2 . (n + 1) = (1 / (b2 . n)) + ((scf r) . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines backContinued_fraction REAL_3:def 9 :
for r being real number
for b2 being Real_Sequence holds
( b2 = backContinued_fraction r iff ( b2 . 0 = (scf r) . 0 & ( for n being Nat holds b2 . (n + 1) = (1 / (b2 . n)) + ((scf r) . (n + 1)) ) ) );

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

theorem :: REAL_3:78
for r being real number st (scf r) . 0 > 0 holds
for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n)
proof end;