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 ) )
:: deftheorem Def1 defines increasing SEQM_3:def 1 :
:: deftheorem Def2 defines decreasing SEQM_3:def 2 :
:: deftheorem Def3 defines non-decreasing SEQM_3:def 3 :
:: deftheorem Def4 defines non-increasing SEQM_3:def 4 :
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) )
:: deftheorem SEQM_3:def 5 :
canceled;
:: deftheorem SEQM_3:def 6 :
canceled;
:: deftheorem Def7 defines monotone SEQM_3:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th21:
theorem Th22:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
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) )
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
:: deftheorem SEQM_3:def 8 :
canceled;
:: deftheorem SEQM_3:def 9 :
canceled;
:: deftheorem SEQM_3:def 10 :
canceled;
:: deftheorem defines increasing SEQM_3:def 11 :
:: deftheorem defines decreasing SEQM_3:def 12 :
:: deftheorem defines non-decreasing SEQM_3:def 13 :
:: deftheorem defines non-increasing SEQM_3:def 14 :
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th37:
theorem Th38:
theorem
theorem
canceled;
theorem Th41:
theorem Th42:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th51:
theorem Th52:
theorem
theorem
canceled;
theorem
canceled;
theorem Th56:
theorem Th57:
theorem
theorem
theorem
theorem
theorem
theorem Th63:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th68:
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem