:: SEQ_1 semantic presentation

definition

mode Real_Sequence is Function of NAT , REAL ;

end;

theorem Th1: :: SEQ_1:1

canceled;

theorem Th2: :: SEQ_1:2

canceled;

theorem Th3: :: SEQ_1:3

for b₁ being Function holds
( b₁ is Real_Sequence iff ( dom b₁ = NAT & ( for b₂ being set st b₂ in NAT holds
b₁ . b₂ is real ) ) )

proof end;

theorem Th4: :: SEQ_1:4

for b₁ being Function holds
( b₁ is Real_Sequence iff ( dom b₁ = NAT & ( for b₂ being Nat holds b₁ . b₂ is real ) ) )

proof end;

definition

let c₁ be Relation;
attr a₁ is real-yielding means :Def1: :: SEQ_1:def 1
rng a₁ c= REAL ;

end;

:: deftheorem Def1 defines real-yielding SEQ_1:def 1 :

registration

let c₁ be set ;
let c₂ be real-membered set ;
cluster -> real-yielding Relation of a₁,a₂;
coherence

proof end;

end;

registration

cluster real-yielding set ;
existence

proof end;

end;

registration

let c₁ be real-yielding Function;
let c₂ be set ;
cluster a₁ . a₂ -> real ;
coherence

proof end;

end;

definition

let c₁ be real-yielding Function;
let c₂ be set ;
redefine func . as c₁ . c₂ -> Real;
coherence by XREAL_0:def 1;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
redefine func . as c₃ . c₄ -> Real;
coherence by XREAL_0:def 1;

end;

registration

let c₁ be real-yielding Relation;
let c₂ be set ;
cluster a₁ | a₂ -> real-yielding ;
coherence

proof end;

end;

notation

let c₁ be PartFunc of NAT , REAL ;
synonym being_not_0 c₁ for non-empty c₁;
synonym c₁ is_not_0 for non-empty c₁;

end;

definition

let c₁ be PartFunc of NAT , REAL ;
redefine attr a₁ is non-empty means :Def2: :: SEQ_1:def 2
rng a₁ c= REAL \ {0};
compatibility

proof end;

end;

:: deftheorem Def2 defines being_not_0 SEQ_1:def 2 :

theorem Th5: :: SEQ_1:5

canceled;

theorem Th6: :: SEQ_1:6

for b₁ being Real_Sequence holds
( b₁ is being_not_0 iff for b₂ being set st b₂ in NAT holds
b₁ . b₂ <> 0 )

proof end;

theorem Th7: :: SEQ_1:7

for b₁ being Real_Sequence holds
( b₁ is being_not_0 iff for b₂ being Nat holds b₁ . b₂ <> 0 )

proof end;

theorem Th8: :: SEQ_1:8

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

proof end;

theorem Th9: :: SEQ_1:9

canceled;

theorem Th10: :: SEQ_1:10

for b₁ being real number ex b₂ being Real_Sequence st rng b₂ = {b₁}

proof end;

scheme :: SEQ_1:sch 1
s1{ F₁( set ) -> real number } :

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

definition

let c₁, c₂ be real-yielding Function;
func c₁ + c₂ -> Function means :Def3: :: SEQ_1:def 3
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) + (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
func c₁ - c₂ -> Function means :Def4: :: SEQ_1:def 4
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) - (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func c₁ (#) c₂ -> Function means :Def5: :: SEQ_1:def 5
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) * (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def3 defines + SEQ_1:def 3 :

:: deftheorem Def4 defines - SEQ_1:def 4 :

:: deftheorem Def5 defines (#) SEQ_1:def 5 :

registration

let c₁, c₂ be real-yielding Function;
cluster a₁ + a₂ -> real-yielding ;
coherence

proof end;

cluster a₁ - a₂ -> real-yielding ;
coherence

proof end;

cluster a₁ (#) a₂ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃, c₄ be PartFunc of c₁,c₂;
redefine func + as c₃ + c₄ -> PartFunc of a₁, REAL ;
coherence

proof end;

redefine func - as c₃ - c₄ -> PartFunc of a₁, REAL ;
coherence

proof end;

redefine func (#) as c₃ (#) c₄ -> PartFunc of a₁, REAL ;
coherence

proof end;

end;

theorem Th11: :: SEQ_1:11

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

proof end;

theorem Th12: :: SEQ_1:12

for b₁, b₂, b₃ being Real_Sequence holds
( b₁ = b₂ (#) b₃ iff for b₄ being Nat holds b₁ . b₄ = (b₂ . b₄) * (b₃ . b₄) )

proof end;

definition

let c₁, c₂ be Real_Sequence;
redefine func + as c₁ + c₂ -> Real_Sequence;
coherence

proof end;

redefine func - as c₁ - c₂ -> Real_Sequence;
coherence

proof end;

redefine func (#) as c₁ (#) c₂ -> Real_Sequence;
coherence

proof end;

end;

definition

let c₁ be real-yielding Function;
let c₂ be real number ;
func c₂ (#) c₁ -> Function means :Def6: :: SEQ_1:def 6
( dom a₃ = dom a₁ & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = a₂ * (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines (#) SEQ_1:def 6 :

registration

let c₁ be real number ;
let c₂ be real-yielding Function;
cluster a₁ (#) a₂ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃ be PartFunc of c₁,c₂;
let c₄ be real number ;
redefine func (#) as c₄ (#) c₃ -> PartFunc of a₁, REAL ;
coherence

proof end;

end;

definition

let c₁ be Real_Sequence;
let c₂ be real number ;
redefine func (#) as c₂ (#) c₁ -> Real_Sequence;
coherence

proof end;

end;

theorem Th13: :: SEQ_1:13

for b₁ being real number
for b₂, b₃ being Real_Sequence holds
( b₂ = b₁ (#) b₃ iff for b₄ being Nat holds b₂ . b₄ = b₁ * (b₃ . b₄) )

proof end;

definition

let c₁ be real-yielding Function;
func - c₁ -> Function means :Def7: :: SEQ_1:def 7
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₂ holds
a₂ . b₁ = - (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - SEQ_1:def 7 :

registration

let c₁ be real-yielding Function;
cluster - a₁ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃ be PartFunc of c₁,c₂;
redefine func - as - c₃ -> PartFunc of a₁, REAL ;
coherence

proof end;

end;

definition

let c₁ be Real_Sequence;
redefine func - as - c₁ -> Real_Sequence;
coherence

proof end;

end;

theorem Th14: :: SEQ_1:14

for b₁, b₂ being Real_Sequence holds
( b₁ = - b₂ iff for b₃ being Nat holds b₁ . b₃ = - (b₂ . b₃) )

proof end;

theorem Th15: :: SEQ_1:15

for b₁, b₂ being Real_Sequence holds b₁ - b₂ = b₁ + (- b₂)

proof end;

definition

let c₁ be Real_Sequence;
func c₁ " -> Real_Sequence means :Def8: :: SEQ_1:def 8
for b₁ being Nat holds a₂ . b₁ = (a₁ . b₁) " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines " SEQ_1:def 8 :

definition

let c₁, c₂ be Real_Sequence;
func c₁ /" c₂ -> Real_Sequence equals :: SEQ_1:def 9
a₁ (#) (a₂ " );
correctness ;

end;

:: deftheorem Def9 defines /" SEQ_1:def 9 :

definition

let c₁ be real-yielding Function;
func abs c₁ -> Function means :Def10: :: SEQ_1:def 10
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₂ holds
a₂ . b₁ = abs (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines abs SEQ_1:def 10 :

registration

let c₁ be real-yielding Function;
cluster abs a₁ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃ be PartFunc of c₁,c₂;
redefine func abs as abs c₃ -> PartFunc of a₁, REAL ;
coherence

proof end;

end;

definition

let c₁ be Real_Sequence;
redefine func abs as abs c₁ -> Real_Sequence;
coherence

proof end;

end;

theorem Th16: :: SEQ_1:16

for b₁, b₂ being Real_Sequence holds
( b₁ = abs b₂ iff for b₃ being Nat holds b₁ . b₃ = abs (b₂ . b₃) )

proof end;

theorem Th17: :: SEQ_1:17

canceled;

theorem Th18: :: SEQ_1:18

canceled;

theorem Th19: :: SEQ_1:19

canceled;

theorem Th20: :: SEQ_1:20

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

proof end;

theorem Th21: :: SEQ_1:21

canceled;

theorem Th22: :: SEQ_1:22

for b₁, b₂, b₃ being Real_Sequence holds (b₁ (#) b₂) (#) b₃ = b₁ (#) (b₂ (#) b₃)

proof end;

theorem Th23: :: SEQ_1:23

for b₁, b₂, b₃ being Real_Sequence holds (b₁ + b₂) (#) b₃ = (b₁ (#) b₃) + (b₂ (#) b₃)

proof end;

theorem Th24: :: SEQ_1:24

for b₁, b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ + b₃) = (b₁ (#) b₂) + (b₁ (#) b₃) by Th23;

theorem Th25: :: SEQ_1:25

for b₁ being Real_Sequence holds - b₁ = (- 1) (#) b₁

proof end;

theorem Th26: :: SEQ_1:26

for b₁ being real number
for b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ (#) b₃) = (b₁ (#) b₂) (#) b₃

proof end;

theorem Th27: :: SEQ_1:27

for b₁ being real number
for b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ (#) b₃) = b₂ (#) (b₁ (#) b₃)

proof end;

theorem Th28: :: SEQ_1:28

for b₁, b₂, b₃ being Real_Sequence holds (b₁ - b₂) (#) b₃ = (b₁ (#) b₃) - (b₂ (#) b₃)

proof end;

theorem Th29: :: SEQ_1:29

for b₁, b₂, b₃ being Real_Sequence holds (b₁ (#) b₂) - (b₁ (#) b₃) = b₁ (#) (b₂ - b₃) by Th28;

theorem Th30: :: SEQ_1:30

for b₁ being real number
for b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ + b₃) = (b₁ (#) b₂) + (b₁ (#) b₃)

proof end;

theorem Th31: :: SEQ_1:31

for b₁, b₂ being real number
for b₃ being Real_Sequence holds (b₁ * b₂) (#) b₃ = b₁ (#) (b₂ (#) b₃)

proof end;

theorem Th32: :: SEQ_1:32

for b₁ being real number
for b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ - b₃) = (b₁ (#) b₂) - (b₁ (#) b₃)

proof end;

theorem Th33: :: SEQ_1:33

for b₁ being real number
for b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ /" b₃) = (b₁ (#) b₂) /" b₃ by Th26;

theorem Th34: :: SEQ_1:34

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

proof end;

theorem Th35: :: SEQ_1:35

for b₁ being Real_Sequence holds 1 (#) b₁ = b₁

proof end;

theorem Th36: :: SEQ_1:36

for b₁ being Real_Sequence holds - (- b₁) = b₁

proof end;

theorem Th37: :: SEQ_1:37

for b₁, b₂ being Real_Sequence holds b₁ - (- b₂) = b₁ + b₂

proof end;

theorem Th38: :: SEQ_1:38

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

proof end;

theorem Th39: :: SEQ_1:39

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

proof end;

theorem Th40: :: SEQ_1:40

for b₁, b₂ being Real_Sequence holds
( (- b₁) (#) b₂ = - (b₁ (#) b₂) & b₁ (#) (- b₂) = - (b₁ (#) b₂) )

proof end;

theorem Th41: :: SEQ_1:41

for b₁ being Real_Sequence st b₁ is being_not_0 holds
b₁ " is being_not_0

proof end;

theorem Th42: :: SEQ_1:42

for b₁ being Real_Sequence holds (b₁ " ) " = b₁

proof end;

theorem Th43: :: SEQ_1:43

for b₁, b₂ being Real_Sequence holds
( ( b₁ is being_not_0 & b₂ is being_not_0 ) iff b₁ (#) b₂ is being_not_0 )

proof end;

theorem Th44: :: SEQ_1:44

for b₁, b₂ being Real_Sequence holds (b₁ " ) (#) (b₂ " ) = (b₁ (#) b₂) "

proof end;

theorem Th45: :: SEQ_1:45

for b₁, b₂ being Real_Sequence st b₁ is being_not_0 holds
(b₂ /" b₁) (#) b₁ = b₂

proof end;

theorem Th46: :: SEQ_1:46

for b₁, b₂, b₃, b₄ being Real_Sequence holds (b₁ /" b₂) (#) (b₃ /" b₄) = (b₁ (#) b₃) /" (b₂ (#) b₄)

proof end;

theorem Th47: :: SEQ_1:47

for b₁, b₂ being Real_Sequence st b₁ is being_not_0 & b₂ is being_not_0 holds
b₁ /" b₂ is being_not_0

proof end;

theorem Th48: :: SEQ_1:48

for b₁, b₂ being Real_Sequence holds (b₁ /" b₂) " = b₂ /" b₁

proof end;

theorem Th49: :: SEQ_1:49

for b₁, b₂, b₃ being Real_Sequence holds b₁ (#) (b₂ /" b₃) = (b₁ (#) b₂) /" b₃ by Th22;

theorem Th50: :: SEQ_1:50

for b₁, b₂, b₃ being Real_Sequence holds b₁ /" (b₂ /" b₃) = (b₁ (#) b₃) /" b₂

proof end;

theorem Th51: :: SEQ_1:51

for b₁, b₂, b₃ being Real_Sequence st b₁ is being_not_0 holds
b₂ /" b₃ = (b₂ (#) b₁) /" (b₃ (#) b₁)

proof end;

theorem Th52: :: SEQ_1:52

for b₁ being real number
for b₂ being Real_Sequence st b₁ <> 0 & b₂ is being_not_0 holds
b₁ (#) b₂ is being_not_0

proof end;

theorem Th53: :: SEQ_1:53

for b₁ being Real_Sequence st b₁ is being_not_0 holds
- b₁ is being_not_0

proof end;

theorem Th54: :: SEQ_1:54

for b₁ being real number
for b₂ being Real_Sequence holds (b₁ (#) b₂) " = (b₁ " ) (#) (b₂ " )

proof end;

Lemma43: (- 1) " = - 1
;

theorem Th55: :: SEQ_1:55

for b₁ being Real_Sequence holds (- b₁) " = (- 1) (#) (b₁ " )

proof end;

theorem Th56: :: SEQ_1:56

for b₁, b₂ being Real_Sequence holds
( - (b₁ /" b₂) = (- b₁) /" b₂ & b₁ /" (- b₂) = - (b₁ /" b₂) )

proof end;

theorem Th57: :: SEQ_1:57

for b₁, b₂, b₃ being Real_Sequence holds
( (b₁ /" b₂) + (b₃ /" b₂) = (b₁ + b₃) /" b₂ & (b₁ /" b₂) - (b₃ /" b₂) = (b₁ - b₃) /" b₂ ) by Th23, Th28;

theorem Th58: :: SEQ_1:58

for b₁, b₂, b₃, b₄ being Real_Sequence st b₁ is being_not_0 & b₂ is being_not_0 holds
( (b₃ /" b₁) + (b₄ /" b₂) = ((b₃ (#) b₂) + (b₄ (#) b₁)) /" (b₁ (#) b₂) & (b₃ /" b₁) - (b₄ /" b₂) = ((b₃ (#) b₂) - (b₄ (#) b₁)) /" (b₁ (#) b₂) )

proof end;

theorem Th59: :: SEQ_1:59

for b₁, b₂, b₃, b₄ being Real_Sequence holds (b₁ /" b₂) /" (b₃ /" b₄) = (b₁ (#) b₄) /" (b₂ (#) b₃)

proof end;

theorem Th60: :: SEQ_1:60

for b₁, b₂ being Real_Sequence holds abs (b₁ (#) b₂) = (abs b₁) (#) (abs b₂)

proof end;

theorem Th61: :: SEQ_1:61

for b₁ being Real_Sequence st b₁ is being_not_0 holds
abs b₁ is being_not_0

proof end;

theorem Th62: :: SEQ_1:62

for b₁ being Real_Sequence holds (abs b₁) " = abs (b₁ " )

proof end;

theorem Th63: :: SEQ_1:63

for b₁, b₂ being Real_Sequence holds abs (b₁ /" b₂) = (abs b₁) /" (abs b₂)

proof end;

theorem Th64: :: SEQ_1:64

for b₁ being real number
for b₂ being Real_Sequence holds abs (b₁ (#) b₂) = (abs b₁) (#) (abs b₂)

proof end;