begin
Lm1:
now for n being Nat st n > 1 holds
n - 1 is Nat
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
begin
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));
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;
Lm3:
for m, n, a being Nat holds
( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
Lm4:
for m, n, a being Nat st (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . (a + 1) = 0
set g = NAT --> 0;
Lm5:
dom (NAT --> 0) = NAT
by FUNCOP_1:13;
Lm6:
for m, n being Nat ex k being Nat st (modSeq (m,n)) . k = 0
begin
defpred S1[ set , Element of REAL , set ] means $3 = 1 / (frac $2);
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 )
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) )
begin