:: SEQM_3 semantic presentation

Lm1: for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k

proof end;

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) ) )

proof end;

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 ) )

proof end;

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) ) )

proof end;

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 ) )

proof end;

definition

let f be PartFunc of NAT , REAL ;
attr f is increasing means :Def1: :: SEQM_3:def 1
for m, n being Nat st m in dom f & n in dom f & m < n holds
f . m < f . n;
attr f is decreasing means :Def2: :: SEQM_3:def 2
for m, n being Nat st m in dom f & n in dom f & m < n holds
f . m > f . n;
attr f is non-decreasing means :Def3: :: SEQM_3:def 3
for m, n being Nat st m in dom f & n in dom f & m <= n holds
f . m <= f . n;
attr f is non-increasing means :Def4: :: SEQM_3:def 4
for m, n being Nat st m in dom f & n in dom f & m <= n holds
f . m >= f . n;

end;

:: 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 Nat holds f . n < f . (n + 1) )

proof end;

Lm7: for f being Real_Sequence holds
( f is decreasing iff for n being Nat holds f . n > f . (n + 1) )

proof end;

Lm8: for f being Real_Sequence holds
( f is non-decreasing iff for n being Nat holds f . n <= f . (n + 1) )

proof end;

Lm9: for f being Real_Sequence holds
( f is non-increasing iff for n being Nat holds f . n >= f . (n + 1) )

proof end;

definition

let f be Function;
attr f is constant means :Def5: :: SEQM_3:def 5
for n1, n2 being set st n1 in dom f & n2 in dom f holds
f . n1 = f . n2;

end;

:: deftheorem Def5 defines constant SEQM_3:def 5 :

definition

let seq be Real_Sequence;
redefine attr seq is constant means :Def6: :: SEQM_3:def 6
ex r being real number st
for n being Nat holds seq . n = r;
compatibility

proof end;

end;

:: deftheorem Def6 defines constant SEQM_3:def 6 :

definition

let seq be Real_Sequence;
attr seq is monotone means :Def7: :: SEQM_3:def 7
( seq is non-decreasing or seq is non-increasing );

end;

:: deftheorem Def7 defines monotone SEQM_3:def 7 :

theorem :: SEQM_3:1

canceled;

theorem :: SEQM_3:2

canceled;

theorem :: SEQM_3:3

canceled;

theorem :: SEQM_3:4

canceled;

theorem :: SEQM_3:5

canceled;

theorem :: SEQM_3:6

canceled;

theorem Th7: :: SEQM_3:7

for seq being Real_Sequence holds
( seq is increasing iff for n, m being Nat st n < m holds
seq . n < seq . m )

proof end;

theorem :: SEQM_3:8

for seq being Real_Sequence holds
( seq is increasing iff for n, k being Nat holds seq . n < seq . ((n + 1) + k) )

proof end;

theorem Th9: :: SEQM_3:9

for seq being Real_Sequence holds
( seq is decreasing iff for n, k being Nat holds seq . ((n + 1) + k) < seq . n )

proof end;

theorem Th10: :: SEQM_3:10

for seq being Real_Sequence holds
( seq is decreasing iff for n, m being Nat st n < m holds
seq . m < seq . n )

proof end;

theorem Th11: :: SEQM_3:11

for seq being Real_Sequence holds
( seq is non-decreasing iff for n, k being Nat holds seq . n <= seq . (n + k) )

proof end;

theorem Th12: :: SEQM_3:12

for seq being Real_Sequence holds
( seq is non-decreasing iff for n, m being Nat st n <= m holds
seq . n <= seq . m )

proof end;

theorem Th13: :: SEQM_3:13

for seq being Real_Sequence holds
( seq is non-increasing iff for n, k being Nat holds seq . (n + k) <= seq . n )

proof end;

theorem Th14: :: SEQM_3:14

for seq being Real_Sequence holds
( seq is non-increasing iff for n, m being Nat st n <= m holds
seq . m <= seq . n )

proof end;

Lm10: for seq being Real_Sequence holds
( ( ex r being real number st
for n being Nat holds seq . n = r implies ex r being real number st rng seq = {r} ) & ( ex r being real number st rng seq = {r} implies for n being Nat holds seq . n = seq . (n + 1) ) & ( ( 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 holds seq . n = seq . m ) & ( ( for n, m being Nat holds seq . n = seq . m ) implies ex r being real number st
for n being Nat holds seq . n = r ) )

proof end;

theorem Th15: :: SEQM_3:15

for seq being Real_Sequence holds
( seq is constant iff ex r being real number st rng seq = {r} )

proof end;

theorem Th16: :: SEQM_3:16

for seq being Real_Sequence holds
( seq is constant iff for n being Nat holds seq . n = seq . (n + 1) )

proof end;

theorem Th17: :: SEQM_3:17

for seq being Real_Sequence holds
( seq is constant iff for n, k being Nat holds seq . n = seq . (n + k) )

proof end;

theorem Th18: :: SEQM_3:18

for seq being Real_Sequence holds
( seq is constant iff for n, m being Nat holds seq . n = seq . m )

proof end;

theorem :: SEQM_3:19

for seq being Real_Sequence st seq is increasing holds
for n being Nat st 0 < n holds
seq . 0 < seq . n by Th7;

theorem :: SEQM_3:20

for seq being Real_Sequence st seq is decreasing holds
for n being Nat st 0 < n holds
seq . n < seq . 0 by Th10;

theorem Th21: :: SEQM_3:21

for seq being Real_Sequence st seq is non-decreasing holds
for n being Nat holds seq . 0 <= seq . n

proof end;

theorem Th22: :: SEQM_3:22

for seq being Real_Sequence st seq is non-increasing holds
for n being Nat holds seq . n <= seq . 0

proof end;

registration

cluster increasing -> non-decreasing M5( NAT , REAL );
coherence

proof end;

cluster decreasing -> non-increasing M5( NAT , REAL );
coherence

proof end;

cluster constant -> non-decreasing non-increasing M5( NAT , REAL );
coherence

proof end;

cluster non-decreasing non-increasing -> constant M5( NAT , REAL );
coherence

proof end;

end;

theorem :: SEQM_3:23

for seq being Real_Sequence st seq is increasing holds
seq is non-decreasing

proof end;

theorem :: SEQM_3:24

for seq being Real_Sequence st seq is decreasing holds
seq is non-increasing

proof end;

theorem Th25: :: SEQM_3:25

for seq being Real_Sequence st seq is constant holds
seq is non-decreasing

proof end;

theorem Th26: :: SEQM_3:26

for seq being Real_Sequence st seq is constant holds
seq is non-increasing

proof end;

theorem :: SEQM_3:27

for seq being Real_Sequence st seq is non-decreasing & seq is non-increasing holds
seq is constant

proof end;

definition

let IT be Relation;
attr IT is natural-yielding means :Def8: :: SEQM_3:def 8
rng IT c= NAT ;

end;

:: deftheorem Def8 defines natural-yielding SEQM_3:def 8 :

Lm11: ( incl NAT is increasing & incl NAT is natural-yielding )

proof end;

registration

cluster increasing non-decreasing natural-yielding M5( NAT , REAL );
existence by Lm11;

end;

definition

mode Seq_of_Nat is natural-yielding Real_Sequence;

end;

definition

let seq be Real_Sequence;
let k be Nat;
func seq ^\ k -> Real_Sequence means :Def9: :: SEQM_3:def 9
for n being Nat holds it . n = seq . (n + k);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines ^\ SEQM_3:def 9 :

theorem :: SEQM_3:28

canceled;

theorem Th29: :: SEQM_3:29

for seq being Real_Sequence holds
( seq is increasing Seq_of_Nat iff ( seq is increasing & ( for n being Nat holds seq . n is Nat ) ) )

proof end;

theorem :: SEQM_3:30

canceled;

theorem Th31: :: SEQM_3:31

for seq being Real_Sequence
for Nseq being increasing Seq_of_Nat
for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)

proof end;

definition

let Nseq be increasing Seq_of_Nat;
let n be Nat;
:: original: .
redefine func Nseq . n -> Nat;
coherence by Th29;

end;

definition

let Nseq be increasing Seq_of_Nat;
let seq be Real_Sequence;
:: original: *
redefine func seq * Nseq -> Real_Sequence;
coherence

proof end;

end;

definition

let Nseq, Nseq1 be increasing Seq_of_Nat;
:: original: *
redefine func Nseq1 * Nseq -> increasing Seq_of_Nat;
coherence

proof end;

end;

registration

let Nseq be increasing Seq_of_Nat;
let k be Nat;
cluster Nseq ^\ k -> increasing non-decreasing natural-yielding ;
coherence

proof end;

end;

definition

let seq be Real_Sequence;
mode subsequence of seq -> Real_Sequence means :Def10: :: SEQM_3:def 10
ex Nseq being increasing Seq_of_Nat st it = seq * Nseq;
existence

proof end;

end;

:: deftheorem Def10 defines subsequence SEQM_3:def 10 :

definition

let f be Real_Sequence;
redefine attr f is increasing means :: SEQM_3:def 11
for n being Nat holds f . n < f . (n + 1);
compatibility by Lm6;
redefine attr f is decreasing means :: SEQM_3:def 12
for n being Nat holds f . n > f . (n + 1);
compatibility by Lm7;
redefine attr f is non-decreasing means :: SEQM_3:def 13
for n being Nat holds f . n <= f . (n + 1);
compatibility by Lm8;
redefine attr f is non-increasing means :: SEQM_3:def 14
for n being Nat holds f . n >= f . (n + 1);
compatibility by Lm9;

end;

:: 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 :: SEQM_3:32

canceled;

theorem :: SEQM_3:33

for Nseq being increasing Seq_of_Nat
for n being Nat holds n <= Nseq . n

proof end;

theorem :: SEQM_3:34

for seq being Real_Sequence holds seq ^\ 0 = seq

proof end;

theorem :: SEQM_3:35

for k, m being Nat
for seq being Real_Sequence holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k

proof end;

theorem :: SEQM_3:36

for k, m being Nat
for seq being Real_Sequence holds (seq ^\ k) ^\ m = seq ^\ (k + m)

proof end;

theorem Th37: :: SEQM_3:37

for k being Nat
for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

proof end;

theorem Th38: :: SEQM_3:38

for k being Nat
for seq being Real_Sequence holds (- seq) ^\ k = - (seq ^\ k)

proof end;

theorem :: SEQM_3:39

for k being Nat
for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

proof end;

theorem :: SEQM_3:40

for k being Nat
for seq being Real_Sequence st seq is_not_0 holds
seq ^\ k is_not_0

proof end;

theorem Th41: :: SEQM_3:41

for k being Nat
for seq being Real_Sequence holds (seq " ) ^\ k = (seq ^\ k) "

proof end;

theorem Th42: :: SEQM_3:42

for k being Nat
for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)

proof end;

theorem :: SEQM_3:43

for k being Nat
for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)

proof end;

theorem :: SEQM_3:44

for k being Nat
for r being real number
for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)

proof end;

theorem :: SEQM_3:45

for k being Nat
for seq being Real_Sequence
for Nseq being increasing Seq_of_Nat holds (seq * Nseq) ^\ k = seq * (Nseq ^\ k)

proof end;

theorem :: SEQM_3:46

for seq being Real_Sequence holds seq is subsequence of seq

proof end;

theorem :: SEQM_3:47

for k being Nat
for seq being Real_Sequence holds seq ^\ k is subsequence of seq

proof end;

theorem :: SEQM_3:48

for seq, seq1, seq2 being Real_Sequence st seq is subsequence of seq1 & seq1 is subsequence of seq2 holds
seq is subsequence of seq2

proof end;

theorem :: SEQM_3:49

for seq, seq1 being Real_Sequence st seq is increasing & seq1 is subsequence of seq holds
seq1 is increasing

proof end;

theorem :: SEQM_3:50

for seq, seq1 being Real_Sequence st seq is decreasing & seq1 is subsequence of seq holds
seq1 is decreasing

proof end;

theorem Th51: :: SEQM_3:51

for seq, seq1 being Real_Sequence st seq is non-decreasing & seq1 is subsequence of seq holds
seq1 is non-decreasing

proof end;

theorem Th52: :: SEQM_3:52

for seq, seq1 being Real_Sequence st seq is non-increasing & seq1 is subsequence of seq holds
seq1 is non-increasing

proof end;

theorem :: SEQM_3:53

for seq, seq1 being Real_Sequence st seq is monotone & seq1 is subsequence of seq holds
seq1 is monotone

proof end;

theorem :: SEQM_3:54

for seq, seq1 being Real_Sequence st seq is constant & seq1 is subsequence of seq holds
seq1 is constant

proof end;

theorem :: SEQM_3:55

for seq, seq1 being Real_Sequence st seq is constant & seq1 is subsequence of seq holds
seq = seq1

proof end;

theorem Th56: :: SEQM_3:56

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is subsequence of seq holds
seq1 is bounded_above

proof end;

theorem Th57: :: SEQM_3:57

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is subsequence of seq holds
seq1 is bounded_below

proof end;

theorem :: SEQM_3:58

for seq, seq1 being Real_Sequence st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded

proof end;

theorem :: SEQM_3:59

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 ) )

proof end;

theorem :: SEQM_3:60

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 ) )

proof end;

theorem :: SEQM_3:61

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 ) )

proof end;

theorem :: SEQM_3:62

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 ) )

proof end;

theorem Th63: :: SEQM_3:63

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 ) )

proof end;

theorem :: SEQM_3:64

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 ) )

proof end;

theorem Th65: :: SEQM_3:65

for seq being Real_Sequence st seq is constant holds
( ( for r being real number holds r (#) seq is constant ) & - seq is constant & abs seq is constant )

proof end;

theorem Th66: :: SEQM_3:66

for seq, seq1 being Real_Sequence st seq is constant & seq1 is constant holds
( seq (#) seq1 is constant & seq + seq1 is constant )

proof end;

theorem :: SEQM_3:67

for seq, seq1 being Real_Sequence st seq is constant & seq1 is constant holds
seq - seq1 is constant

proof end;

theorem Th68: :: SEQM_3:68

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 ) )

proof end;

theorem Th69: :: SEQM_3:69

for r being real number
for seq being Real_Sequence holds
( ( seq is bounded_below & 0 < r implies r (#) seq is bounded_below ) & ( seq is bounded_below & r < 0 implies r (#) seq is bounded_above ) )

proof end;

theorem Th70: :: SEQM_3:70

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 ) )

proof end;

theorem Th71: :: SEQM_3:71

for seq, seq1 being Real_Sequence holds
( ( seq is bounded_above & seq1 is bounded_above implies seq + seq1 is bounded_above ) & ( seq is bounded_below & seq1 is bounded_below implies seq + seq1 is bounded_below ) & ( seq is bounded & seq1 is bounded implies seq + seq1 is bounded ) )

proof end;

theorem Th72: :: SEQM_3:72

for seq, seq1 being Real_Sequence st seq is bounded & seq1 is bounded holds
( seq (#) seq1 is bounded & seq - seq1 is bounded )

proof end;

theorem Th73: :: SEQM_3:73

for seq being Real_Sequence st seq is constant holds
seq is bounded

proof end;

theorem :: SEQM_3:74

for seq being Real_Sequence st seq is constant holds
( ( for r being real number holds r (#) seq is bounded ) & - seq is bounded & abs seq is bounded )

proof end;

theorem Th75: :: SEQM_3:75

for seq, seq1 being Real_Sequence holds
( ( seq is bounded_above & seq1 is constant implies seq + seq1 is bounded_above ) & ( seq is bounded_below & seq1 is constant implies seq + seq1 is bounded_below ) & ( seq is bounded & seq1 is constant implies seq + seq1 is bounded ) )

proof end;

theorem :: SEQM_3:76

for seq, seq1 being Real_Sequence holds
( ( seq is bounded_above & seq1 is constant implies seq - seq1 is bounded_above ) & ( seq is bounded_below & seq1 is constant implies seq - seq1 is bounded_below ) & ( seq is bounded & seq1 is constant implies ( seq - seq1 is bounded & seq1 - seq is bounded & seq (#) seq1 is bounded ) ) )

proof end;

theorem :: SEQM_3:77

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is non-increasing holds
seq + seq1 is bounded_above

proof end;

theorem :: SEQM_3:78

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is non-decreasing holds
seq + seq1 is bounded_below

proof end;

theorem Th79: :: SEQM_3:79

for X, x being set holds X --> x is constant

proof end;

registration

let X, x be set ;
cluster X --> x -> constant ;
coherence by Th79;

end;

theorem :: SEQM_3:80

( incl NAT is increasing & incl NAT is natural-yielding ) by Lm11;