SEQ_4: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers

:: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: SEQ_4:1

canceled;

theorem :: SEQ_4:2

canceled;

theorem :: SEQ_4:3

canceled;

theorem :: SEQ_4:4

canceled;

theorem :: SEQ_4:5

canceled;

theorem :: SEQ_4:6

canceled;

theorem :: SEQ_4:7

canceled;

theorem Th8: :: SEQ_4:8

for X, Y being Subset of REAL st ( for r, p being real number st r in X & p in Y holds
r < p ) holds
ex g being real number st
for r, p being real number st r in X & p in Y holds
( r <= g & g <= p )

proof end;

theorem Th9: :: SEQ_4:9

for p being real number
for X being Subset of REAL st 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X & g < r )

proof end;

theorem Th10: :: SEQ_4:10

for r being real number ex n being Element of NAT st r < n

proof end;

theorem :: SEQ_4:11

canceled;

theorem :: SEQ_4:12

canceled;

theorem :: SEQ_4:13

canceled;

theorem :: SEQ_4:14

for X being Subset of REAL holds
( X is bounded iff ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) )

proof end;

definition

canceled;
canceled;
let r be real number ;
:: original: {
redefine func {r} -> Subset of REAL;
coherence

proof end;

end;

:: deftheorem SEQ_4:def 1 :

:: deftheorem SEQ_4:def 2 :

theorem :: SEQ_4:15

canceled;

theorem Th16: :: SEQ_4:16

for X being real-membered set st not X is empty & X is bounded_above holds
ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )

proof end;

theorem Th17: :: SEQ_4:17

for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) holds
g1 = g2

proof end;

theorem Th18: :: SEQ_4:18

for X being real-membered set st not X is empty & X is bounded_below holds
ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )

proof end;

theorem Th19: :: SEQ_4:19

for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
g1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) ) & ( for r being real number st r in X holds
g2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ) holds
g1 = g2

proof end;

definition

canceled;
let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_above ) ;
func upper_bound X -> real number means :Def4: :: SEQ_4:def 4
( ( for r being real number st r in X holds
r <= it ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & it - s < r ) ) );
existence by A1, Th16;
uniqueness by Th17;

end;

:: deftheorem SEQ_4:def 3 :

:: deftheorem Def4 defines upper_bound SEQ_4:def 4 :

definition

let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_below ) ;
func lower_bound X -> real number means :Def5: :: SEQ_4:def 5
( ( for r being real number st r in X holds
it <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < it + s ) ) );
existence by A1, Th18;
uniqueness by Th19;

end;

:: deftheorem Def5 defines lower_bound SEQ_4:def 5 :

Lm1: for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X

proof end;

Lm2: for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X

proof end;

registration

let X be non empty real-membered bounded_below set ;
identify lower_bound X with inf X;
compatibility

proof end;

end;

registration

let X be non empty real-membered bounded_above set ;
identify upper_bound X with sup X;
compatibility

proof end;

end;

definition

let X be Subset of REAL;
:: original: upper_bound
redefine func upper_bound X -> Real;
coherence by XREAL_0:def 1;
:: original: lower_bound
redefine func lower_bound X -> Real;
coherence by XREAL_0:def 1;

end;

theorem :: SEQ_4:20

canceled;

theorem :: SEQ_4:21

canceled;

theorem Th22: :: SEQ_4:22

for r being real number holds
( lower_bound {r} = r & upper_bound {r} = r ) by XXREAL_2:11, XXREAL_2:13;

theorem Th23: :: SEQ_4:23

for r being real number holds lower_bound {r} = upper_bound {r}

proof end;

theorem :: SEQ_4:24

for X being Subset of REAL st X is bounded & not X is empty holds
lower_bound X <= upper_bound X

proof end;

theorem :: SEQ_4:25

for X being Subset of REAL st X is bounded & not X is empty holds
( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )

proof end;

theorem Th26: :: SEQ_4:26

for seq being Real_Sequence st seq is convergent holds
abs seq is convergent

proof end;

theorem :: SEQ_4:27

for seq being Real_Sequence st seq is convergent holds
lim (abs seq) = abs (lim seq)

proof end;

theorem :: SEQ_4:28

for seq being Real_Sequence st abs seq is convergent & lim (abs seq) = 0 holds
( seq is convergent & lim seq = 0 )

proof end;

theorem Th29: :: SEQ_4:29

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

proof end;

theorem Th30: :: SEQ_4:30

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

proof end;

theorem Th31: :: SEQ_4:31

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent

proof end;

theorem :: SEQ_4:32

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1

proof end;

registration

cluster Function-like V8() V15( NAT , REAL ) -> convergent Element of bool [:NAT,REAL:];
coherence

proof end;

end;

registration

cluster Relation-like NAT -defined REAL -valued Function-like V8() non empty total V15( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:];
existence

proof end;

end;

registration

let seq be convergent Real_Sequence;
let k be Element of NAT ;
cluster seq ^\ k -> convergent Real_Sequence;
coherence by Th29;

end;

theorem :: SEQ_4:33

for k being Element of NAT
for seq being Real_Sequence st seq is convergent holds
lim (seq ^\ k) = lim seq by Th30;

theorem :: SEQ_4:34

canceled;

theorem Th35: :: SEQ_4:35

for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent

proof end;

theorem :: SEQ_4:36

for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
lim seq = lim (seq ^\ k)

proof end;

theorem Th37: :: SEQ_4:37

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Element of NAT st seq ^\ k is non-empty

proof end;

theorem :: SEQ_4:38

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-empty )

proof end;

theorem :: SEQ_4:39

canceled;

theorem Th40: :: SEQ_4:40

for r being real number
for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Element of NAT st seq . n = r ) holds
lim seq = r

proof end;

theorem :: SEQ_4:41

for seq being Real_Sequence st seq is constant holds
for n being Element of NAT holds lim seq = seq . n by Th40;

theorem :: SEQ_4:42

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-empty holds
lim (seq1 ") = (lim seq) "

proof end;

theorem Th43: :: SEQ_4:43

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
seq is convergent

proof end;

theorem Th44: :: SEQ_4:44

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:45

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / (n + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th43, Th44;

theorem :: SEQ_4:46

for r, g being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )

proof end;

theorem Th47: :: SEQ_4:47

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent

proof end;

theorem Th48: :: SEQ_4:48

for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:49

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / ((n * n) + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th47, Th48;

theorem :: SEQ_4:50

for r, g being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )

proof end;

registration

cluster Function-like V15( NAT , REAL ) V36() bounded_above -> convergent Element of bool [:NAT,REAL:];
coherence

proof end;

end;

registration

cluster Function-like V15( NAT , REAL ) V37() bounded_below -> convergent Element of bool [:NAT,REAL:];
coherence

proof end;

end;

registration

cluster Function-like V15( NAT , REAL ) bounded monotone -> convergent Element of bool [:NAT,REAL:];
coherence

proof end;

end;

theorem :: SEQ_4:51

canceled;

theorem :: SEQ_4:52

canceled;

theorem Th53: :: SEQ_4:53

for seq being Real_Sequence st seq is monotone & seq is bounded holds
seq is convergent ;

theorem :: SEQ_4:54

for seq being Real_Sequence st seq is bounded_above & seq is non-decreasing holds
for n being Element of NAT holds seq . n <= lim seq

proof end;

theorem :: SEQ_4:55

for seq being Real_Sequence st seq is bounded_below & seq is non-increasing holds
for n being Element of NAT holds lim seq <= seq . n

proof end;

theorem Th56: :: SEQ_4:56

for seq being Real_Sequence ex Nseq being V34() sequence of NAT st seq * Nseq is monotone

proof end;

theorem Th57: :: SEQ_4:57

for seq being Real_Sequence st seq is bounded holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )

proof end;

theorem :: SEQ_4:58

for seq being Real_Sequence holds
( seq is convergent iff for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )

proof end;

theorem :: SEQ_4:59

for seq, seq1 being Real_Sequence st seq is constant & seq1 is convergent holds
( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )

proof end;

begin

theorem Th60: :: SEQ_4:60

for X being non empty real-membered set
for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t

proof end;

theorem :: SEQ_4:61

for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X by Lm1;

theorem Th62: :: SEQ_4:62

for X being non empty real-membered set
for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t

proof end;

theorem :: SEQ_4:63

for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X by Lm2;

theorem :: SEQ_4:64

for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_below holds
lower_bound Y <= lower_bound X

proof end;

theorem :: SEQ_4:65

for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y

proof end;

definition

let A be non empty natural-membered set ;
:: original: inf
redefine func min A -> Element of NAT ;
coherence by ORDINAL1:def 13;

end;

begin

theorem :: SEQ_4:66

0c is_a_unity_wrt addcomplex by BINOP_2:1, SETWISEO:22;

theorem Th6: :: SEQ_4:67

compcomplex is_an_inverseOp_wrt addcomplex

proof end;

theorem Th7: :: SEQ_4:68

addcomplex is having_an_inverseOp by Th6, FINSEQOP:def 2;

theorem Th8: :: SEQ_4:69

the_inverseOp_wrt addcomplex = compcomplex by Th6, Th7, FINSEQOP:def 3;

definition

redefine func diffcomplex equals :: SEQ_4:def 6
addcomplex * ((id COMPLEX),compcomplex);
compatibility

proof end;

end;

:: deftheorem defines diffcomplex SEQ_4:def 6 :

theorem :: SEQ_4:70

1r is_a_unity_wrt multcomplex by BINOP_2:6, SETWISEO:22;

theorem Th15: :: SEQ_4:71

multcomplex is_distributive_wrt addcomplex

proof end;

definition

let c be complex number ;
func c multcomplex -> UnOp of COMPLEX equals :: SEQ_4:def 7
multcomplex [;] (c,(id COMPLEX));
coherence

proof end;

end;

:: deftheorem defines multcomplex SEQ_4:def 7 :

Lm1: for c, c9 being Element of COMPLEX holds (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9

proof end;

theorem :: SEQ_4:72

for c, c9 being Element of COMPLEX holds (c multcomplex) . c9 = c * c9 by Lm1;

theorem :: SEQ_4:73

for c being Element of COMPLEX holds c multcomplex is_distributive_wrt addcomplex by Th15, FINSEQOP:55;

definition

func abscomplex -> Function of COMPLEX,REAL means :Def6: :: SEQ_4:def 8
for c being Element of COMPLEX holds it . c = |.c.|;
existence from FUNCT_2:sch 4();
uniqueness from BINOP_2:sch 1();

end;

:: deftheorem Def6 defines abscomplex SEQ_4:def 8 :

definition

let z1, z2 be FinSequence of COMPLEX ;
:: original: +
redefine func z1 + z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 9
addcomplex .: (z1,z2);
coherence

proof end;

proof end;

:: original: -
redefine func z1 - z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 10
diffcomplex .: (z1,z2);
coherence

proof end;

proof end;

end;

:: deftheorem defines + SEQ_4:def 9 :

:: deftheorem defines - SEQ_4:def 10 :

definition

let z be FinSequence of COMPLEX ;
:: original: -
redefine func - z -> FinSequence of COMPLEX equals :: SEQ_4:def 11
compcomplex * z;
coherence

proof end;

proof end;

end;

:: deftheorem defines - SEQ_4:def 11 :

notation

let z be FinSequence of COMPLEX ;
let c be complex number ;
synonym c * z for c (#) z;

end;

definition

let z be FinSequence of COMPLEX ;
let c be complex number ;
:: original: *
redefine func c * z -> FinSequence of COMPLEX equals :: SEQ_4:def 12
(c multcomplex) * z;
coherence

proof end;

proof end;

end;

:: deftheorem defines * SEQ_4:def 12 :

definition

let z be FinSequence of COMPLEX ;
:: original: |.
redefine func abs z -> FinSequence of REAL equals :: SEQ_4:def 13
abscomplex * z;
coherence

proof end;

proof end;

end;

:: deftheorem defines abs SEQ_4:def 13 :

definition

let n be Element of NAT ;
func COMPLEX n -> FinSequence-DOMAIN of COMPLEX equals :: SEQ_4:def 14
n -tuples_on COMPLEX;
correctness ;

end;

:: deftheorem defines COMPLEX SEQ_4:def 14 :

registration

let n be Element of NAT ;
cluster COMPLEX n -> ;
coherence ;

end;

Lm2: for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n

proof end;

theorem Th21: :: SEQ_4:74

for k, n being Element of NAT
for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX

proof end;

definition

let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original: +
redefine func z1 + z2 -> Element of COMPLEX n;
coherence by FINSEQ_2:140;

end;

theorem Th24: :: SEQ_4:75

for k, n being Element of NAT
for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2

proof end;

definition

let n be Element of NAT ;
func 0c n -> FinSequence of COMPLEX equals :: SEQ_4:def 15
n |-> 0c;
correctness ;

end;

:: deftheorem defines 0c SEQ_4:def 15 :

definition

let n be Element of NAT ;
:: original: 0c
redefine func 0c n -> Element of COMPLEX n;
coherence ;

end;

theorem :: SEQ_4:76

for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (0c n) = z & z = (0c n) + z ) by BINOP_2:1, FINSEQOP:57;

definition

let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original: -
redefine func - z -> Element of COMPLEX n;
coherence by FINSEQ_2:133;

end;

theorem Th29: :: SEQ_4:77

for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c

proof end;

Lm3: for n being Element of NAT holds - (0c n) = 0c n

proof end;

theorem :: SEQ_4:78

for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (- z) = 0c n & (- z) + z = 0c n ) by Th7, Th8, BINOP_2:1, FINSEQOP:77;

theorem :: SEQ_4:79

for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 & z2 = - z1 ) by Th7, Th8, BINOP_2:1, FINSEQOP:78;

theorem :: SEQ_4:80

for n being Element of NAT
for z being Element of COMPLEX n holds - (- z) = z ;

theorem :: SEQ_4:81

for n being Element of NAT
for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2

proof end;

Lm4: for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2

proof end;

theorem :: SEQ_4:82

for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds
z1 = z2 by Lm4;

theorem Th35: :: SEQ_4:83

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)

proof end;

definition

let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original: -
redefine func z1 - z2 -> Element of COMPLEX n;
coherence by FINSEQ_2:140;

end;

theorem :: SEQ_4:84

for k, n being Element of NAT
for z1, z2 being Element of COMPLEX n st k in Seg n holds
(z1 - z2) . k = (z1 . k) - (z2 . k)

proof end;

theorem :: SEQ_4:85

for n being Element of NAT
for z being Element of COMPLEX n holds z - (0c n) = z

proof end;

theorem :: SEQ_4:86

for n being Element of NAT
for z being Element of COMPLEX n holds (0c n) - z = - z

proof end;

theorem :: SEQ_4:87

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2 ;

theorem Th41: :: SEQ_4:88

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1

proof end;

theorem Th42: :: SEQ_4:89

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2

proof end;

theorem Th43: :: SEQ_4:90

for n being Element of NAT
for z being Element of COMPLEX n holds z - z = 0c n

proof end;

theorem Th44: :: SEQ_4:91

for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds
z1 = z2

proof end;

theorem Th45: :: SEQ_4:92

for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) - z3 = z1 - (z2 + z3)

proof end;

theorem Th46: :: SEQ_4:93

for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3

proof end;

theorem :: SEQ_4:94

for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3

proof end;

theorem :: SEQ_4:95

for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) + z3 = (z1 + z3) - z2 by Th46;

theorem Th49: :: SEQ_4:96

for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z

proof end;

theorem Th50: :: SEQ_4:97

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2

proof end;

theorem Th51: :: SEQ_4:98

for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 - z) + z

proof end;

definition

let n be Element of NAT ;
let z be Element of COMPLEX n;
let c be Element of COMPLEX ;
:: original: *
redefine func c * z -> Element of COMPLEX n;
coherence by FINSEQ_2:133;

end;

theorem Th52: :: SEQ_4:99

for k, n being Element of NAT
for c9, c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds
(c * z) . k = c * c9

proof end;

theorem :: SEQ_4:100

for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z

proof end;

theorem :: SEQ_4:101

for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)

proof end;

theorem :: SEQ_4:102

for n being Element of NAT
for c being Element of COMPLEX
for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2) by Th15, FINSEQOP:52, FINSEQOP:55;

theorem :: SEQ_4:103

for n being Element of NAT
for z being Element of COMPLEX n holds 1r * z = z

proof end;

theorem :: SEQ_4:104

for n being Element of NAT
for z being Element of COMPLEX n holds 0c * z = 0c n

proof end;

theorem :: SEQ_4:105

for n being Element of NAT
for z being Element of COMPLEX n holds (- 1r) * z = - z ;

definition

let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original: |.
redefine func abs z -> Element of n -tuples_on REAL;
correctness by FINSEQ_2:133;

end;

theorem Th59: :: SEQ_4:106

for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|

proof end;

theorem Th60: :: SEQ_4:107

for n being Element of NAT holds abs (0c n) = n |-> 0

proof end;

theorem Th61: :: SEQ_4:108

for n being Element of NAT
for z being Element of COMPLEX n holds abs (- z) = abs z

proof end;

theorem Th62: :: SEQ_4:109

for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)

proof end;

definition

let z be FinSequence of COMPLEX ;
func |.z.| -> Real equals :: SEQ_4:def 16
sqrt (Sum (sqr (abs z)));
correctness ;

end;

:: deftheorem defines |. SEQ_4:def 16 :

theorem Th63: :: SEQ_4:110

for n being Element of NAT holds |.(0c n).| = 0

proof end;

theorem Th64: :: SEQ_4:111

for n being Element of NAT
for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n

proof end;

theorem Th65: :: SEQ_4:112

for n being Element of NAT
for z being Element of COMPLEX n holds 0 <= |.z.|

proof end;

theorem :: SEQ_4:113

for n being Element of NAT
for z being Element of COMPLEX n holds |.(- z).| = |.z.| by Th61;

theorem :: SEQ_4:114

for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|

proof end;

theorem Th68: :: SEQ_4:115

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|

proof end;

theorem Th69: :: SEQ_4:116

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|

proof end;

theorem :: SEQ_4:117

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|

proof end;

theorem :: SEQ_4:118

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).|

proof end;

theorem Th72: :: SEQ_4:119

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )

proof end;

theorem :: SEQ_4:120

for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 <> z2 holds
0 < |.(z1 - z2).|

proof end;

theorem Th74: :: SEQ_4:121

for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|

proof end;

theorem Th75: :: SEQ_4:122

for n being Element of NAT
for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|

proof end;

definition

let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attr A is open means :Def15: :: SEQ_4:def 17
for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) );

end;

:: deftheorem Def15 defines open SEQ_4:def 17 :

definition

let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attr A is closed means :: SEQ_4:def 18
for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A;

end;

:: deftheorem defines closed SEQ_4:def 18 :

theorem :: SEQ_4:123

for n being Element of NAT
for A being Subset of (COMPLEX n) st A = {} holds
A is open

proof end;

theorem :: SEQ_4:124

for n being Element of NAT
for A being Subset of (COMPLEX n) st A = COMPLEX n holds
A is open

proof end;

theorem :: SEQ_4:125

for n being Element of NAT
for AA being Subset-Family of (COMPLEX n) st ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) holds
for A being Subset of (COMPLEX n) st A = union AA holds
A is open

proof end;

theorem :: SEQ_4:126

for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A is open & B is open holds
for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open

proof end;

definition

let n be Element of NAT ;
let x be Element of COMPLEX n;
let r be Real;
func Ball (x,r) -> Subset of (COMPLEX n) equals :: SEQ_4:def 19
{ z where z is Element of COMPLEX n : |.(z - x).| < r } ;
coherence

proof end;

end;

:: deftheorem defines Ball SEQ_4:def 19 :

theorem Th80: :: SEQ_4:127

for n being Element of NAT
for r being Real
for z, x being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )

proof end;

theorem :: SEQ_4:128

for n being Element of NAT
for r being Real
for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)

proof end;

theorem :: SEQ_4:129

for n being Element of NAT
for r1 being Real
for z1 being Element of COMPLEX n holds Ball (z1,r1) is open

proof end;

definition

let n be Element of NAT ;
let x be Element of COMPLEX n;
let A be Subset of (COMPLEX n);
func dist (x,A) -> Real means :Def18: :: SEQ_4:def 20
for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
it = lower_bound X;
existence

proof end;

proof end;

end;

:: deftheorem Def18 defines dist SEQ_4:def 20 :

definition

let n be Element of NAT ;
let A be Subset of (COMPLEX n);
let r be Real;
func Ball (A,r) -> Subset of (COMPLEX n) equals :: SEQ_4:def 21
{ z where z is Element of COMPLEX n : dist (z,A) < r } ;
coherence

proof end;

end;

:: deftheorem defines Ball SEQ_4:def 21 :

theorem Th84: :: SEQ_4:130

for X being Subset of REAL
for r being Real st X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) holds
lower_bound X >= r

proof end;

theorem Th85: :: SEQ_4:131

for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0

proof end;

theorem Th86: :: SEQ_4:132

for n being Element of NAT
for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|

proof end;

theorem Th87: :: SEQ_4:133

for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0

proof end;

theorem :: SEQ_4:134

for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0

proof end;

theorem :: SEQ_4:135

for n being Element of NAT
for z1, x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)

proof end;

theorem Th90: :: SEQ_4:136

for n being Element of NAT
for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )

proof end;

theorem Th91: :: SEQ_4:137

for n being Element of NAT
for r being Real
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball (A,r)

proof end;

theorem :: SEQ_4:138

for n being Element of NAT
for r being Real
for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)

proof end;

theorem :: SEQ_4:139

for n being Element of NAT
for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open

proof end;

definition

let n be Element of NAT ;
let A, B be Subset of (COMPLEX n);
func dist (A,B) -> Real means :Def20: :: SEQ_4:def 22
for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
it = lower_bound X;
existence

proof end;

proof end;

end;

:: deftheorem Def20 defines dist SEQ_4:def 22 :

definition

canceled;

end;

:: deftheorem SEQ_4:def 23 :

theorem :: SEQ_4:140

for X, Y being Subset of REAL st X <> {} & Y <> {} holds
X ++ Y <> {}

proof end;

theorem Th95: :: SEQ_4:141

for X, Y being Subset of REAL st X is bounded_below & Y is bounded_below holds
X ++ Y is bounded_below

proof end;

theorem Th96: :: SEQ_4:142

for X, Y being Subset of REAL st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds
lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)

proof end;

theorem Th97: :: SEQ_4:143

for X, Y being Subset of REAL st Y is bounded_below & X <> {} & ( for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ) holds
lower_bound X >= lower_bound Y

proof end;

theorem Th98: :: SEQ_4:144

for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
dist (A,B) >= 0

proof end;

theorem :: SEQ_4:145

for n being Element of NAT
for A, B being Subset of (COMPLEX n) holds dist (A,B) = dist (B,A)

proof end;

theorem Th100: :: SEQ_4:146

for n being Element of NAT
for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)

proof end;

theorem :: SEQ_4:147

for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A meets B holds
dist (A,B) = 0

proof end;

definition

let n be Element of NAT ;
func ComplexOpenSets n -> Subset-Family of (COMPLEX n) equals :: SEQ_4:def 24
{ A where A is Subset of (COMPLEX n) : A is open } ;
coherence

proof end;

end;

:: deftheorem defines ComplexOpenSets SEQ_4:def 24 :

theorem :: SEQ_4:148

for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A in ComplexOpenSets n iff A is open )

proof end;

theorem :: SEQ_4:149

for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )

proof end;

begin

defpred S₁[ Nat] means for R being finite Subset of REAL st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );

Lm1: S₁[ 0 ]
;

Lm2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof end;

Lm3: for n being Element of NAT holds S₁[n]
from NAT_1:sch 1(Lm1, Lm2);

theorem Th1: :: SEQ_4:150

for R being finite Subset of REAL st R <> {} holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

proof end;

theorem :: SEQ_4:151

for n being Nat
for f being FinSequence holds
( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )

proof end;

theorem :: SEQ_4:152

for n being Nat
for f being FinSequence holds
( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )

proof end;

theorem :: SEQ_4:153

for D being non empty set
for f1, f2 being FinSequence of D
for n being Element of NAT st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n

proof end;

theorem :: SEQ_4:154

for v being FinSequence of REAL st v is increasing holds
for n, m being Element of NAT st n in dom v & m in dom v & n <= m holds
v . n <= v . m

proof end;

theorem Th19: :: SEQ_4:155

for v being FinSequence of REAL st v is increasing holds
for n, m being Element of NAT st n in dom v & m in dom v & n <> m holds
v . n <> v . m

proof end;

theorem Th20: :: SEQ_4:156

for v, v1 being FinSequence of REAL
for n being Element of NAT st v is increasing & v1 = v | (Seg n) holds
v1 is increasing

proof end;

defpred S₂[ Element of NAT ] means for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );

Lm4: S₂[ 0 ]

proof end;

Lm5: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof end;

Lm6: for n being Element of NAT holds S₂[n]
from NAT_1:sch 1(Lm4, Lm5);

theorem :: SEQ_4:157

for v being FinSequence of REAL ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) by Lm6;

defpred S₃[ Element of NAT ] means for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;

Lm7: S₃[ 0 ]

proof end;

Lm8: for n being Element of NAT st S₃[n] holds
S₃[n + 1]

proof end;

Lm9: for n being Element of NAT holds S₃[n]
from NAT_1:sch 1(Lm7, Lm8);

theorem :: SEQ_4:158

for v1, v2 being FinSequence of REAL st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2 by Lm9;

definition

let v be FinSequence of REAL ;
func Incr v -> increasing FinSequence of REAL means :Def25: :: SEQ_4:def 25
( rng it = rng v & len it = card (rng v) );
existence

proof end;

uniqueness by Lm9;

end;

:: deftheorem Def25 defines Incr SEQ_4:def 25 :

registration

let v be non empty FinSequence of REAL ;
cluster Incr v -> non empty increasing ;
coherence

proof end;

end;