begin
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:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem
begin
:: 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:
(
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:
theorem Th13:
theorem Th14:
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:
theorem Th16:
Lm4:
for m, n, a being Nat st (modSeq m,n) . a = 0 holds
(divSeq m,n) . (a + 1) = 0
theorem Th17:
theorem Th18:
theorem Th19:
theorem
set g = NAT --> 0 ;
Lm5:
dom (NAT --> 0 ) = NAT
by FUNCOP_1:19;
theorem Th21:
theorem Th22:
theorem
theorem
Lm6:
for m, n being Nat ex k being Nat st (modSeq m,n) . k = 0
theorem Th25:
begin
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:
theorem Th27:
theorem
theorem Th29:
theorem Th30:
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
theorem
theorem Th33:
theorem Th34:
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:
theorem
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem
begin
:: deftheorem Def6 defines convergent_numerators REAL_3:def 6 :
:: deftheorem Def7 defines convergent_denominators REAL_3:def 7 :
theorem Th44:
theorem Th45:
theorem
theorem
theorem
theorem
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem Th58:
theorem
theorem
theorem
theorem
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem
theorem
theorem
:: deftheorem defines convergents_of_continued_fractions REAL_3:def 8 :
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem
theorem
theorem
:: deftheorem Def9 defines backContinued_fraction REAL_3:def 9 :
theorem