:: Monotone Real Sequences. Subsequences :: by Jaros{\l}aw Kotowicz :: :: Received November 23, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for n, m being Element of NAT st n < m holds ex k being Element of NAT st m = (n + 1) + k proofend; 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) ) ) proofend; 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 ) ) proofend; 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) ) ) proofend; 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 ) ) proofend; definition let f be NAT -defined REAL -valued Function; redefine attr f is increasing means :Def1: :: SEQM_3:def 1 for m, n being Element of NAT st m in dom f & n in dom f & m < n holds f . m < f . n; compatibility ( f is increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds f . m < f . n ) proofend; redefine attr f is decreasing means :Def2: :: SEQM_3:def 2 for m, n being Element of NAT st m in dom f & n in dom f & m < n holds f . m > f . n; compatibility ( f is decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds f . m > f . n ) proofend; redefine attr f is non-decreasing means :Def3: :: SEQM_3:def 3 for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds f . m <= f . n; compatibility ( f is non-decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds f . m <= f . n ) proofend; redefine attr f is non-increasing means :Def4: :: SEQM_3:def 4 for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds f . m >= f . n; compatibility ( f is non-increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds f . m >= f . n ) proofend; end; :: deftheorem Def1 defines increasing SEQM_3:def_1_:_ for f being NAT -defined REAL -valued Function holds ( f is increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds f . m < f . n ); :: deftheorem Def2 defines decreasing SEQM_3:def_2_:_ for f being NAT -defined REAL -valued Function holds ( f is decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds f . m > f . n ); :: deftheorem Def3 defines non-decreasing SEQM_3:def_3_:_ for f being NAT -defined REAL -valued Function holds ( f is non-decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds f . m <= f . n ); :: deftheorem Def4 defines non-increasing SEQM_3:def_4_:_ for f being NAT -defined REAL -valued Function holds ( f is non-increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds f . m >= f . n ); Lm6: for f being Real_Sequence holds ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) proofend; Lm7: for f being Real_Sequence holds ( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) ) proofend; Lm8: for f being Real_Sequence holds ( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) ) proofend; Lm9: for f being Real_Sequence holds ( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) ) proofend; definition let seq be Real_Sequence; attrseq is monotone means :Def5: :: SEQM_3:def 5 ( seq is non-decreasing or seq is non-increasing ); end; :: deftheorem Def5 defines monotone SEQM_3:def_5_:_ for seq being Real_Sequence holds ( seq is monotone iff ( seq is non-decreasing or seq is non-increasing ) ); theorem Th1: :: SEQM_3:1 for seq being Real_Sequence holds ( seq is increasing iff for n, m being Element of NAT st n < m holds seq . n < seq . m ) proofend; theorem :: SEQM_3:2 for seq being Real_Sequence holds ( seq is increasing iff for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) proofend; theorem Th3: :: SEQM_3:3 for seq being Real_Sequence holds ( seq is decreasing iff for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) proofend; theorem Th4: :: SEQM_3:4 for seq being Real_Sequence holds ( seq is decreasing iff for n, m being Element of NAT st n < m holds seq . m < seq . n ) proofend; theorem Th5: :: SEQM_3:5 for seq being Real_Sequence holds ( seq is non-decreasing iff for n, k being Element of NAT holds seq . n <= seq . (n + k) ) proofend; theorem Th6: :: SEQM_3:6 for seq being Real_Sequence holds ( seq is non-decreasing iff for n, m being Element of NAT st n <= m holds seq . n <= seq . m ) proofend; theorem Th7: :: SEQM_3:7 for seq being Real_Sequence holds ( seq is non-increasing iff for n, k being Element of NAT holds seq . (n + k) <= seq . n ) proofend; theorem Th8: :: SEQM_3:8 for seq being Real_Sequence holds ( seq is non-increasing iff for n, m being Element of NAT st n <= m holds seq . m <= seq . n ) proofend; :: :: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES :: theorem :: SEQM_3:9 for seq being Real_Sequence st seq is increasing holds for n being Element of NAT st 0 < n holds seq . 0 < seq . n by Th1; theorem :: SEQM_3:10 for seq being Real_Sequence st seq is decreasing holds for n being Element of NAT st 0 < n holds seq . n < seq . 0 by Th4; theorem Th11: :: SEQM_3:11 for seq being Real_Sequence st seq is non-decreasing holds for n being Element of NAT holds seq . 0 <= seq . n by Th6; theorem Th12: :: SEQM_3:12 for seq being Real_Sequence st seq is non-increasing holds for n being Element of NAT holds seq . n <= seq . 0 by Th8; registration cluster Function-like constant -> non-decreasing non-increasing for Element of K19(K20(NAT,REAL)); coherence for b1 being PartFunc of NAT,REAL st b1 is constant holds ( b1 is non-decreasing & b1 is non-increasing ) proofend; cluster Function-like non-decreasing non-increasing -> constant for Element of K19(K20(NAT,REAL)); coherence for b1 being PartFunc of NAT,REAL st b1 is non-decreasing & b1 is non-increasing holds b1 is constant proofend; end; Lm10: ( incl NAT is increasing & incl NAT is natural-valued ) proofend; Lm11: ( id NAT is increasing & id NAT is natural-valued ) ; registration cluster Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued increasing for Element of K19(K20(NAT,REAL)); existence ex b1 being Real_Sequence st ( b1 is increasing & b1 is natural-valued ) by Lm10; end; registration cluster Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing for Element of K19(K20(NAT,NAT)); existence ex b1 being sequence of NAT st b1 is increasing by Lm11; end; Lm12: for f being sequence of NAT holds ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) proofend; theorem :: SEQM_3:13 for seq being Real_Sequence holds ( seq is sequence of NAT iff for n being Element of NAT holds seq . n is Element of NAT ) proofend; registration let Nseq be increasing sequence of NAT; let k be Element of NAT ; clusterNseq ^\ k -> ext-real-valued natural-valued increasing for ext-real-valued Function; coherence for b1 being ext-real-valued Function st b1 = Nseq ^\ k holds ( b1 is increasing & b1 is natural-valued ) proofend; end; definition let f be Real_Sequence; redefine attr f is increasing means :: SEQM_3:def 6 for n being Element of NAT holds f . n < f . (n + 1); compatibility ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) by Lm6; redefine attr f is decreasing means :: SEQM_3:def 7 for n being Element of NAT holds f . n > f . (n + 1); compatibility ( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) ) by Lm7; redefine attr f is non-decreasing means :: SEQM_3:def 8 for n being Element of NAT holds f . n <= f . (n + 1); compatibility ( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) ) by Lm8; redefine attr f is non-increasing means :: SEQM_3:def 9 for n being Element of NAT holds f . n >= f . (n + 1); compatibility ( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) ) by Lm9; end; :: deftheorem defines increasing SEQM_3:def_6_:_ for f being Real_Sequence holds ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ); :: deftheorem defines decreasing SEQM_3:def_7_:_ for f being Real_Sequence holds ( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) ); :: deftheorem defines non-decreasing SEQM_3:def_8_:_ for f being Real_Sequence holds ( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) ); :: deftheorem defines non-increasing SEQM_3:def_9_:_ for f being Real_Sequence holds ( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) ); theorem :: SEQM_3:14 for Nseq being increasing sequence of NAT for n being Element of NAT holds n <= Nseq . n proofend; registration let s be Real_Sequence; let k be Nat; clusters ^\ k -> real-valued ; coherence s ^\ k is real-valued ; end; theorem Th15: :: SEQM_3:15 for k being Element of NAT for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) proofend; theorem Th16: :: SEQM_3:16 for k being Element of NAT for seq being Real_Sequence holds (- seq) ^\ k = - (seq ^\ k) proofend; theorem :: SEQM_3:17 for k being Element of NAT for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) proofend; theorem Th18: :: SEQM_3:18 for k being Element of NAT for seq being Real_Sequence holds (seq ") ^\ k = (seq ^\ k) " proofend; theorem Th19: :: SEQM_3:19 for k being Element of NAT for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) proofend; theorem :: SEQM_3:20 for k being Element of NAT for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k) proofend; theorem :: SEQM_3:21 for k being Element of NAT for r being real number for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k) proofend; :: :: SUBSEQUENCES OF MONOTONE SEQUENCE :: SUBSEQUENCE OF BOUNDED SEQUENCE :: theorem :: SEQM_3:22 for seq, seq1 being Real_Sequence st seq is increasing & seq1 is subsequence of seq holds seq1 is increasing proofend; theorem :: SEQM_3:23 for seq, seq1 being Real_Sequence st seq is decreasing & seq1 is subsequence of seq holds seq1 is decreasing proofend; theorem Th24: :: SEQM_3:24 for seq, seq1 being Real_Sequence st seq is non-decreasing & seq1 is subsequence of seq holds seq1 is non-decreasing proofend; theorem Th25: :: SEQM_3:25 for seq, seq1 being Real_Sequence st seq is non-increasing & seq1 is subsequence of seq holds seq1 is non-increasing proofend; theorem :: SEQM_3:26 for seq, seq1 being Real_Sequence st seq is monotone & seq1 is subsequence of seq holds seq1 is monotone proofend; theorem Th27: :: SEQM_3:27 for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is subsequence of seq holds seq1 is bounded_above proofend; theorem Th28: :: SEQM_3:28 for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is subsequence of seq holds seq1 is bounded_below proofend; theorem :: SEQM_3:29 for seq, seq1 being Real_Sequence st seq is bounded & seq1 is subsequence of seq holds seq1 is bounded proofend; :: :: OPERATIONS ON MONOTONE SEQUENCES :: theorem :: SEQM_3:30 for r being real number for seq being Real_Sequence holds ( ( seq is increasing & 0 < r implies r (#) seq is increasing ) & ( 0 = r implies r (#) seq is constant ) & ( seq is increasing & r < 0 implies r (#) seq is decreasing ) ) proofend; theorem :: SEQM_3:31 for r being real number for seq being Real_Sequence holds ( ( seq is decreasing & 0 < r implies r (#) seq is decreasing ) & ( seq is decreasing & r < 0 implies r (#) seq is increasing ) ) proofend; theorem :: SEQM_3:32 for r being real number for seq being Real_Sequence holds ( ( seq is non-decreasing & 0 <= r implies r (#) seq is non-decreasing ) & ( seq is non-decreasing & r <= 0 implies r (#) seq is non-increasing ) ) proofend; theorem :: SEQM_3:33 for r being real number for seq being Real_Sequence holds ( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) ) proofend; theorem Th34: :: SEQM_3:34 for seq, seq1 being Real_Sequence holds ( ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) ) proofend; theorem :: SEQM_3:35 for seq, seq1 being Real_Sequence holds ( ( seq is increasing & seq1 is constant implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is constant implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing ) ) proofend; :: :: OPERATIONS ON BOUNDED SEQUENCES :: theorem Th36: :: SEQM_3:36 for r being real number for seq being Real_Sequence holds ( ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) & ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) ) proofend; theorem :: SEQM_3:37 for seq being Real_Sequence holds ( ( seq is bounded implies for r being real number holds r (#) seq is bounded ) & ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) ) proofend; :: :: OPERATIONS ON BOUNDED & MONOTONE SEQUENCES :: theorem :: SEQM_3:38 for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is non-increasing holds seq + seq1 is bounded_above proofend; theorem :: SEQM_3:39 for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is non-decreasing holds seq + seq1 is bounded_below proofend; theorem :: SEQM_3:40 ( incl NAT is increasing & incl NAT is natural-valued ) by Lm10; registration cluster -> natural-valued for FinSequence of NAT ; coherence for b1 being FinSequence of NAT holds b1 is natural-valued ; end; begin theorem Th41: :: SEQM_3:41 for r, s being Real holds ( abs (r - s) = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ) proofend; theorem :: SEQM_3:42 for i, j, n, m being Element of NAT holds ( (abs (i - j)) + (abs (n - m)) = 1 iff ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ) proofend; theorem :: SEQM_3:43 for n being Element of NAT holds ( n > 1 iff ex m being Element of NAT st ( n = m + 1 & m > 0 ) ) proofend; theorem :: SEQM_3:44 for f being FinSequence for n, m, k being Element of NAT st len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k holds (Del (f,n)) . k = f . (k + 1) proofend; definition let f be FinSequence; redefine attr f is constant means :: SEQM_3:def 10 for n, m being Element of NAT st n in dom f & m in dom f holds f . n = f . m; compatibility ( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds f . n = f . m ) proofend; end; :: deftheorem defines constant SEQM_3:def_10_:_ for f being FinSequence holds ( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds f . n = f . m ); registration cluster -> real-valued for FinSequence of REAL ; coherence for b1 being FinSequence of REAL holds b1 is real-valued ; end; registration cluster Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued increasing V54() FinSequence-like FinSubsequence-like for FinSequence of REAL ; existence ex b1 being FinSequence of REAL st ( not b1 is empty & b1 is increasing ) proofend; end; registration cluster Relation-like NAT -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued V54() FinSequence-like FinSubsequence-like for FinSequence of REAL ; existence ex b1 being FinSequence of REAL st b1 is constant proofend; end; theorem Th45: :: SEQM_3:45 for v being FinSequence of REAL for n, i, m being Element of NAT st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Element of NAT st k in dom v & v . k = i holds k <= m ) holds ( m + 1 in dom v & v . (m + 1) = i + 1 ) proofend; theorem :: SEQM_3:46 for v being FinSequence of REAL for n being Element of NAT st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds r = s ) holds ( ( for i being Element of NAT st i in Seg n holds ex k being Element of NAT st ( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds j <= m ) & m < k & k in dom v & r = v . k holds i < r ) ) proofend;