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

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 object st x in NAT holds
f . x is real ) ) )

proof end;

theorem Th2: :: SEQ_1:2

for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for n being Nat holds f . n is real ) ) )

proof end;

registration

cluster Relation-like NAT -defined REAL -valued Function-like non-zero complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));

existence
ex b₁ being PartFunc of NAT,REAL st b₁ is non-zero

proof end;

end;

theorem :: SEQ_1:3

for f being non-zero PartFunc of NAT,REAL holds rng f c= REAL \ {0} by ORDINAL1:def 15, ZFMISC_1:34;

theorem Th4: :: SEQ_1:4

for seq being Real_Sequence holds
( seq is non-zero iff for x being object st x in NAT holds
seq . x <> 0 )

proof end;

theorem Th5: :: SEQ_1:5

for seq being Real_Sequence holds
( seq is non-zero iff for n being Nat holds seq . n <> 0 )

proof end;

theorem :: SEQ_1:6

for r being Real ex seq being Real_Sequence st rng seq = {r}

proof end;

scheme :: SEQ_1:sch 1
ExRealSeq{ F₁( object ) -> Real } :

ex seq being Real_Sequence st
for n being Nat holds seq . n = F₁(n)

proof end;

::
:: Basic Operations on Sequences
::

scheme :: SEQ_1:sch 2
PartFuncExD9{ F₁() -> non empty set , F₂() -> non empty set , P₁[ object , object ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for d being Element of F₁() holds
( d in dom f iff ex c being Element of F₂() st P₁[d,c] ) ) & ( for d being Element of F₁() st d in dom f holds
P₁[d,f . d] ) )

proof end;

scheme :: SEQ_1:sch 3
LambdaPFD9{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> Element of F₂(), P₁[ object ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for d being Element of F₁() holds
( d in dom f iff P₁[d] ) ) & ( for d being Element of F₁() st d in dom f holds
f . d = F₃(d) ) )

proof end;

scheme :: SEQ_1:sch 4
UnPartFuncD9{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( object ) -> object } :

for f, g being PartFunc of F₁(),F₂() st dom f = F₃() & ( for c being Element of F₁() st c in dom f holds
f . c = F₄(c) ) & dom g = F₃() & ( for c being Element of F₁() st c in dom g holds
g . c = F₄(c) ) holds
f = g

proof end;

theorem Th7: :: SEQ_1:7

for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )

proof end;

theorem Th8: :: SEQ_1:8

for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 (#) seq2 iff for n being Nat holds seq . n = (seq1 . n) * (seq2 . n) )

proof end;

theorem Th9: :: SEQ_1:9

for r being Real
for seq1, seq2 being Real_Sequence holds
( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

proof end;

theorem :: SEQ_1:10

for seq1, seq2 being Real_Sequence holds
( seq1 = - seq2 iff for n being Nat holds seq1 . n = - (seq2 . n) )

proof end;

theorem :: SEQ_1:11

for seq1, seq2 being Real_Sequence holds seq1 - seq2 = seq1 + (- seq2) ;

theorem Th12: :: SEQ_1:12

for seq, seq1 being Real_Sequence holds
( seq1 = abs seq iff for n being Nat holds seq1 . n = |.(seq . n).| )

proof end;

theorem Th13: :: SEQ_1:13

for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)

proof end;

theorem Th14: :: SEQ_1:14

for seq1, seq2, seq3 being Real_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)

proof end;

theorem Th15: :: SEQ_1:15

for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)

proof end;

theorem :: SEQ_1:16

for seq1, seq2, seq3 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
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

proof end;

theorem Th19: :: SEQ_1:19

for r being Real
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

proof end;

theorem Th20: :: SEQ_1:20

for seq1, seq2, seq3 being Real_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)

proof end;

theorem :: SEQ_1:21

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

theorem Th22: :: SEQ_1:22

for r being Real
for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

proof end;

theorem Th23: :: SEQ_1:23

for r, p being Real
for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)

proof end;

theorem Th24: :: SEQ_1:24

for r being Real
for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

proof end;

theorem :: SEQ_1:25

for r being Real
for seq, seq1 being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq

proof end;

theorem :: SEQ_1:26

for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

proof end;

theorem :: SEQ_1:27

for seq being Real_Sequence holds 1 (#) seq = seq

proof end;

theorem :: SEQ_1:28

canceled;

::$CT

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

proof end;

theorem :: SEQ_1:31

for seq1, seq2, seq3 being Real_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3

proof end;

theorem :: SEQ_1:32

for seq1, seq2 being Real_Sequence holds
( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) ) by Th18;

theorem Th32: :: SEQ_1:33

for seq being Real_Sequence st seq is non-zero holds
seq " is non-zero

proof end;

theorem :: SEQ_1:34

canceled;

::$CT

theorem Th33: :: SEQ_1:35

for seq, seq1 being Real_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )

proof end;

theorem Th34: :: SEQ_1:36

for seq, seq1 being Real_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) "

proof end;

theorem :: SEQ_1:37

for seq, seq1 being Real_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1

proof end;

theorem :: SEQ_1:38

for seq, seq1, seq9, seq19 being Real_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)

proof end;

theorem :: SEQ_1:39

for seq, seq1 being Real_Sequence st seq is non-zero & seq1 is non-zero holds
seq /" seq1 is non-zero

proof end;

theorem Th38: :: SEQ_1:40

for seq, seq1 being Real_Sequence holds (seq /" seq1) " = seq1 /" seq

proof end;

theorem :: SEQ_1:41

for seq, seq1, seq2 being Real_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq

proof end;

theorem :: SEQ_1:42

for seq, seq1, seq2 being Real_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq

proof end;

theorem Th41: :: SEQ_1:43

for seq, seq1, seq2 being Real_Sequence st seq1 is non-zero holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

proof end;

theorem Th42: :: SEQ_1:44

for r being Real
for seq being Real_Sequence st r <> 0 & seq is non-zero holds
r (#) seq is non-zero

proof end;

theorem :: SEQ_1:45

for seq being Real_Sequence st seq is non-zero holds
- seq is non-zero by Th42;

theorem Th44: :: SEQ_1:46

for r being Real
for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ")

proof end;

Lm1: (- 1) " = - 1
;

theorem :: SEQ_1:47

for seq being Real_Sequence holds (- seq) " = (- 1) (#) (seq ") by Lm1, Th44;

theorem :: SEQ_1:48

for seq, seq1 being Real_Sequence holds
( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

proof end;

theorem :: SEQ_1:49

for seq, seq1, seq19 being Real_Sequence holds
( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )

proof end;

theorem :: SEQ_1:50

for seq, seq1, seq9, seq19 being Real_Sequence st seq is non-zero & seq9 is non-zero holds
( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )

proof end;

theorem :: SEQ_1:51

for seq, seq1, seq9, seq19 being Real_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)

proof end;

theorem Th50: :: SEQ_1:52

for seq, seq9 being Real_Sequence holds abs (seq (#) seq9) = (abs seq) (#) (abs seq9)

proof end;

theorem :: SEQ_1:53

for seq being Real_Sequence st seq is non-zero holds
abs seq is non-zero

proof end;

theorem Th52: :: SEQ_1:54

for seq being Real_Sequence holds (abs seq) " = abs (seq ")

proof end;

theorem :: SEQ_1:55

for seq, seq9 being Real_Sequence holds abs (seq9 /" seq) = (abs seq9) /" (abs seq)

proof end;

theorem :: SEQ_1:56

for r being Real
for seq being Real_Sequence holds abs (r (#) seq) = |.r.| (#) (abs seq)

proof end;

definition

let b be Real;

func seq_const b -> Real_Sequence equals :Def1: :: SEQ_1:def 1
NAT --> b;

coherence
NAT --> b is Real_Sequence

proof end;

end;

:: deftheorem Def1 defines seq_const SEQ_1:def 1 :
for b being Real holds seq_const b = NAT --> b;

registration

let b be Real;

cluster seq_const b -> constant ;

coherence
seq_const b is constant ;

end;

registration

let b be non zero Real;

cluster seq_const b -> non-zero ;

coherence
seq_const b is non-zero

proof end;

end;

registration

cluster Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));

existence
ex b₁ being Real_Sequence st b₁ is constant

proof end;

end;

theorem :: SEQ_1:57

for a being Real
for k being Nat holds (seq_const a) . k = a by ORDINAL1:def 12, FUNCOP_1:7;

registration

let k be object ;

reduce (NAT --> 0) . k to 0 ;

reducibility
(NAT --> 0) . k = 0

proof end;

end;

registration

let k be object ;

reduce (seq_const 0) . k to 0 ;

reducibility
(seq_const 0) . k = 0 ;

end;