environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, ARYTM_3, NAT_1, CARD_1, FUNCT_1, XXREAL_0, PARTFUN1, ORDINAL2, RELAT_1, TARSKI, VALUED_0, ARYTM_1, VALUED_1, XXREAL_2, REAL_1, COMPLEX1, FINSEQ_1, SEQM_3, XBOOLE_0, FINSEQ_3, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_3, FINSEQ_1, FINSEQ_3, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, REAL_1, COMPLEX1, NAT_1, VALUED_0;
definitions TARSKI, SEQ_2, FUNCT_1, VALUED_0;
theorems FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, FUNCT_2, XREAL_1, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, RELAT_1, COMPLEX1, INT_1, FINSEQ_1, FINSEQ_3, XBOOLE_1, TARSKI, NUMBERS;
schemes NAT_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_0, FUNCT_2, VALUED_1, SEQ_2, RFUNCT_1, RELAT_1, NAT_1, FINSEQ_1, CARD_1, INT_1;
constructors HIDDEN, PARTFUN1, FUNCT_3, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, FINSEQ_1, RECDEF_1, RELSET_1, FINSEQ_3, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
expansions SEQ_2, FUNCT_1, VALUED_0, VALUED_1;
Lm1:
for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k
Lm2:
for seq being Real_Sequence holds
( ( ( for n being Nat holds seq . n < seq . (n + 1) ) implies for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Nat st n < m holds
seq . n < seq . m ) & ( ( for n, m being Nat st n < m holds
seq . n < seq . m ) implies for n being Nat holds seq . n < seq . (n + 1) ) )
Lm3:
for seq being Real_Sequence holds
( ( ( for n being Nat holds seq . (n + 1) < seq . n ) implies for n, k being Nat holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Nat holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Nat st n < m holds
seq . m < seq . n ) & ( ( for n, m being Nat st n < m holds
seq . m < seq . n ) implies for n being Nat holds seq . (n + 1) < seq . n ) )
Lm4:
for seq being Real_Sequence holds
( ( ( for n being Nat holds seq . n <= seq . (n + 1) ) implies for n, k being Nat holds seq . n <= seq . (n + k) ) & ( ( for n, k being Nat holds seq . n <= seq . (n + k) ) implies for n, m being Nat st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Nat st n <= m holds
seq . n <= seq . m ) implies for n being Nat holds seq . n <= seq . (n + 1) ) )
Lm5:
for seq being Real_Sequence holds
( ( ( for n being Nat holds seq . (n + 1) <= seq . n ) implies for n, k being Nat holds seq . (n + k) <= seq . n ) & ( ( for n, k being Nat holds seq . (n + k) <= seq . n ) implies for n, m being Nat st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Nat st n <= m holds
seq . m <= seq . n ) implies for n being Nat holds seq . (n + 1) <= seq . n ) )
Lm6:
( id NAT is increasing & id NAT is natural-valued )
;
Lm7:
for f being sequence of NAT holds
( f is increasing iff for n being Nat holds f . n < f . (n + 1) )
;
theorem Th40:
for
r,
s being
Real holds
(
|.(r - s).| = 1 iff ( (
r > s &
r = s + 1 ) or (
r < s &
s = r + 1 ) ) )
theorem
for
n being
Nat holds
(
n > 1 iff ex
m being
Nat st
(
n = m + 1 &
m > 0 ) )
:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES
::