:: 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 b₁ being Real_Sequence st b₁ 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 H₁( 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 b₁ being sequence of NAT st
( b₁ . 0 = m mod n & b₁ . 1 = n mod (m mod n) & ( for k being Nat holds b₁ . (k + 2) = (b₁ . k) mod (b₁ . (k + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st b₁ . 0 = m mod n & b₁ . 1 = n mod (m mod n) & ( for k being Nat holds b₁ . (k + 2) = (b₁ . k) mod (b₁ . (k + 1)) ) & b₂ . 0 = m mod n & b₂ . 1 = n mod (m mod n) & ( for k being Nat holds b₂ . (k + 2) = (b₂ . k) mod (b₂ . (k + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem REAL_3:def 1 :
canceled;

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

definition

let m, n be Nat;
set a = m div n;
set b = n div (m mod n);
deffunc H₁( 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 b₁ being sequence of NAT st
( b₁ . 0 = m div n & b₁ . 1 = n div (m mod n) & ( for k being Nat holds b₁ . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st b₁ . 0 = m div n & b₁ . 1 = n div (m mod n) & ( for k being Nat holds b₁ . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) & b₂ . 0 = m div n & b₂ . 1 = n div (m mod n) & ( for k being Nat holds b₂ . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines divSeq REAL_3:def 3 :
for m, n being Nat
for b₃ being sequence of NAT holds
( b₃ = divSeq (m,n) iff ( b₃ . 0 = m div n & b₃ . 1 = n div (m mod n) & ( for k being Nat holds b₃ . (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 S₁[ 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 b₁ being Real_Sequence st
( b₁ . 0 = r & ( for n being Nat holds b₁ . (n + 1) = 1 / (frac (b₁ . n)) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = r & ( for n being Nat holds b₁ . (n + 1) = 1 / (frac (b₁ . n)) ) & b₂ . 0 = r & ( for n being Nat holds b₂ . (n + 1) = 1 / (frac (b₂ . n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines remainders_for_scf REAL_3:def 4 :
for r being real number
for b₂ being Real_Sequence holds
( b₂ = remainders_for_scf r iff ( b₂ . 0 = r & ( for n being Nat holds b₂ . (n + 1) = 1 / (frac (b₂ . 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 b₁ being Integer_Sequence st
for n being Nat holds b₁ . n = [\((rfs r) . n)/]

proof end;

uniqueness
for b₁, b₂ being Integer_Sequence st ( for n being Nat holds b₁ . n = [\((rfs r) . n)/] ) & ( for n being Nat holds b₂ . n = [\((rfs r) . n)/] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines SimpleContinuedFraction REAL_3:def 5 :
for r being real number
for b₂ being Integer_Sequence holds
( b₂ = SimpleContinuedFraction r iff for n being Nat holds b₂ . 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 b₁ being Real_Sequence st
( b₁ . 0 = (scf r) . 0 & b₁ . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b₁ . (n + 2) = (((scf r) . (n + 2)) * (b₁ . (n + 1))) + (b₁ . n) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = (scf r) . 0 & b₁ . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b₁ . (n + 2) = (((scf r) . (n + 2)) * (b₁ . (n + 1))) + (b₁ . n) ) & b₂ . 0 = (scf r) . 0 & b₂ . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b₂ . (n + 2) = (((scf r) . (n + 2)) * (b₂ . (n + 1))) + (b₂ . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines convergent_numerators REAL_3:def 6 :
for r being real number
for b₂ being Real_Sequence holds
( b₂ = convergent_numerators r iff ( b₂ . 0 = (scf r) . 0 & b₂ . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b₂ . (n + 2) = (((scf r) . (n + 2)) * (b₂ . (n + 1))) + (b₂ . 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 b₁ being Real_Sequence st
( b₁ . 0 = 1 & b₁ . 1 = (scf r) . 1 & ( for n being Nat holds b₁ . (n + 2) = (((scf r) . (n + 2)) * (b₁ . (n + 1))) + (b₁ . n) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = 1 & b₁ . 1 = (scf r) . 1 & ( for n being Nat holds b₁ . (n + 2) = (((scf r) . (n + 2)) * (b₁ . (n + 1))) + (b₁ . n) ) & b₂ . 0 = 1 & b₂ . 1 = (scf r) . 1 & ( for n being Nat holds b₂ . (n + 2) = (((scf r) . (n + 2)) * (b₂ . (n + 1))) + (b₂ . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines convergent_denominators REAL_3:def 7 :
for r being real number
for b₂ being Real_Sequence holds
( b₂ = convergent_denominators r iff ( b₂ . 0 = 1 & b₂ . 1 = (scf r) . 1 & ( for n being Nat holds b₂ . (n + 2) = (((scf r) . (n + 2)) * (b₂ . (n + 1))) + (b₂ . 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 b₁ being Real_Sequence st
( b₁ . 0 = (scf r) . 0 & ( for n being Nat holds b₁ . (n + 1) = (1 / (b₁ . n)) + ((scf r) . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st b₁ . 0 = (scf r) . 0 & ( for n being Nat holds b₁ . (n + 1) = (1 / (b₁ . n)) + ((scf r) . (n + 1)) ) & b₂ . 0 = (scf r) . 0 & ( for n being Nat holds b₂ . (n + 1) = (1 / (b₂ . n)) + ((scf r) . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines backContinued_fraction REAL_3:def 9 :
for r being real number
for b₂ being Real_Sequence holds
( b₂ = backContinued_fraction r iff ( b₂ . 0 = (scf r) . 0 & ( for n being Nat holds b₂ . (n + 1) = (1 / (b₂ . 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;