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

theorem Th1: :: SEQ_4:1
for X, Y being Subset of REAL st ( for r, p being Real st r in X & p in Y holds
r < p ) holds
ex g being Real st
for r, p being Real st r in X & p in Y holds
( r <= g & g <= p )
proof end;

theorem Th2: :: SEQ_4:2
for p being Real
for X being Subset of REAL st 0 < p & ex r being Real st r in X & ( for r being Real st r in X holds
r + p in X ) holds
for g being Real ex r being Real st
( r in X & g < r )
proof end;

theorem Th3: :: SEQ_4:3
for r being Real ex n being Nat st r < n
proof end;

theorem :: SEQ_4:4
for X being Subset of REAL holds
( X is real-bounded iff ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) )
proof end;

definition
let r be Real;
:: original: {
redefine func {r} -> Subset of REAL;
coherence
{r} is Subset of REAL
proof end;
end;

theorem Th5: :: SEQ_4:5
for X being real-membered set st not X is empty & X is bounded_above holds
ex g being Real st
( ( for r being Real st r in X holds
r <= g ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g - s < r ) ) )
proof end;

theorem Th6: :: SEQ_4:6
for g1, g2 being Real
for X being real-membered set st ( for r being Real st r in X holds
r <= g1 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g1 - s < r ) ) & ( for r being Real st r in X holds
r <= g2 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g2 - s < r ) ) holds
g1 = g2
proof end;

theorem Th7: :: SEQ_4:7
for X being real-membered set st not X is empty & X is bounded_below holds
ex g being Real st
( ( for r being Real st r in X holds
g <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < g + s ) ) )
proof end;

theorem Th8: :: SEQ_4:8
for g1, g2 being Real
for X being real-membered set st ( for r being Real st r in X holds
g1 <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < g1 + s ) ) & ( for r being Real st r in X holds
g2 <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < g2 + s ) ) holds
g1 = g2
proof end;

definition
let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_above ) ;
func upper_bound X -> Real means :Def1: :: SEQ_4:def 1
( ( for r being Real st r in X holds
r <= it ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & it - s < r ) ) );
existence
ex b1 being Real st
( ( for r being Real st r in X holds
r <= b1 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & b1 - s < r ) ) )
by ;
uniqueness
for b1, b2 being Real st ( for r being Real st r in X holds
r <= b1 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & b1 - s < r ) ) & ( for r being Real st r in X holds
r <= b2 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & b2 - s < r ) ) holds
b1 = b2
by Th6;
end;

:: deftheorem Def1 defines upper_bound SEQ_4:def 1 :
for X being real-membered set st not X is empty & X is bounded_above holds
for b2 being Real holds
( b2 = upper_bound X iff ( ( for r being Real st r in X holds
r <= b2 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & b2 - s < r ) ) ) );

definition
let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_below ) ;
func lower_bound X -> Real means :Def2: :: SEQ_4:def 2
( ( for r being Real st r in X holds
it <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < it + s ) ) );
existence
ex b1 being Real st
( ( for r being Real st r in X holds
b1 <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < b1 + s ) ) )
by ;
uniqueness
for b1, b2 being Real st ( for r being Real st r in X holds
b1 <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < b1 + s ) ) & ( for r being Real st r in X holds
b2 <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < b2 + s ) ) holds
b1 = b2
by Th8;
end;

:: deftheorem Def2 defines lower_bound SEQ_4:def 2 :
for X being real-membered set st not X is empty & X is bounded_below holds
for b2 being Real holds
( b2 = lower_bound X iff ( ( for r being Real st r in X holds
b2 <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < b2 + s ) ) ) );

Lm1: for r being Real
for X being non empty real-membered set st ( for s being Real st s in X holds
s >= r ) & ( for t being Real st ( for s being Real 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 st ( for s being Real st s in X holds
s <= r ) & ( for t being Real st ( for s being Real 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;

theorem Th9: :: SEQ_4:9
for r being Real holds
( lower_bound {r} = r & upper_bound {r} = r ) by ;

theorem Th10: :: SEQ_4:10
for r being Real holds lower_bound {r} = upper_bound {r}
proof end;

theorem :: SEQ_4:11
for X being Subset of REAL st X is real-bounded & not X is empty holds
lower_bound X <= upper_bound X
proof end;

theorem :: SEQ_4:12
for X being Subset of REAL st X is real-bounded & not X is empty holds
( ex r, p being Real st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )
proof end;

::
:: Theorems about the Convergence and the Limit
::
theorem Th13: :: SEQ_4:13
for seq being Real_Sequence st seq is convergent holds
abs seq is convergent
proof end;

registration
let seq be convergent Real_Sequence;
cluster |.seq.| -> convergent for Real_Sequence;
coherence
for b1 being Real_Sequence st b1 = abs seq holds
b1 is convergent
by Th13;
end;

theorem :: SEQ_4:14
for seq being Real_Sequence st seq is convergent holds
lim (abs seq) = |.(lim seq).|
proof end;

theorem :: SEQ_4:15
for seq being Real_Sequence st abs seq is convergent & lim (abs seq) = 0 holds
( seq is convergent & lim seq = 0 )
proof end;

theorem Th16: :: SEQ_4:16
for seq, seq1 being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
proof end;

theorem Th17: :: SEQ_4:17
for seq, seq1 being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof end;

theorem Th18: :: SEQ_4:18
for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent
proof end;

theorem :: SEQ_4:19
for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1
proof end;

registration
let seq be convergent Real_Sequence;
let k be Nat;
cluster seq ^\ k -> convergent for Real_Sequence;
coherence
for b1 being Real_Sequence st b1 = seq ^\ k holds
b1 is convergent
by Th16;
end;

theorem :: SEQ_4:20
for k being Nat
for seq being Real_Sequence st seq is convergent holds
lim (seq ^\ k) = lim seq by Th17;

theorem Th21: :: SEQ_4:21
for k being Nat
for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent
proof end;

theorem :: SEQ_4:22
for k being Nat
for seq being Real_Sequence st seq ^\ k is convergent holds
lim seq = lim (seq ^\ k)
proof end;

theorem Th23: :: SEQ_4:23
for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Nat st seq ^\ k is non-zero
proof end;

theorem :: SEQ_4:24
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-zero )
proof end;

theorem Th25: :: SEQ_4:25
for r being Real
for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Nat st seq . n = r ) holds
lim seq = r
proof end;

theorem :: SEQ_4:26
for seq being Real_Sequence st seq is constant holds
for n being Nat holds lim seq = seq . n by Th25;

theorem :: SEQ_4:27
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-zero holds
lim (seq1 ") = (lim seq) "
proof end;

theorem :: SEQ_4:28
canceled;

theorem :: SEQ_4:29
canceled;

theorem :: SEQ_4:30
canceled;

LmTh28: for r being Real
for seq being Real_Sequence st ( for n being Nat holds seq . n = 1 / (n + r) ) holds
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p

proof end;

Th28: for r being Real
for seq being Real_Sequence st ( for n being Nat holds seq . n = 1 / (n + r) ) holds
seq is convergent

proof end;

Th29: for r being Real
for seq being Real_Sequence st ( for n being Nat holds seq . n = 1 / (n + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:31
for r, g being Real
for seq being Real_Sequence st ( for n being Nat holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )
proof end;

theorem :: SEQ_4:32
canceled;

theorem :: SEQ_4:33
canceled;

theorem :: SEQ_4:34
canceled;

LmTh32: for r being Real
for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p

proof end;

Th32: for r being Real
for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent

proof end;

Th33: for r being Real
for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:35
for r, g being Real
for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )
proof end;

registration
coherence
for b1 being Real_Sequence st b1 is V47() & b1 is bounded_above holds
b1 is convergent
proof end;
end;

registration
coherence
for b1 being Real_Sequence st b1 is V48() & b1 is bounded_below holds
b1 is convergent
proof end;
end;

registration
coherence
for b1 being Real_Sequence st b1 is monotone & b1 is bounded holds
b1 is convergent
proof end;
end;

theorem Th36: :: SEQ_4:36
for seq being Real_Sequence st seq is monotone & seq is bounded holds
seq is convergent ;

theorem :: SEQ_4:37
for seq being Real_Sequence st seq is bounded_above & seq is V47() holds
for n being Nat holds seq . n <= lim seq
proof end;

theorem :: SEQ_4:38
for seq being Real_Sequence st seq is bounded_below & seq is V48() holds
for n being Nat holds lim seq <= seq . n
proof end;

theorem Th39: :: SEQ_4:39
for seq being Real_Sequence ex Nseq being V45() sequence of NAT st seq * Nseq is monotone
proof end;

:: Bolzano-Weierstrass Theorem (1 dimension)
theorem Th40: :: SEQ_4:40
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;

:: Cauchy sequence
theorem :: SEQ_4:41
for seq being Real_Sequence holds
( seq is convergent iff for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s )
proof end;

theorem :: SEQ_4:42
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;

:: from PSCOMP_1
theorem Th43: :: SEQ_4:43
for X being non empty real-membered set
for t being Real st ( for s being Real st s in X holds
s >= t ) holds
lower_bound X >= t
proof end;

theorem Th44: :: SEQ_4:44
for r being Real
for X being non empty real-membered set st ( for s being Real st s in X holds
s >= r ) & ( for t being Real st ( for s being Real st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X by Lm1;

theorem Th45: :: SEQ_4:45
for X being non empty real-membered set
for r, t being Real st ( for s being Real st s in X holds
s <= t ) holds
upper_bound X <= t
proof end;

theorem Th46: :: SEQ_4:46
for X being non empty real-membered set
for r being Real st ( for s being Real st s in X holds
s <= r ) & ( for t being Real st ( for s being Real st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X by Lm2;

theorem :: SEQ_4:47
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:48
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;

:: from CQC_SIM1, 2007.03.15, A.T.
definition
let A be non empty natural-membered set ;
:: original: inf
redefine func min A -> Element of NAT ;
coherence
inf A is Element of NAT
by ORDINAL1:def 12;
end;

theorem :: SEQ_4:49

theorem Th50: :: SEQ_4:50
proof end;

theorem Th51: :: SEQ_4:51

theorem Th52: :: SEQ_4:52

definition
redefine func diffcomplex equals :: SEQ_4:def 3
compatibility
for b1 being Element of bool holds
( b1 = diffcomplex iff b1 = addcomplex * ((),compcomplex) )
proof end;
end;

:: deftheorem defines diffcomplex SEQ_4:def 3 :

theorem :: SEQ_4:53

theorem Th54: :: SEQ_4:54
proof end;

definition
let c be Complex;
func c multcomplex -> UnOp of COMPLEX equals :: SEQ_4:def 4
multcomplex [;] (c,());
coherence
multcomplex [;] (c,()) is UnOp of COMPLEX
proof end;
end;

:: deftheorem defines multcomplex SEQ_4:def 4 :
for c being Complex holds c multcomplex = multcomplex [;] (c,());

Lm3: for c, c9 being Element of COMPLEX holds (multcomplex [;] (c,())) . c9 = c * c9
proof end;

theorem :: SEQ_4:55
for c, c9 being Element of COMPLEX holds () . c9 = c * c9 by Lm3;

theorem :: SEQ_4:56
for c being Element of COMPLEX holds c multcomplex is_distributive_wrt addcomplex by ;

definition
func abscomplex -> Function of COMPLEX,REAL means :Def5: :: SEQ_4:def 5
for c being Element of COMPLEX holds it . c = |.c.|;
existence
ex b1 being Function of COMPLEX,REAL st
for c being Element of COMPLEX holds b1 . c = |.c.|
proof end;
uniqueness
for b1, b2 being Function of COMPLEX,REAL st ( for c being Element of COMPLEX holds b1 . c = |.c.| ) & ( for c being Element of COMPLEX holds b2 . c = |.c.| ) holds
b1 = b2
from
end;

:: deftheorem Def5 defines abscomplex SEQ_4:def 5 :
for b1 being Function of COMPLEX,REAL holds
( b1 = abscomplex iff for c being Element of COMPLEX holds b1 . c = |.c.| );

definition
let z1, z2 be FinSequence of COMPLEX ;
:: original: +
redefine func z1 + z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 6
coherence
z1 + z2 is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = z1 + z2 iff b1 = addcomplex .: (z1,z2) )
proof end;
:: original: -
redefine func z1 - z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 7
diffcomplex .: (z1,z2);
coherence
z1 - z2 is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = z1 - z2 iff b1 = diffcomplex .: (z1,z2) )
proof end;
end;

:: deftheorem defines + SEQ_4:def 6 :
for z1, z2 being FinSequence of COMPLEX holds z1 + z2 = addcomplex .: (z1,z2);

:: deftheorem defines - SEQ_4:def 7 :
for z1, z2 being FinSequence of COMPLEX holds z1 - z2 = diffcomplex .: (z1,z2);

definition
let z be FinSequence of COMPLEX ;
:: original: -
redefine func - z -> FinSequence of COMPLEX equals :: SEQ_4:def 8
compcomplex * z;
coherence
- z is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = - z iff b1 = compcomplex * z )
proof end;
end;

:: deftheorem defines - SEQ_4:def 8 :
for z being FinSequence of COMPLEX holds - z = compcomplex * z;

notation
let z be FinSequence of COMPLEX ;
let c be Complex;
synonym c * z for c (#) z;
end;

definition
let z be FinSequence of COMPLEX ;
let c be Complex;
:: original: *
redefine func c * z -> FinSequence of COMPLEX equals :: SEQ_4:def 9
() * z;
coherence
c * z is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = c * z iff b1 = () * z )
proof end;
end;

:: deftheorem defines * SEQ_4:def 9 :
for z being FinSequence of COMPLEX
for c being Complex holds c * z = () * z;

definition
let z be FinSequence of COMPLEX ;
:: original: |.
redefine func abs z -> FinSequence of REAL equals :: SEQ_4:def 10
abscomplex * z;
coherence
|.z.| is FinSequence of REAL
proof end;
compatibility
for b1 being FinSequence of REAL holds
( b1 = |.z.| iff b1 = abscomplex * z )
proof end;
end;

:: deftheorem defines abs SEQ_4:def 10 :
for z being FinSequence of COMPLEX holds abs z = abscomplex * z;

definition
let n be Nat;
correctness
coherence ;
;
end;

:: deftheorem defines COMPLEX SEQ_4:def 11 :
for n being Nat holds COMPLEX n = n -tuples_on COMPLEX;

registration
let n be Nat;
cluster COMPLEX n -> non empty ;
coherence
not COMPLEX n is empty
;
end;

Lm4: for n being Nat
for z being Element of COMPLEX n holds dom z = Seg n

proof end;

theorem Th57: :: SEQ_4:57
for k, n being Nat
for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX
proof end;

definition
let n be Nat;
let z1, z2 be Element of COMPLEX n;
:: original: +
redefine func z1 + z2 -> Element of COMPLEX n;
coherence
z1 + z2 is Element of COMPLEX n
by FINSEQ_2:120;
end;

theorem Th58: :: SEQ_4:58
for k, n being 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 Nat;
func 0c n -> FinSequence of COMPLEX equals :: SEQ_4:def 12
n |-> 0c;
correctness
coherence ;
;
end;

:: deftheorem defines 0c SEQ_4:def 12 :
for n being Nat holds 0c n = n |-> 0c;

definition
let n be Nat;
:: original: 0c
redefine func 0c n -> Element of COMPLEX n;
coherence
0c n is Element of COMPLEX n
;
end;

theorem :: SEQ_4:59
for n being Nat
for z being Element of COMPLEX n holds
( z + (0c n) = z & z = (0c n) + z ) by ;

definition
let n be Nat;
let z be Element of COMPLEX n;
:: original: -
redefine func - z -> Element of COMPLEX n;
coherence
- z is Element of COMPLEX n
by FINSEQ_2:113;
end;

theorem Th60: :: SEQ_4:60
for k, n being 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;

Lm5: for n being Nat holds - (0c n) = 0c n
proof end;

theorem :: SEQ_4:61
for n being Nat
for z being Element of COMPLEX n holds
( z + (- z) = 0c n & (- z) + z = 0c n ) by ;

theorem :: SEQ_4:62
for n being Nat
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 & z2 = - z1 ) by ;

theorem :: SEQ_4:63
canceled;

::$CT theorem :: SEQ_4:64 for n being Nat for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds z1 = z2 proof end; Lm6: for n being Nat for z, z1, z2 being Element of COMPLEX n st z1 + z = z2 + z holds z1 = z2 proof end; theorem :: SEQ_4:65 for n being Nat for z, z1, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds z1 = z2 by Lm6; theorem Th65: :: SEQ_4:66 for n being Nat for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2) proof end; definition let n be Nat; let z1, z2 be Element of COMPLEX n; :: original: - redefine func z1 - z2 -> Element of COMPLEX n; coherence z1 - z2 is Element of COMPLEX n by FINSEQ_2:120; end; theorem :: SEQ_4:67 for k, n being 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:68 for n being Nat for z being Element of COMPLEX n holds z - (0c n) = z proof end; theorem :: SEQ_4:69 for n being Nat for z being Element of COMPLEX n holds (0c n) - z = - z proof end; theorem :: SEQ_4:70 for n being Nat for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2 ; theorem Th70: :: SEQ_4:71 for n being Nat for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1 proof end; theorem Th71: :: SEQ_4:72 for n being Nat for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2 proof end; theorem Th72: :: SEQ_4:73 for n being Nat for z being Element of COMPLEX n holds z - z = 0c n proof end; theorem Th73: :: SEQ_4:74 for n being Nat for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds z1 = z2 proof end; theorem Th74: :: SEQ_4:75 for n being Nat for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) - z3 = z1 - (z2 + z3) proof end; theorem Th75: :: SEQ_4:76 for n being Nat for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3 proof end; theorem :: SEQ_4:77 for n being Nat for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3 proof end; theorem :: SEQ_4:78 for n being Nat for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) + z3 = (z1 + z3) - z2 by Th75; theorem Th78: :: SEQ_4:79 for n being Nat for z, z1 being Element of COMPLEX n holds z1 = (z1 + z) - z proof end; theorem Th79: :: SEQ_4:80 for n being Nat for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2 proof end; theorem Th80: :: SEQ_4:81 for n being Nat for z, z1 being Element of COMPLEX n holds z1 = (z1 - z) + z proof end; definition let n be Nat; let z be Element of COMPLEX n; let c be Element of COMPLEX ; :: original: * redefine func c * z -> Element of COMPLEX n; coherence c * z is Element of COMPLEX n by FINSEQ_2:113; end; theorem Th81: :: SEQ_4:82 for k, n being Nat for c, c9 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:83 for n being 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:84 for n being 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:85 for n being Nat for c being Element of COMPLEX for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2) by ; theorem :: SEQ_4:86 for n being Nat for z being Element of COMPLEX n holds 1r * z = z proof end; theorem :: SEQ_4:87 for n being Nat for z being Element of COMPLEX n holds 0c * z = 0c n proof end; theorem :: SEQ_4:88 for n being Nat for z being Element of COMPLEX n holds () * z = - z ; definition let n be Nat; let z be Element of COMPLEX n; :: original: |. redefine func abs z -> Element of n -tuples_on REAL; correctness coherence ; by FINSEQ_2:113; end; theorem Th88: :: SEQ_4:89 for k, n being 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 Th89: :: SEQ_4:90 for n being Nat holds abs (0c n) = n |-> 0 proof end; theorem Th90: :: SEQ_4:91 for n being Nat for z being Element of COMPLEX n holds abs (- z) = abs z proof end; theorem Th91: :: SEQ_4:92 for n being 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 13 sqrt (Sum (sqr (abs z))); correctness coherence sqrt (Sum (sqr (abs z))) is Real ; ; end; :: deftheorem defines |. SEQ_4:def 13 : for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z))); theorem Th92: :: SEQ_4:93 for n being Nat holds |.(0c n).| = 0 proof end; theorem Th93: :: SEQ_4:94 for n being Nat for z being Element of COMPLEX n st |.z.| = 0 holds z = 0c n proof end; theorem Th94: :: SEQ_4:95 for n being Nat for z being Element of COMPLEX n holds 0 <= |.z.| proof end; theorem :: SEQ_4:96 for n being Nat for z being Element of COMPLEX n holds |.(- z).| = |.z.| by Th90; theorem :: SEQ_4:97 for n being Nat for c being Element of COMPLEX for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.| proof end; theorem Th97: :: SEQ_4:98 for n being Nat for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.| proof end; theorem Th98: :: SEQ_4:99 for n being Nat for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.| proof end; theorem :: SEQ_4:100 for n being Nat for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).| proof end; theorem :: SEQ_4:101 for n being Nat for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).| proof end; theorem Th101: :: SEQ_4:102 for n being Nat for z1, z2 being Element of COMPLEX n holds ( |.(z1 - z2).| = 0 iff z1 = z2 ) proof end; theorem :: SEQ_4:103 for n being Nat for z1, z2 being Element of COMPLEX n st z1 <> z2 holds 0 < |.(z1 - z2).| proof end; theorem Th103: :: SEQ_4:104 for n being Nat for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).| proof end; theorem Th104: :: SEQ_4:105 for n being Nat for z, z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| proof end; definition let n be Nat; let A be Subset of (); attr A is open means :: SEQ_4:def 14 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 defines open SEQ_4:def 14 : for n being Nat for A being Subset of () holds ( A is open iff 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 ) ) ); definition let n be Nat; let A be Subset of (); attr A is closed means :: SEQ_4:def 15 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 15 : for n being Nat for A being Subset of () holds ( A is closed iff 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 ); theorem :: SEQ_4:106 for n being Nat for A being Subset of () st A = {} holds A is open ; theorem :: SEQ_4:107 for n being Nat for A being Subset of () st A = COMPLEX n holds A is open proof end; theorem :: SEQ_4:108 for n being Nat for AA being Subset-Family of () st ( for A being Subset of () st A in AA holds A is open ) holds for A being Subset of () st A = union AA holds A is open proof end; theorem :: SEQ_4:109 for n being Nat for A, B being Subset of () st A is open & B is open holds for C being Subset of () st C = A /\ B holds C is open proof end; definition let n be Nat; let x be Element of COMPLEX n; let r be Real; func Ball (x,r) -> Subset of () equals :: SEQ_4:def 16 { z where z is Element of COMPLEX n : |.(z - x).| < r } ; coherence { z where z is Element of COMPLEX n : |.(z - x).| < r } is Subset of () proof end; end; :: deftheorem defines Ball SEQ_4:def 16 : for n being Nat for x being Element of COMPLEX n for r being Real holds Ball (x,r) = { z where z is Element of COMPLEX n : |.(z - x).| < r } ; theorem Th109: :: SEQ_4:110 for n being Nat for r being Real for x, z being Element of COMPLEX n holds ( z in Ball (x,r) iff |.(x - z).| < r ) proof end; theorem :: SEQ_4:111 for n being 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:112 for n being Nat for r1 being Real for z1 being Element of COMPLEX n holds Ball (z1,r1) is open proof end; definition let n be Nat; let x be Element of COMPLEX n; let A be Subset of (); func dist (x,A) -> Real means :Def17: :: SEQ_4:def 17 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 ex b1 being Real st for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds b1 = lower_bound X proof end; uniqueness for b1, b2 being Real st ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds b1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds b2 = lower_bound X ) holds b1 = b2 proof end; end; :: deftheorem Def17 defines dist SEQ_4:def 17 : for n being Nat for x being Element of COMPLEX n for A being Subset of () for b4 being Real holds ( b4 = dist (x,A) iff for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds b4 = lower_bound X ); definition let n be Nat; let A be Subset of (); let r be Real; func Ball (A,r) -> Subset of () equals :: SEQ_4:def 18 { z where z is Element of COMPLEX n : dist (z,A) < r } ; coherence { z where z is Element of COMPLEX n : dist (z,A) < r } is Subset of () proof end; end; :: deftheorem defines Ball SEQ_4:def 18 : for n being Nat for A being Subset of () for r being Real holds Ball (A,r) = { z where z is Element of COMPLEX n : dist (z,A) < r } ; theorem Th112: :: SEQ_4:113 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 Th113: :: SEQ_4:114 for n being Nat for x being Element of COMPLEX n for A being Subset of () st A <> {} holds dist (x,A) >= 0 proof end; theorem Th114: :: SEQ_4:115 for n being Nat for x, z being Element of COMPLEX n for A being Subset of () st A <> {} holds dist ((x + z),A) <= (dist (x,A)) + |.z.| proof end; theorem Th115: :: SEQ_4:116 for n being Nat for x being Element of COMPLEX n for A being Subset of () st x in A holds dist (x,A) = 0 proof end; theorem :: SEQ_4:117 for n being Nat for x being Element of COMPLEX n for A being Subset of () st not x in A & A <> {} & A is closed holds dist (x,A) > 0 proof end; theorem :: SEQ_4:118 for n being Nat for x, z1 being Element of COMPLEX n for A being Subset of () st A <> {} holds |.(z1 - x).| + (dist (x,A)) >= dist (z1,A) proof end; theorem Th118: :: SEQ_4:119 for n being Nat for r being Real for z being Element of COMPLEX n for A being Subset of () holds ( z in Ball (A,r) iff dist (z,A) < r ) proof end; theorem Th119: :: SEQ_4:120 for n being Nat for r being Real for x being Element of COMPLEX n for A being Subset of () st 0 < r & x in A holds x in Ball (A,r) proof end; theorem :: SEQ_4:121 for n being Nat for r being Real for A being Subset of () st 0 < r holds A c= Ball (A,r) by Th119; theorem :: SEQ_4:122 for n being Nat for r1 being Real for A being Subset of () st A <> {} holds Ball (A,r1) is open proof end; definition let n be Nat; let A, B be Subset of (); func dist (A,B) -> Real means :Def19: :: SEQ_4:def 19 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 ex b1 being Real st 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 b1 = lower_bound X proof end; uniqueness for b1, b2 being Real st ( 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 b1 = lower_bound X ) & ( 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 b2 = lower_bound X ) holds b1 = b2 proof end; end; :: deftheorem Def19 defines dist SEQ_4:def 19 : for n being Nat for A, B being Subset of () for b4 being Real holds ( b4 = dist (A,B) iff 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 b4 = lower_bound X ); theorem :: SEQ_4:123 for X, Y being Subset of REAL st X <> {} & Y <> {} holds X ++ Y <> {} ; theorem Th123: :: SEQ_4:124 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 Th124: :: SEQ_4:125 for X, Y being Subset of REAL st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds lower_bound (X ++ Y) = () + () proof end; theorem Th125: :: SEQ_4:126 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 Th126: :: SEQ_4:127 for n being Nat for A, B being Subset of () st A <> {} & B <> {} holds dist (A,B) >= 0 proof end; theorem :: SEQ_4:128 for n being Nat for A, B being Subset of () holds dist (A,B) = dist (B,A) proof end; theorem Th128: :: SEQ_4:129 for n being Nat for x being Element of COMPLEX n for A, B being Subset of () st A <> {} & B <> {} holds (dist (x,A)) + (dist (x,B)) >= dist (A,B) proof end; theorem :: SEQ_4:130 for n being Nat for A, B being Subset of () st A meets B holds dist (A,B) = 0 proof end; definition let n be Nat; func ComplexOpenSets n -> Subset-Family of () equals :: SEQ_4:def 20 { A where A is Subset of () : A is open } ; coherence { A where A is Subset of () : A is open } is Subset-Family of () proof end; end; :: deftheorem defines ComplexOpenSets SEQ_4:def 20 : for n being Nat holds ComplexOpenSets n = { A where A is Subset of () : A is open } ; theorem :: SEQ_4:131 for n being Nat for A being Subset of () holds ( A in ComplexOpenSets n iff A is open ) proof end; theorem :: SEQ_4:132 for n being Nat for A being Subset of () holds ( A is closed iff A ` is open ) proof end; defpred S1[ 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 );

Lm7: S1[ 0 ]
;

Lm8: for n being Nat st S1[n] holds
S1[n + 1]

proof end;

Lm9: for n being Nat holds S1[n]
from
theorem Th132: :: SEQ_4:133
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:134
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:135
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:136
for D being non empty set
for f1, f2 being FinSequence of D
for n being Nat st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
proof end;

theorem :: SEQ_4:137
for v being FinSequence of REAL st v is increasing holds
for n, m being Nat st n in dom v & m in dom v & n <= m holds
v . n <= v . m
proof end;

theorem Th137: :: SEQ_4:138
for v being FinSequence of REAL st v is increasing holds
for n, m being Nat st n in dom v & m in dom v & n <> m holds
v . n <> v . m
proof end;

theorem Th138: :: SEQ_4:139
for v, v1 being FinSequence of REAL
for n being Nat st v is increasing & v1 = v | (Seg n) holds
v1 is increasing
proof end;

defpred S2[ 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 ); Lm10: S2[ 0 ] proof end; Lm11: for n being Nat st S2[n] holds S2[n + 1] proof end; Lm12: for n being Nat holds S2[n] from theorem :: SEQ_4:140 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 Lm12; defpred S3[ 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;

Lm13: S3[ 0 ]
proof end;

Lm14: for n being Nat st S3[n] holds
S3[n + 1]

proof end;

Lm15: for n being Nat holds S3[n]
from
theorem :: SEQ_4:141
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 Lm15;

definition
let v be FinSequence of REAL ;
func Incr v -> increasing FinSequence of REAL means :Def21: :: SEQ_4:def 21
( rng it = rng v & len it = card (rng v) );
existence
ex b1 being increasing FinSequence of REAL st
( rng b1 = rng v & len b1 = card (rng v) )
proof end;
uniqueness
for b1, b2 being increasing FinSequence of REAL st rng b1 = rng v & len b1 = card (rng v) & rng b2 = rng v & len b2 = card (rng v) holds
b1 = b2
by Lm15;
end;

:: deftheorem Def21 defines Incr SEQ_4:def 21 :
for v being FinSequence of REAL
for b2 being increasing FinSequence of REAL holds
( b2 = Incr v iff ( rng b2 = rng v & len b2 = card (rng v) ) );

registration
let v be non empty FinSequence of REAL ;
cluster Incr v -> non empty increasing ;
coherence
not Incr v is empty
proof end;
end;

:: from SPRECT_1, 2011.04.24, A.T
registration
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is bounded_above & b1 is bounded_below )
proof end;
end;

theorem :: SEQ_4:142
for A, B being non empty bounded_below Subset of REAL holds lower_bound (A \/ B) = min ((),())
proof end;

theorem :: SEQ_4:143
for A, B being non empty bounded_above Subset of REAL holds upper_bound (A \/ B) = max ((),())
proof end;

:: from TOPMETR3, 2011.04.24, A.T
theorem :: SEQ_4:144
for R being non empty Subset of REAL
for r0 being Real st ( for r being Real st r in R holds
r <= r0 ) holds
upper_bound R <= r0
proof end;