:: TOPRNS_1 semantic presentation

definition

let c₁ be Nat;
mode Real_Sequence of a₁ is sequence of (TOP-REAL a₁);

end;

theorem Th1: :: TOPRNS_1:1

canceled;

theorem Th2: :: TOPRNS_1:2

for b₁ being Nat
for b₂ being Function holds
( b₂ is Real_Sequence of b₁ iff ( dom b₂ = NAT & ( for b₃ being Nat holds b₂ . b₃ is Point of (TOP-REAL b₁) ) ) )

proof end;

definition

let c₁ be Nat;
let c₂ be Real_Sequence of c₁;
attr a₂ is non-zero means :Def1: :: TOPRNS_1:def 1
rng a₂ c= the carrier of (TOP-REAL a₁) \ {(0.REAL a₁)};

end;

:: deftheorem Def1 defines non-zero TOPRNS_1:def 1 :

theorem Th3: :: TOPRNS_1:3

for b₁ being Nat
for b₂ being Real_Sequence of b₁ holds
( b₂ is non-zero iff for b₃ being set st b₃ in NAT holds
b₂ . b₃ <> 0.REAL b₁ )

proof end;

theorem Th4: :: TOPRNS_1:4

for b₁ being Nat
for b₂ being Real_Sequence of b₁ holds
( b₂ is non-zero iff for b₃ being Nat holds b₂ . b₃ <> 0.REAL b₁ )

proof end;

theorem Th5: :: TOPRNS_1:5

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ st ( for b₄ being set st b₄ in NAT holds
b₂ . b₄ = b₃ . b₄ ) holds
b₂ = b₃

proof end;

theorem Th6: :: TOPRNS_1:6

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ st ( for b₄ being Nat holds b₂ . b₄ = b₃ . b₄ ) holds
b₂ = b₃

proof end;

scheme :: TOPRNS_1:sch 1
s1{ F₁() -> Nat, F₂( Nat) -> Point of (TOP-REAL F₁()) } :

ex b₁ being Real_Sequence of F₁() st
for b₂ being Nat holds b₁ . b₂ = F₂(b₂)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Real_Sequence of c₁;
func c₂ + c₃ -> Real_Sequence of a₁ means :Def2: :: TOPRNS_1:def 2
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines + TOPRNS_1:def 2 :

definition

let c₁ be Real;
let c₂ be Nat;
let c₃ be Real_Sequence of c₂;
func c₁ * c₃ -> Real_Sequence of a₂ means :Def3: :: TOPRNS_1:def 3
for b₁ being Nat holds a₄ . b₁ = a₁ * (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines * TOPRNS_1:def 3 :

definition

let c₁ be Nat;
let c₂ be Real_Sequence of c₁;
func - c₂ -> Real_Sequence of a₁ means :Def4: :: TOPRNS_1:def 4
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines - TOPRNS_1:def 4 :

definition

let c₁ be Nat;
let c₂, c₃ be Real_Sequence of c₁;
func c₂ - c₃ -> Real_Sequence of a₁ equals :: TOPRNS_1:def 5
a₂ + (- a₃);
correctness ;

end;

:: deftheorem Def5 defines - TOPRNS_1:def 5 :

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
func |.c₂.| -> Real means :Def6: :: TOPRNS_1:def 6
ex b₁ being FinSequence of REAL st
( a₂ = b₁ & a₃ = |.b₁.| );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines |. TOPRNS_1:def 6 :

definition

let c₁ be Nat;
let c₂ be Real_Sequence of c₁;
func |.c₂.| -> Real_Sequence means :Def7: :: TOPRNS_1:def 7
for b₁ being Nat holds a₃ . b₁ = |.(a₂ . b₁).|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines |. TOPRNS_1:def 7 :

theorem Th7: :: TOPRNS_1:7

canceled;

theorem Th8: :: TOPRNS_1:8

for b₁ being Nat
for b₂ being Real
for b₃ being Point of (TOP-REAL b₁) holds (abs b₂) * |.b₃.| = |.(b₂ * b₃).|

proof end;

theorem Th9: :: TOPRNS_1:9

for b₁ being Nat
for b₂ being Real
for b₃ being Real_Sequence of b₁ holds |.(b₂ * b₃).| = (abs b₂) (#) |.b₃.|

proof end;

theorem Th10: :: TOPRNS_1:10

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ holds b₂ + b₃ = b₃ + b₂

proof end;

theorem Th11: :: TOPRNS_1:11

for b₁ being Nat
for b₂, b₃, b₄ being Real_Sequence of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th12: :: TOPRNS_1:12

for b₁ being Nat
for b₂ being Real_Sequence of b₁ holds - b₂ = (- 1) * b₂

proof end;

theorem Th13: :: TOPRNS_1:13

for b₁ being Nat
for b₂ being Real
for b₃, b₄ being Real_Sequence of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th14: :: TOPRNS_1:14

for b₁ being Nat
for b₂, b₃ being Real
for b₄ being Real_Sequence of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th15: :: TOPRNS_1:15

for b₁ being Nat
for b₂ being Real
for b₃, b₄ being Real_Sequence of b₁ holds b₂ * (b₃ - b₄) = (b₂ * b₃) - (b₂ * b₄)

proof end;

theorem Th16: :: TOPRNS_1:16

for b₁ being Nat
for b₂, b₃, b₄ being Real_Sequence of b₁ holds b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

proof end;

theorem Th17: :: TOPRNS_1:17

for b₁ being Nat
for b₂ being Real_Sequence of b₁ holds 1 * b₂ = b₂

proof end;

theorem Th18: :: TOPRNS_1:18

for b₁ being Nat
for b₂ being Real_Sequence of b₁ holds - (- b₂) = b₂

proof end;

theorem Th19: :: TOPRNS_1:19

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ holds b₂ - (- b₃) = b₂ + b₃ by Th18;

theorem Th20: :: TOPRNS_1:20

for b₁ being Nat
for b₂, b₃, b₄ being Real_Sequence of b₁ holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th21: :: TOPRNS_1:21

for b₁ being Nat
for b₂, b₃, b₄ being Real_Sequence of b₁ holds b₂ + (b₃ - b₄) = (b₂ + b₃) - b₄ by Th11;

theorem Th22: :: TOPRNS_1:22

for b₁ being Nat
for b₂ being Real
for b₃ being Real_Sequence of b₁ st b₂ <> 0 & b₃ is non-zero holds
b₂ * b₃ is non-zero

proof end;

theorem Th23: :: TOPRNS_1:23

for b₁ being Nat
for b₂ being Real_Sequence of b₁ st b₂ is non-zero holds
- b₂ is non-zero

proof end;

theorem Th24: :: TOPRNS_1:24

for b₁ being Nat holds |.(0.REAL b₁).| = 0

proof end;

theorem Th25: :: TOPRNS_1:25

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) st |.b₂.| = 0 holds
b₂ = 0.REAL b₁

proof end;

theorem Th26: :: TOPRNS_1:26

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds |.b₂.| >= 0

proof end;

theorem Th27: :: TOPRNS_1:27

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds |.(- b₂).| = |.b₂.|

proof end;

theorem Th28: :: TOPRNS_1:28

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds |.(b₂ - b₃).| = |.(b₃ - b₂).|

proof end;

Lemma27: for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st |.(b₂ - b₃).| = 0 holds
b₂ = b₃

proof end;

Lemma28: for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ = b₃ holds
|.(b₂ - b₃).| = 0

proof end;

theorem Th29: :: TOPRNS_1:29

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds
( |.(b₂ - b₃).| = 0 iff b₂ = b₃ ) by Lemma27, Lemma28;

theorem Th30: :: TOPRNS_1:30

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds |.(b₂ + b₃).| <= |.b₂.| + |.b₃.|

proof end;

theorem Th31: :: TOPRNS_1:31

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds |.(b₂ - b₃).| <= |.b₂.| + |.b₃.|

proof end;

theorem Th32: :: TOPRNS_1:32

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds |.b₂.| - |.b₃.| <= |.(b₂ + b₃).|

proof end;

theorem Th33: :: TOPRNS_1:33

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds |.b₂.| - |.b₃.| <= |.(b₂ - b₃).|

proof end;

theorem Th34: :: TOPRNS_1:34

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ <> b₃ holds
|.(b₂ - b₃).| > 0

proof end;

theorem Th35: :: TOPRNS_1:35

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds |.(b₂ - b₃).| <= |.(b₂ - b₄).| + |.(b₄ - b₃).|

proof end;

theorem Th36: :: TOPRNS_1:36

for b₁ being Nat
for b₂, b₃ being Real
for b₄, b₅ being Point of (TOP-REAL b₁) st 0 <= b₂ & |.b₄.| < |.b₅.| & b₂ < b₃ holds
|.b₄.| * b₂ < |.b₅.| * b₃

proof end;

theorem Th37: :: TOPRNS_1:37

canceled;

theorem Th38: :: TOPRNS_1:38

for b₁ being Nat
for b₂ being Real
for b₃ being Point of (TOP-REAL b₁) holds
( ( - |.b₃.| < b₂ & b₂ < |.b₃.| ) iff abs b₂ < |.b₃.| )

proof end;

definition

let c₁ be Nat;
let c₂ be Real_Sequence of c₁;
attr a₂ is bounded means :Def8: :: TOPRNS_1:def 8
ex b₁ being Real st
for b₂ being Nat holds |.(a₂ . b₂).| < b₁;

end;

:: deftheorem Def8 defines bounded TOPRNS_1:def 8 :

theorem Th39: :: TOPRNS_1:39

for b₁ being Nat
for b₂ being Real_Sequence of b₁
for b₃ being Nat ex b₄ being Real st
( 0 < b₄ & ( for b₅ being Nat st b₅ <= b₃ holds
|.(b₂ . b₅).| < b₄ ) )

proof end;

definition

let c₁ be Nat;
let c₂ be Real_Sequence of c₁;
attr a₂ is convergent means :Def9: :: TOPRNS_1:def 9
ex b₁ being Point of (TOP-REAL a₁) st
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
|.((a₂ . b₄) - b₁).| < b₂;

end;

:: deftheorem Def9 defines convergent TOPRNS_1:def 9 :

definition

let c₁ be Nat;
let c₂ be Real_Sequence of c₁;
assume E34: c₂ is convergent ;
func lim c₂ -> Point of (TOP-REAL a₁) means :Def10: :: TOPRNS_1:def 10
for b₁ being Real st 0 < b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
|.((a₂ . b₃) - a₃).| < b₁;
existence by E34, Def9;
uniqueness

proof end;

end;

:: deftheorem Def10 defines lim TOPRNS_1:def 10 :

theorem Th40: :: TOPRNS_1:40

canceled;

theorem Th41: :: TOPRNS_1:41

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ + b₃ is convergent

proof end;

theorem Th42: :: TOPRNS_1:42

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ + b₃) = (lim b₂) + (lim b₃)

proof end;

theorem Th43: :: TOPRNS_1:43

for b₁ being Nat
for b₂ being Real
for b₃ being Real_Sequence of b₁ st b₃ is convergent holds
b₂ * b₃ is convergent

proof end;

theorem Th44: :: TOPRNS_1:44

for b₁ being Nat
for b₂ being Real
for b₃ being Real_Sequence of b₁ st b₃ is convergent holds
lim (b₂ * b₃) = b₂ * (lim b₃)

proof end;

theorem Th45: :: TOPRNS_1:45

for b₁ being Nat
for b₂ being Real_Sequence of b₁ st b₂ is convergent holds
- b₂ is convergent

proof end;

theorem Th46: :: TOPRNS_1:46

for b₁ being Nat
for b₂ being Real_Sequence of b₁ st b₂ is convergent holds
lim (- b₂) = - (lim b₂)

proof end;

theorem Th47: :: TOPRNS_1:47

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ - b₃ is convergent

proof end;

theorem Th48: :: TOPRNS_1:48

for b₁ being Nat
for b₂, b₃ being Real_Sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ - b₃) = (lim b₂) - (lim b₃)

proof end;

theorem Th49: :: TOPRNS_1:49

canceled;

theorem Th50: :: TOPRNS_1:50

for b₁ being Nat
for b₂ being Real_Sequence of b₁ st b₂ is convergent holds
b₂ is bounded

proof end;

theorem Th51: :: TOPRNS_1:51

for b₁ being Nat
for b₂ being Real_Sequence of b₁ st b₂ is convergent & lim b₂ <> 0.REAL b₁ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
|.(lim b₂).| / 2 < |.(b₂ . b₄).|

proof end;