:: by Bo Li , Yan Zhang and Artur Korni{\l}owicz

::

:: Received August 18, 2006

:: Copyright (c) 2006-2019 Association of Mizar Users

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 end;

registration

let n be Nat;

coherence

n div 0 is zero by NAT_D:def 1;

coherence

n mod 0 is zero by NAT_D:def 2;

coherence

0 div n is zero by NAT_2:2;

coherence

0 mod n is zero by NAT_D:26;

end;
coherence

n div 0 is zero by NAT_D:def 1;

coherence

n mod 0 is zero by NAT_D:def 2;

coherence

0 div n is zero by NAT_2:2;

coherence

0 mod n is zero by NAT_D:26;

registration
end;

registration

ex b_{1} being Real_Sequence st b_{1} is INT -valued
end;

cluster Relation-like omega -defined REAL -valued INT -valued V6() Function-like V29( omega ) V33( omega , REAL ) V67() V68() V69() for Element of K16(K17(omega,REAL));

existence ex b

proof end;

theorem Th8: :: REAL_3:8

for f being Function holds

( f is Integer_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds

f . x is integer ) ) )

( f is Integer_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds

f . x is integer ) ) )

proof end;

theorem :: REAL_3:10

for f being Function holds

( f is sequence of NAT iff ( dom f = NAT & ( for x being object st x in NAT holds

f . x is natural ) ) )

( f is sequence of NAT iff ( dom f = NAT & ( for x being object st x in NAT holds

f . x is natural ) ) )

proof end;

definition

deffunc H_{1}( Nat, Nat, Nat) -> Element of omega = $2 mod $3;

let m, n be Nat;

set a = m mod n;

set b = n mod (m mod n);

ex b_{1} being sequence of NAT st

( b_{1} . 0 = m mod n & b_{1} . 1 = n mod (m mod n) & ( for k being Nat holds b_{1} . (k + 2) = (b_{1} . k) mod (b_{1} . (k + 1)) ) )

for b_{1}, b_{2} being sequence of NAT st b_{1} . 0 = m mod n & b_{1} . 1 = n mod (m mod n) & ( for k being Nat holds b_{1} . (k + 2) = (b_{1} . k) mod (b_{1} . (k + 1)) ) & b_{2} . 0 = m mod n & b_{2} . 1 = n mod (m mod n) & ( for k being Nat holds b_{2} . (k + 2) = (b_{2} . k) mod (b_{2} . (k + 1)) ) holds

b_{1} = b_{2}

end;
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: :: REAL_3:def 1

( 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 ( 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)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines modSeq REAL_3:def 1 :

for m, n being Nat

for b_{3} being sequence of NAT holds

( b_{3} = modSeq (m,n) iff ( b_{3} . 0 = m mod n & b_{3} . 1 = n mod (m mod n) & ( for k being Nat holds b_{3} . (k + 2) = (b_{3} . k) mod (b_{3} . (k + 1)) ) ) );

for m, n being Nat

for b

( b

definition

let m, n be Nat;

set a = m div n;

set b = n div (m mod n);

deffunc H_{1}( Nat, Nat, Nat) -> Element of omega = ((modSeq (m,n)) . $1) div ((modSeq (m,n)) . ($1 + 1));

ex b_{1} being sequence of NAT st

( b_{1} . 0 = m div n & b_{1} . 1 = n div (m mod n) & ( for k being Nat holds b_{1} . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) )

for b_{1}, b_{2} being sequence of NAT st b_{1} . 0 = m div n & b_{1} . 1 = n div (m mod n) & ( for k being Nat holds b_{1} . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) & b_{2} . 0 = m div n & b_{2} . 1 = n div (m mod n) & ( for k being Nat holds b_{2} . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) holds

b_{1} = b_{2}

end;
set a = m div n;

set b = n div (m mod n);

deffunc H

func divSeq (m,n) -> sequence of NAT means :Def2: :: REAL_3:def 2

( 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 ( 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)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines divSeq REAL_3:def 2 :

for m, n being Nat

for b_{3} being sequence of NAT holds

( b_{3} = divSeq (m,n) iff ( b_{3} . 0 = m div n & b_{3} . 1 = n div (m mod n) & ( for k being Nat holds b_{3} . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) ) );

for m, n being Nat

for b

( b

Lm2: for a, n, m 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, n, m being Nat holds

( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 )

( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 )

proof end;

Lm3: for a, n, m being Nat st (modSeq (m,n)) . a = 0 holds

(divSeq (m,n)) . (a + 1) = 0

proof end;

set g = NAT --> 0;

Lm4: for n, m being Nat ex k being Nat st (modSeq (m,n)) . k = 0

proof end;

defpred S

definition

let r be Real;

ex b_{1} being Real_Sequence st

( b_{1} . 0 = r & ( for n being Nat holds b_{1} . (n + 1) = 1 / (frac (b_{1} . n)) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = r & ( for n being Nat holds b_{1} . (n + 1) = 1 / (frac (b_{1} . n)) ) & b_{2} . 0 = r & ( for n being Nat holds b_{2} . (n + 1) = 1 / (frac (b_{2} . n)) ) holds

b_{1} = b_{2}

end;
func remainders_for_scf r -> Real_Sequence means :Def3: :: REAL_3:def 3

( it . 0 = r & ( for n being Nat holds it . (n + 1) = 1 / (frac (it . n)) ) );

existence ( it . 0 = r & ( for n being Nat holds it . (n + 1) = 1 / (frac (it . n)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines remainders_for_scf REAL_3:def 3 :

for r being Real

for b_{2} being Real_Sequence holds

( b_{2} = remainders_for_scf r iff ( b_{2} . 0 = r & ( for n being Nat holds b_{2} . (n + 1) = 1 / (frac (b_{2} . n)) ) ) );

for r being Real

for b

( b

definition

let r be Real;

ex b_{1} being Integer_Sequence st

for n being Nat holds b_{1} . n = [\((rfs r) . n)/]

for b_{1}, b_{2} being Integer_Sequence st ( for n being Nat holds b_{1} . n = [\((rfs r) . n)/] ) & ( for n being Nat holds b_{2} . n = [\((rfs r) . n)/] ) holds

b_{1} = b_{2}

end;
func SimpleContinuedFraction r -> Integer_Sequence means :Def4: :: REAL_3:def 4

for n being Nat holds it . n = [\((rfs r) . n)/];

existence for n being Nat holds it . n = [\((rfs r) . n)/];

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines SimpleContinuedFraction REAL_3:def 4 :

for r being Real

for b_{2} being Integer_Sequence holds

( b_{2} = SimpleContinuedFraction r iff for n being Nat holds b_{2} . n = [\((rfs r) . n)/] );

for r being Real

for b

( b

Lm5: 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

theorem :: REAL_3:32

Lm6: for n being Nat

for r being Real 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 :: REAL_3:39

theorem Th41: :: REAL_3:41

for k, n, m 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)) )

( (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 holds

( r is rational iff ex n being Nat st

for m being Nat st m >= n holds

(scf r) . m = 0 )

( r is rational iff ex n being Nat st

for m being Nat st m >= n holds

(scf r) . m = 0 )

proof end;

definition

let r be Real;

ex b_{1} being Real_Sequence st

( b_{1} . 0 = (scf r) . 0 & b_{1} . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b_{1} . (n + 2) = (((scf r) . (n + 2)) * (b_{1} . (n + 1))) + (b_{1} . n) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = (scf r) . 0 & b_{1} . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b_{1} . (n + 2) = (((scf r) . (n + 2)) * (b_{1} . (n + 1))) + (b_{1} . n) ) & b_{2} . 0 = (scf r) . 0 & b_{2} . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b_{2} . (n + 2) = (((scf r) . (n + 2)) * (b_{2} . (n + 1))) + (b_{2} . n) ) holds

b_{1} = b_{2}

end;
func convergent_numerators r -> Real_Sequence means :Def5: :: REAL_3:def 5

( 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 ( 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) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines convergent_numerators REAL_3:def 5 :

for r being Real

for b_{2} being Real_Sequence holds

( b_{2} = convergent_numerators r iff ( b_{2} . 0 = (scf r) . 0 & b_{2} . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b_{2} . (n + 2) = (((scf r) . (n + 2)) * (b_{2} . (n + 1))) + (b_{2} . n) ) ) );

for r being Real

for b

( b

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

definition

let r be Real;

set s = scf r;

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 1 & b_{1} . 1 = (scf r) . 1 & ( for n being Nat holds b_{1} . (n + 2) = (((scf r) . (n + 2)) * (b_{1} . (n + 1))) + (b_{1} . n) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = 1 & b_{1} . 1 = (scf r) . 1 & ( for n being Nat holds b_{1} . (n + 2) = (((scf r) . (n + 2)) * (b_{1} . (n + 1))) + (b_{1} . n) ) & b_{2} . 0 = 1 & b_{2} . 1 = (scf r) . 1 & ( for n being Nat holds b_{2} . (n + 2) = (((scf r) . (n + 2)) * (b_{2} . (n + 1))) + (b_{2} . n) ) holds

b_{1} = b_{2}

end;
set s = scf r;

func convergent_denominators r -> Real_Sequence means :Def6: :: REAL_3:def 6

( 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 ( 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) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines convergent_denominators REAL_3:def 6 :

for r being Real

for b_{2} being Real_Sequence holds

( b_{2} = convergent_denominators r iff ( b_{2} . 0 = 1 & b_{2} . 1 = (scf r) . 1 & ( for n being Nat holds b_{2} . (n + 2) = (((scf r) . (n + 2)) * (b_{2} . (n + 1))) + (b_{2} . n) ) ) );

for r being Real

for b

( b

notation

let r be Real;

synonym c_n r for convergent_numerators r;

synonym c_d r for convergent_denominators r;

end;
synonym c_n r for convergent_numerators r;

synonym c_d r for convergent_denominators r;

theorem :: REAL_3:46

for r being Real 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))

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

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

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 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

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 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)

for r being Real 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 :: REAL_3:53

for n being Nat

for r being Real holds (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1))

for r being Real 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 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))

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 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))

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 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)

for r being Real 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

for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds

n1 gcd n2 = 1

for r being Real

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 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))

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 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))

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 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)

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 st ( for n being Nat holds (scf r) . n <> 0 ) holds

for n being Nat holds (c_d r) . (n + 1) >= tau |^ n

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 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

for r being Real 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 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))

for r being Real 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 holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n

for r being Real 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 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))

for r being Real 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 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))

for r being Real 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 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))

for r being Real 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 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)))

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 st ( for n being Nat holds (c_d r) . n <> 0 ) holds

for n being Nat 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)).|

for n being Nat 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 end;

theorem :: REAL_3:70

for r being Real 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))

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;

(c_n r) /" (c_d r) is Real_Sequence ;

end;
:: Convergents of continued fraction

func convergents_of_continued_fractions r -> Real_Sequence equals :: REAL_3:def 7

(c_n r) /" (c_d r);

coherence (c_n r) /" (c_d r);

(c_n r) /" (c_d r) is Real_Sequence ;

:: deftheorem defines convergents_of_continued_fractions REAL_3:def 7 :

for r being Real holds convergents_of_continued_fractions r = (c_n r) /" (c_d r);

for r being Real holds convergents_of_continued_fractions r = (c_n r) /" (c_d r);

theorem Th73: :: REAL_3:73

for r being Real 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))))

(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 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))))))

(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 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))

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 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))

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 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))

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;

set s = scf r;

ex b_{1} being Real_Sequence st

( b_{1} . 0 = (scf r) . 0 & ( for n being Nat holds b_{1} . (n + 1) = (1 / (b_{1} . n)) + ((scf r) . (n + 1)) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = (scf r) . 0 & ( for n being Nat holds b_{1} . (n + 1) = (1 / (b_{1} . n)) + ((scf r) . (n + 1)) ) & b_{2} . 0 = (scf r) . 0 & ( for n being Nat holds b_{2} . (n + 1) = (1 / (b_{2} . n)) + ((scf r) . (n + 1)) ) holds

b_{1} = b_{2}

end;
set s = scf r;

func backContinued_fraction r -> Real_Sequence means :Def8: :: REAL_3:def 8

( it . 0 = (scf r) . 0 & ( for n being Nat holds it . (n + 1) = (1 / (it . n)) + ((scf r) . (n + 1)) ) );

existence ( it . 0 = (scf r) . 0 & ( for n being Nat holds it . (n + 1) = (1 / (it . n)) + ((scf r) . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines backContinued_fraction REAL_3:def 8 :

for r being Real

for b_{2} being Real_Sequence holds

( b_{2} = backContinued_fraction r iff ( b_{2} . 0 = (scf r) . 0 & ( for n being Nat holds b_{2} . (n + 1) = (1 / (b_{2} . n)) + ((scf r) . (n + 1)) ) ) );

for r being Real

for b

( b

theorem :: REAL_3:78

for r being Real st (scf r) . 0 > 0 holds

for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n)

for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n)

proof end;