environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, XREAL_0, ORDINAL1, RAT_1, XCMPLX_0, FUNCT_1, XXREAL_0, ARYTM_1, ARYTM_3, CARD_1, RELAT_1, SUBSET_1, SEQ_1, FUNCOP_1, TARSKI, IRRAT_1, REAL_1, INT_2, FIB_NUM, NEWTON, SQUARE_1, COMPLEX1, POWER, VALUED_1, REAL_3, FUNCT_7;
notations HIDDEN, TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, VALUED_0, XCMPLX_0, COMPLEX1, REAL_1, XXREAL_0, XREAL_0, RAT_1, SQUARE_1, INT_1, NAT_D, RELAT_1, RELSET_1, FUNCOP_1, VALUED_1, SEQ_1, FUNCT_2, NEWTON, NAT_1, FIB_NUM, POWER, IRRAT_1;
definitions TARSKI, FUNCT_2;
theorems INT_1, XREAL_0, ORDINAL1, XCMPLX_0, FUNCT_2, XCMPLX_1, FUNCT_1, NAT_1, RAT_1, NAT_2, FUNCOP_1, XREAL_1, NEWTON, SEQ_1, ABSVALUE, COMPLEX1, PREPOWER, WSIERP_1, SQUARE_1, EULER_1, FIB_NUM, POWER, SERIES_1, XXREAL_0, NAT_D, VALUED_1, RELSET_1, RELAT_1;
schemes NAT_1, RECDEF_1, RECDEF_2, FIB_NUM, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1, MEMBERED, NEWTON, VALUED_0, VALUED_1, FUNCT_2;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, NAT_D, NEWTON, POWER, FUNCOP_1, BINARITH, FIB_NUM, VALUED_1, PARTFUN1, RELSET_1, NUMBERS;
requirements HIDDEN, BOOLE, REAL, SUBSET, NUMERALS, ARITHM;
equalities VALUED_1, SQUARE_1, INT_1, XCMPLX_0;
expansions TARSKI, FUNCT_2, INT_1;
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
theorem Th1:
for
r being
Real st
0 < r &
r < 1 holds
1
< 1
/ r
definition
let m,
n be
Nat;
set a =
m div n;
set b =
n div (m mod n);
deffunc H1(
Nat,
Nat,
Nat)
-> Element of
omega =
((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;
Lm2:
for a, n, m being Nat holds
( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
Lm3:
for a, n, m being Nat st (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . (a + 1) = 0
set g = NAT --> 0;
Lm4:
for n, m being Nat ex k being Nat st (modSeq (m,n)) . k = 0
defpred S1[ set , Element of REAL , object ] means $3 = 1 / (frac $2);
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 )
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) )
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;