begin
Lm1:
for n, m being Element of NAT st n < m holds
ex k being Element of NAT st m = (n + 1) + k
Lm2:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n < seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) ) )
Lm3:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )
Lm4:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n <= seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) & ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) ) )
Lm5:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) <= seq . n ) implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) & ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n ) )
Lm6:
for f being Real_Sequence holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
Lm7:
for f being Real_Sequence holds
( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )
Lm8:
for f being Real_Sequence holds
( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) )
Lm9:
for f being Real_Sequence holds
( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) )
Lm10:
( incl NAT is increasing & incl NAT is natural-valued )
Lm11:
( id NAT is increasing & id NAT is natural-valued )
;
Lm12:
for f being sequence of NAT holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
begin
theorem Th41:
for
r,
s being
Real holds
(
abs (r - s) = 1 iff ( (
r > s &
r = s + 1 ) or (
r < s &
s = r + 1 ) ) )
:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES
::