:: Real Sequences and Basic Operations on Them
:: by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
mode Real_Sequence is sequence of REAL;
end;

theorem Th1: :: SEQ_1:1
for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) )
proofend;

theorem Th2: :: SEQ_1:2
for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) )
proofend;

definition
let f be real-valued Function;
let x be set ;
:: original:.
redefine funcf . x ->  Real;
coherence
 f . x is Real by XREAL_0:def_1;
end;

registration
cluster Relation-like non-zero NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));
existence
 ex b1 being PartFunc of NAT,REAL st b1 is non-zero
proofend;
end;

theorem :: SEQ_1:3
for f being non-zero PartFunc of NAT,REAL holds rng f c= REAL \ {0}
proofend;

theorem Th4: :: SEQ_1:4
for seq being Real_Sequence holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0 )
proofend;

theorem Th5: :: SEQ_1:5
for seq being Real_Sequence holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0 )
proofend;

theorem :: SEQ_1:6
for r being real number ex seq being Real_Sequence st rng seq = {r}
proofend;

scheme :: SEQ_1:sch 1
ExRealSeq{ F1( set ) ->  real number } :
 ex seq being Real_Sequence st
for n being Element of NAT holds seq . n = F1(n)
proofend;

scheme :: SEQ_1:sch 2
PartFuncExD9{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ] } :
 ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) &amp; ( for d being Element of F1() st d in dom f holds
P1[d,f . d] ) )
proofend;

scheme :: SEQ_1:sch 3
LambdaPFD9{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  Element of F2(), P1[ set ] } :
 ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) &amp; ( for d being Element of F1() st d in dom f holds
f . d = F3(d) ) )
proofend;

scheme :: SEQ_1:sch 4
UnPartFuncD9{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set ) ->  set } :
 for f, g being PartFunc of F1(),F2() st dom f = F3() &amp; ( for c being Element of F1() st c in dom f holds
f . c = F4(c) ) &amp; dom g = F3() &amp; ( for c being Element of F1() st c in dom g holds
g . c = F4(c) ) holds
f = g
proofend;

theorem Th7: :: SEQ_1:7
for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
proofend;

theorem Th8: :: SEQ_1:8
for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 (#) seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) * (seq2 . n) )
proofend;

theorem Th9: :: SEQ_1:9
for r being real number
for seq1, seq2 being Real_Sequence holds
( seq1 = r (#) seq2 iff for n being Element of NAT holds seq1 . n = r * (seq2 . n) )
proofend;

theorem :: SEQ_1:10
for seq1, seq2 being Real_Sequence holds
( seq1 = - seq2 iff for n being Element of NAT holds seq1 . n = - (seq2 . n) )
proofend;

theorem :: SEQ_1:11
for seq1, seq2 being Real_Sequence holds seq1 - seq2 = seq1 + (- seq2) ;

theorem Th12: :: SEQ_1:12
for seq1, seq being Real_Sequence holds
( seq1 = abs seq iff for n being Element of NAT holds seq1 . n = abs (seq . n) )
proofend;

theorem Th13: :: SEQ_1:13
for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proofend;

theorem Th14: :: SEQ_1:14
for seq1, seq2, seq3 being Real_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)
proofend;

theorem Th15: :: SEQ_1:15
for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)
proofend;

theorem :: SEQ_1:16
for seq3, seq1, seq2 being Real_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th15;

theorem :: SEQ_1:17
for seq being Real_Sequence holds - seq = (- 1) (#) seq ;

theorem Th18: :: SEQ_1:18
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
proofend;

theorem Th19: :: SEQ_1:19
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
proofend;

theorem Th20: :: SEQ_1:20
for seq1, seq2, seq3 being Real_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
proofend;

theorem :: SEQ_1:21
for seq3, seq1, seq2 being Real_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th20;

theorem Th22: :: SEQ_1:22
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
proofend;

theorem Th23: :: SEQ_1:23
for r, p being real number
for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
proofend;

theorem Th24: :: SEQ_1:24
for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
proofend;

theorem :: SEQ_1:25
for r being real number
for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
proofend;

theorem :: SEQ_1:26
for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proofend;

theorem :: SEQ_1:27
for seq being Real_Sequence holds 1 (#) seq = seq
proofend;

theorem :: SEQ_1:28
canceled;

theorem :: SEQ_1:29
for seq1, seq2 being Real_Sequence holds seq1 - (- seq2) = seq1 + seq2 ;

theorem :: SEQ_1:30
for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proofend;

theorem :: SEQ_1:31
for seq1, seq2, seq3 being Real_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
proofend;

theorem :: SEQ_1:32
for seq1, seq2 being Real_Sequence holds
( (- seq1) (#) seq2 = - (seq1 (#) seq2) &amp; seq1 (#) (- seq2) = - (seq1 (#) seq2) ) by Th18;

theorem Th33: :: SEQ_1:33
for seq being Real_Sequence st seq is non-zero holds
seq " is non-zero
proofend;

theorem :: SEQ_1:34
canceled;

theorem Th35: :: SEQ_1:35
for seq, seq1 being Real_Sequence holds
( ( seq is non-zero &amp; seq1 is non-zero ) iff seq (#) seq1 is non-zero )
proofend;

theorem Th36: :: SEQ_1:36
for seq, seq1 being Real_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) "
proofend;

theorem :: SEQ_1:37
for seq, seq1 being Real_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1
proofend;

theorem :: SEQ_1:38
for seq9, seq, seq19, seq1 being Real_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)
proofend;

theorem :: SEQ_1:39
for seq, seq1 being Real_Sequence st seq is non-zero &amp; seq1 is non-zero holds
seq /" seq1 is non-zero
proofend;

theorem Th40: :: SEQ_1:40
for seq, seq1 being Real_Sequence holds (seq /" seq1) " = seq1 /" seq
proofend;

theorem :: SEQ_1:41
for seq2, seq1, seq being Real_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
proofend;

theorem :: SEQ_1:42
for seq2, seq, seq1 being Real_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq
proofend;

theorem Th43: :: SEQ_1:43
for seq1, seq2, seq being Real_Sequence st seq1 is non-zero holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
proofend;

theorem Th44: :: SEQ_1:44
for r being real number
for seq being Real_Sequence st r <> 0 &amp; seq is non-zero holds
r (#) seq is non-zero
proofend;

theorem :: SEQ_1:45
for seq being Real_Sequence st seq is non-zero holds
- seq is non-zero by Th44;

theorem Th46: :: SEQ_1:46
for r being real number
for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
proofend;

Lm1:  (- 1) " = - 1
;

theorem :: SEQ_1:47
for seq being Real_Sequence holds (- seq) " = (- 1) (#) (seq ") by Lm1, Th46;

theorem :: SEQ_1:48
for seq1, seq being Real_Sequence holds
( - (seq1 /" seq) = (- seq1) /" seq &amp; seq1 /" (- seq) = - (seq1 /" seq) )
proofend;

theorem :: SEQ_1:49
for seq1, seq, seq19 being Real_Sequence holds
( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq &amp; (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )
proofend;

theorem :: SEQ_1:50
for seq, seq9, seq1, seq19 being Real_Sequence st seq is non-zero &amp; seq9 is non-zero holds
( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) &amp; (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
proofend;

theorem :: SEQ_1:51
for seq19, seq, seq9, seq1 being Real_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
proofend;

theorem Th52: :: SEQ_1:52
for seq, seq9 being Real_Sequence holds abs (seq (#) seq9) = (abs seq) (#) (abs seq9)
proofend;

theorem :: SEQ_1:53
for seq being Real_Sequence st seq is non-zero holds
abs seq is non-zero
proofend;

theorem Th54: :: SEQ_1:54
for seq being Real_Sequence holds (abs seq) " = abs (seq ")
proofend;

theorem :: SEQ_1:55
for seq9, seq being Real_Sequence holds abs (seq9 /" seq) = (abs seq9) /" (abs seq)
proofend;

theorem :: SEQ_1:56
for r being real number
for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq)
proofend;