:: Simple Continued Fractions and Their Convergents
:: by Bo Li , Yan Zhang and Artur Korni{\l}owicz
::
:: Received August 18, 2006
:: Copyright (c) 2006 Association of Mizar Users
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
theorem Th1: :: REAL_3:1
theorem Th2: :: REAL_3:2
theorem :: REAL_3:3
theorem Th4: :: REAL_3:4
theorem Th5: :: REAL_3:5
theorem Th6: :: REAL_3:6
theorem Th7: :: REAL_3:7
theorem Th8: :: REAL_3:8
theorem Th9: :: REAL_3:9
theorem :: REAL_3:10
theorem :: REAL_3:11
:: deftheorem REAL_3:def 1 :
canceled;
:: deftheorem Def2 defines modSeq REAL_3:def 2 :
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)) ) )
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
end;
:: deftheorem Def3 defines divSeq REAL_3:def 3 :
theorem Th12: :: REAL_3:12
theorem Th13: :: REAL_3:13
theorem Th14: :: REAL_3:14
Lm3:
for m, n, a being Nat holds
( (modSeq m,n) . a > (modSeq m,n) . (a + 1) or (modSeq m,n) . a = 0 )
theorem Th15: :: REAL_3:15
theorem Th16: :: REAL_3:16
Lm4:
for m, n, a being Nat st (modSeq m,n) . a = 0 holds
(divSeq m,n) . (a + 1) = 0
theorem Th17: :: REAL_3:17
theorem Th18: :: REAL_3:18
theorem Th19: :: REAL_3:19
theorem :: REAL_3:20
set g = NAT --> 0 ;
Lm5:
dom (NAT --> 0 ) = NAT
by FUNCOP_1:19;
theorem Th21: :: REAL_3:21
theorem Th22: :: REAL_3:22
theorem :: REAL_3:23
theorem :: REAL_3:24
Lm6:
for m, n being Nat ex k being Nat st (modSeq m,n) . k = 0
theorem Th25: :: REAL_3:25
defpred S1[ set , Element of REAL , set ] means $3 = 1 / (frac $2);
:: deftheorem Def4 defines remainders_for_scf REAL_3:def 4 :
:: deftheorem Def5 defines SimpleContinuedFraction REAL_3:def 5 :
theorem Th26: :: REAL_3:26
theorem Th27: :: REAL_3:27
theorem :: REAL_3:28
theorem Th29: :: REAL_3:29
theorem Th30: :: REAL_3:30
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 )
theorem :: REAL_3:31
theorem :: REAL_3:32
theorem Th33: :: REAL_3:33
theorem Th34: :: REAL_3:34
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) )
theorem Th35: :: REAL_3:35
theorem :: REAL_3:36
theorem Th37: :: REAL_3:37
theorem Th38: :: REAL_3:38
theorem :: REAL_3:39
theorem Th40: :: REAL_3:40
theorem Th41: :: REAL_3:41
theorem Th42: :: REAL_3:42
theorem :: REAL_3:43
:: deftheorem Def6 defines convergent_numerators REAL_3:def 6 :
:: deftheorem Def7 defines convergent_denominators REAL_3:def 7 :
theorem Th44: :: REAL_3:44
theorem Th45: :: REAL_3:45
theorem :: REAL_3:46
theorem :: REAL_3:47
theorem :: REAL_3:48
theorem :: REAL_3:49
theorem Th50: :: REAL_3:50
theorem Th51: :: REAL_3:51
theorem Th52: :: REAL_3:52
theorem :: REAL_3:53
theorem :: REAL_3:54
theorem :: REAL_3:55
theorem :: REAL_3:56
theorem :: REAL_3:57
theorem Th58: :: REAL_3:58
theorem :: REAL_3:59
theorem :: REAL_3:60
theorem :: REAL_3:61
theorem :: REAL_3:62
theorem :: REAL_3:63
theorem Th64: :: REAL_3:64
theorem Th65: :: REAL_3:65
theorem Th66: :: REAL_3:66
theorem :: REAL_3:67
theorem :: REAL_3:68
theorem :: REAL_3:69
theorem :: REAL_3:70
:: deftheorem defines convergents_of_continued_fractions REAL_3:def 8 :
theorem :: REAL_3:71
theorem Th72: :: REAL_3:72
theorem Th73: :: REAL_3:73
theorem Th74: :: REAL_3:74
theorem :: REAL_3:75
theorem :: REAL_3:76
theorem :: REAL_3:77
:: deftheorem Def9 defines backContinued_fraction REAL_3:def 9 :
theorem :: REAL_3:78