:: SUPINF_2 semantic presentation

definition

func 0. -> R_eal equals :: SUPINF_2:def 1
0;
correctness by SUPINF_1:10;

end;

:: deftheorem Def1 defines 0. SUPINF_2:def 1 :

definition

let c₁, c₂ be R_eal;
func c₁ + c₂ -> R_eal means :Def2: :: SUPINF_2:def 2
ex b₁, b₂ being Real st
( a₁ = b₁ & a₂ = b₂ & a₃ = b₁ + b₂ ) if ( a₁ in REAL & a₂ in REAL )
a₃ = +infty if ( ( a₁ = +infty & a₂ <> -infty ) or ( a₂ = +infty & a₁ <> -infty ) )
a₃ = -infty if ( ( a₁ = -infty & a₂ <> +infty ) or ( a₂ = -infty & a₁ <> +infty ) )
otherwise a₃ = 0. ;
existence

proof end;

uniqueness ;
consistency by SUPINF_1:6;
commutativity ;

end;

:: deftheorem Def2 defines + SUPINF_2:def 2 :

theorem Th1: :: SUPINF_2:1

for b₁, b₂ being R_eal
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ + b₂ = b₃ + b₄

proof end;

theorem Th2: :: SUPINF_2:2

for b₁ being R_eal holds
( b₁ in REAL or b₁ = +infty or b₁ = -infty )

proof end;

definition

let c₁ be R_eal;
func - c₁ -> R_eal means :Def3: :: SUPINF_2:def 3
ex b₁ being Real st
( a₁ = b₁ & a₂ = - b₁ ) if a₁ in REAL
a₂ = -infty if a₁ = +infty
otherwise a₂ = +infty ;
existence

proof end;

uniqueness ;
consistency ;
involutiveness

proof end;

end;

:: deftheorem Def3 defines - SUPINF_2:def 3 :

definition

let c₁, c₂ be R_eal;
func c₁ - c₂ -> R_eal equals :: SUPINF_2:def 4
a₁ + (- a₂);
coherence ;

end;

:: deftheorem Def4 defines - SUPINF_2:def 4 :

theorem Th3: :: SUPINF_2:3

for b₁ being R_eal
for b₂ being Real st b₁ = b₂ holds
- b₁ = - b₂

proof end;

theorem Th4: :: SUPINF_2:4

- -infty = +infty by Def3, SUPINF_1:6, SUPINF_1:14;

theorem Th5: :: SUPINF_2:5

for b₁, b₂ being R_eal
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ - b₂ = b₃ - b₄

proof end;

theorem Th6: :: SUPINF_2:6

for b₁ being R_eal st b₁ <> +infty holds
( +infty - b₁ = +infty & b₁ - +infty = -infty )

proof end;

theorem Th7: :: SUPINF_2:7

for b₁ being R_eal st b₁ <> -infty holds
( -infty - b₁ = -infty & b₁ - -infty = +infty )

proof end;

theorem Th8: :: SUPINF_2:8

for b₁, b₂ being R_eal holds
( not b₁ + b₂ = +infty or b₁ = +infty or b₂ = +infty )

proof end;

theorem Th9: :: SUPINF_2:9

for b₁, b₂ being R_eal holds
( not b₁ + b₂ = -infty or b₁ = -infty or b₂ = -infty )

proof end;

theorem Th10: :: SUPINF_2:10

for b₁, b₂ being R_eal holds
( not b₁ - b₂ = +infty or b₁ = +infty or b₂ = -infty )

proof end;

theorem Th11: :: SUPINF_2:11

for b₁, b₂ being R_eal holds
( not b₁ - b₂ = -infty or b₁ = -infty or b₂ = +infty )

proof end;

theorem Th12: :: SUPINF_2:12

for b₁, b₂ being R_eal holds
( ( b₁ = +infty & b₂ = -infty ) or ( b₁ = -infty & b₂ = +infty ) or not b₁ + b₂ in REAL or ( b₁ in REAL & b₂ in REAL ) )

proof end;

theorem Th13: :: SUPINF_2:13

for b₁, b₂ being R_eal holds
( ( b₁ = +infty & b₂ = +infty ) or ( b₁ = -infty & b₂ = -infty ) or not b₁ - b₂ in REAL or ( b₁ in REAL & b₂ in REAL ) )

proof end;

theorem Th14: :: SUPINF_2:14

for b₁, b₂, b₃, b₄ being R_eal holds
( ( b₁ = +infty & b₃ = -infty ) or ( b₁ = -infty & b₃ = +infty ) or ( b₂ = +infty & b₄ = -infty ) or ( b₂ = -infty & b₄ = +infty ) or not b₁ <=' b₂ or not b₃ <=' b₄ or b₁ + b₃ <=' b₂ + b₄ )

proof end;

theorem Th15: :: SUPINF_2:15

for b₁, b₂, b₃, b₄ being R_eal holds
( ( b₁ = +infty & b₄ = +infty ) or ( b₁ = -infty & b₄ = -infty ) or ( b₂ = +infty & b₃ = +infty ) or ( b₂ = -infty & b₃ = -infty ) or not b₁ <=' b₂ or not b₃ <=' b₄ or b₁ - b₄ <=' b₂ - b₃ )

proof end;

Lemma17: for b₁ being R_eal holds
( - b₁ in REAL iff b₁ in REAL )

proof end;

Lemma18: for b₁, b₂ being R_eal st b₁ <=' b₂ holds
- b₂ <=' - b₁

proof end;

theorem Th16: :: SUPINF_2:16

for b₁, b₂ being R_eal holds
( b₁ <=' b₂ iff - b₂ <=' - b₁ )

proof end;

theorem Th17: :: SUPINF_2:17

for b₁, b₂ being R_eal holds
( b₁ <' b₂ iff - b₂ <' - b₁ ) by Th16;

theorem Th18: :: SUPINF_2:18

for b₁ being R_eal holds
( b₁ + 0. = b₁ & 0. + b₁ = b₁ )

proof end;

theorem Th19: :: SUPINF_2:19

( -infty <' 0. & 0. <' +infty )

proof end;

theorem Th20: :: SUPINF_2:20

for b₁, b₂, b₃ being R_eal st 0. <=' b₃ & 0. <=' b₁ & b₂ = b₁ + b₃ holds
b₁ <=' b₂

proof end;

Lemma22: for b₁, b₂, b₃, b₄ being R_eal st 0. <=' b₁ & 0. <=' b₃ & b₁ <=' b₂ & b₃ <=' b₄ holds
b₁ + b₃ <=' b₂ + b₄

proof end;

theorem Th21: :: SUPINF_2:21

for b₁ being R_eal st b₁ in NAT holds
0. <=' b₁

proof end;

definition

let c₁, c₂ be non empty Subset of ExtREAL ;
func c₁ + c₂ -> Subset of ExtREAL means :Def5: :: SUPINF_2:def 5
for b₁ being R_eal holds
( b₁ in a₃ iff ex b₂, b₃ being R_eal st
( b₂ in a₁ & b₃ in a₂ & b₁ = b₂ + b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + SUPINF_2:def 5 :

registration

let c₁, c₂ be non empty Subset of ExtREAL ;
cluster a₁ + a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty Subset of ExtREAL ;
func - c₁ -> Subset of ExtREAL means :Def6: :: SUPINF_2:def 6
for b₁ being R_eal holds
( b₁ in a₂ iff ex b₂ being R_eal st
( b₂ in a₁ & b₁ = - b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - SUPINF_2:def 6 :

registration

let c₁ be non empty Subset of ExtREAL ;
cluster - a₁ -> non empty ;
coherence

proof end;

end;

theorem Th22: :: SUPINF_2:22

for b₁ being non empty Subset of ExtREAL holds - (- b₁) = b₁

proof end;

theorem Th23: :: SUPINF_2:23

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal holds
( b₂ in b₁ iff - b₂ in - b₁ )

proof end;

theorem Th24: :: SUPINF_2:24

for b₁, b₂ being non empty Subset of ExtREAL holds
( b₁ c= b₂ iff - b₁ c= - b₂ )

proof end;

theorem Th25: :: SUPINF_2:25

for b₁ being R_eal holds
( b₁ in REAL iff - b₁ in REAL )

proof end;

theorem Th26: :: SUPINF_2:26

for b₁, b₂ being non empty Subset of ExtREAL holds
( ( -infty in b₁ & +infty in b₂ ) or ( +infty in b₁ & -infty in b₂ ) or ( sup b₁ = +infty & sup b₂ = -infty ) or ( sup b₁ = -infty & sup b₂ = +infty ) or sup (b₁ + b₂) <=' (sup b₁) + (sup b₂) )

proof end;

theorem Th27: :: SUPINF_2:27

for b₁, b₂ being non empty Subset of ExtREAL holds
( ( -infty in b₁ & +infty in b₂ ) or ( +infty in b₁ & -infty in b₂ ) or ( inf b₁ = +infty & inf b₂ = -infty ) or ( inf b₁ = -infty & inf b₂ = +infty ) or (inf b₁) + (inf b₂) <=' inf (b₁ + b₂) )

proof end;

theorem Th28: :: SUPINF_2:28

for b₁, b₂ being non empty Subset of ExtREAL st b₁ is bounded_above & b₂ is bounded_above holds
sup (b₁ + b₂) <=' (sup b₁) + (sup b₂)

proof end;

theorem Th29: :: SUPINF_2:29

for b₁, b₂ being non empty Subset of ExtREAL st b₁ is bounded_below & b₂ is bounded_below holds
(inf b₁) + (inf b₂) <=' inf (b₁ + b₂)

proof end;

theorem Th30: :: SUPINF_2:30

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal holds
( b₂ is majorant of b₁ iff - b₂ is minorant of - b₁ )

proof end;

theorem Th31: :: SUPINF_2:31

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal holds
( b₂ is minorant of b₁ iff - b₂ is majorant of - b₁ )

proof end;

theorem Th32: :: SUPINF_2:32

for b₁ being non empty Subset of ExtREAL holds inf (- b₁) = - (sup b₁)

proof end;

theorem Th33: :: SUPINF_2:33

for b₁ being non empty Subset of ExtREAL holds sup (- b₁) = - (inf b₁)

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
redefine func rng as rng c₃ -> non empty Subset of ExtREAL ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
func sup c₃ -> R_eal equals :: SUPINF_2:def 7
sup (rng a₃);
correctness ;

end;

:: deftheorem Def7 defines sup SUPINF_2:def 7 :

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
func inf c₃ -> R_eal equals :: SUPINF_2:def 8
inf (rng a₃);
correctness ;

end;

:: deftheorem Def8 defines inf SUPINF_2:def 8 :

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> R_eal;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be non empty Subset of ExtREAL ;
let c₄ be Function of c₁,c₂;
let c₅ be Function of c₁,c₃;
func c₄ + c₅ -> Function of a₁,a₂ + a₃ means :Def9: :: SUPINF_2:def 9
for b₁ being Element of a₁ holds a₆ . b₁ = (a₄ . b₁) + (a₅ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines + SUPINF_2:def 9 :

theorem Th34: :: SUPINF_2:34

for b₁ being non empty set
for b₂, b₃ being non empty Subset of ExtREAL
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ holds rng (b₄ + b₅) c= (rng b₄) + (rng b₅)

proof end;

theorem Th35: :: SUPINF_2:35

for b₁ being non empty set
for b₂, b₃ being non empty Subset of ExtREAL holds
( ( -infty in b₂ & +infty in b₃ ) or ( +infty in b₂ & -infty in b₃ ) or for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ holds
( ( sup b₄ = +infty & sup b₅ = -infty ) or ( sup b₄ = -infty & sup b₅ = +infty ) or sup (b₄ + b₅) <=' (sup b₄) + (sup b₅) ) )

proof end;

theorem Th36: :: SUPINF_2:36

for b₁ being non empty set
for b₂, b₃ being non empty Subset of ExtREAL holds
( ( -infty in b₂ & +infty in b₃ ) or ( +infty in b₂ & -infty in b₃ ) or for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ holds
( ( inf b₄ = +infty & inf b₅ = -infty ) or ( inf b₄ = -infty & inf b₅ = +infty ) or (inf b₄) + (inf b₅) <=' inf (b₄ + b₅) ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
func - c₃ -> Function of a₁, - a₂ means :Def10: :: SUPINF_2:def 10
for b₁ being Element of a₁ holds a₄ . b₁ = - (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines - SUPINF_2:def 10 :

theorem Th37: :: SUPINF_2:37

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ holds rng (- b₃) = - (rng b₃)

proof end;

theorem Th38: :: SUPINF_2:38

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ holds
( inf (- b₃) = - (sup b₃) & sup (- b₃) = - (inf b₃) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
attr a₃ is bounded_above means :Def11: :: SUPINF_2:def 11
sup a₃ <' +infty ;

end;

:: deftheorem Def11 defines bounded_above SUPINF_2:def 11 :

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
attr a₃ is bounded_below means :Def12: :: SUPINF_2:def 12
-infty <' inf a₃;

end;

:: deftheorem Def12 defines bounded_below SUPINF_2:def 12 :

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
let c₃ be Function of c₁,c₂;
attr a₃ is bounded means :Def13: :: SUPINF_2:def 13
( a₃ is bounded_above & a₃ is bounded_below );

end;

:: deftheorem Def13 defines bounded SUPINF_2:def 13 :

registration

let c₁ be non empty set ;
let c₂ be non empty Subset of ExtREAL ;
cluster bounded -> bounded_above bounded_below M8(a₁,a₂);
coherence by Def13;
cluster bounded_above bounded_below -> bounded M8(a₁,a₂);
coherence by Def13;

end;

theorem Th39: :: SUPINF_2:39

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ holds
( b₃ is bounded iff ( sup b₃ <' +infty & -infty <' inf b₃ ) )

proof end;

theorem Th40: :: SUPINF_2:40

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ holds
( b₃ is bounded_above iff - b₃ is bounded_below )

proof end;

theorem Th41: :: SUPINF_2:41

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ holds
( b₃ is bounded_below iff - b₃ is bounded_above )

proof end;

theorem Th42: :: SUPINF_2:42

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ holds
( b₃ is bounded iff - b₃ is bounded )

proof end;

theorem Th43: :: SUPINF_2:43

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂
for b₄ being Element of b₁ holds
( -infty <=' b₃ . b₄ & b₃ . b₄ <=' +infty ) by SUPINF_1:20, SUPINF_1:21;

theorem Th44: :: SUPINF_2:44

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂
for b₄ being Element of b₁ st b₂ c= REAL holds
( -infty <' b₃ . b₄ & b₃ . b₄ <' +infty )

proof end;

theorem Th45: :: SUPINF_2:45

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂
for b₄ being Element of b₁ holds
( inf b₃ <=' b₃ . b₄ & b₃ . b₄ <=' sup b₃ )

proof end;

theorem Th46: :: SUPINF_2:46

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ st b₂ c= REAL holds
( b₃ is bounded_above iff sup b₃ in REAL )

proof end;

theorem Th47: :: SUPINF_2:47

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ st b₂ c= REAL holds
( b₃ is bounded_below iff inf b₃ in REAL )

proof end;

theorem Th48: :: SUPINF_2:48

for b₁ being non empty set
for b₂ being non empty Subset of ExtREAL
for b₃ being Function of b₁,b₂ st b₂ c= REAL holds
( b₃ is bounded iff ( inf b₃ in REAL & sup b₃ in REAL ) )

proof end;

theorem Th49: :: SUPINF_2:49

for b₁ being non empty set
for b₂, b₃ being non empty Subset of ExtREAL st b₂ c= REAL & b₃ c= REAL holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₄ is bounded_above & b₅ is bounded_above holds
b₄ + b₅ is bounded_above

proof end;

theorem Th50: :: SUPINF_2:50

for b₁ being non empty set
for b₂, b₃ being non empty Subset of ExtREAL st b₂ c= REAL & b₃ c= REAL holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₄ is bounded_below & b₅ is bounded_below holds
b₄ + b₅ is bounded_below

proof end;

theorem Th51: :: SUPINF_2:51

for b₁ being non empty set
for b₂, b₃ being non empty Subset of ExtREAL st b₂ c= REAL & b₃ c= REAL holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₄ is bounded & b₅ is bounded holds
b₄ + b₅ is bounded

proof end;

theorem Th52: :: SUPINF_2:52

ex b₁ being Function of NAT , ExtREAL st
( b₁ is one-to-one & NAT = rng b₁ & rng b₁ is non empty Subset of ExtREAL )

proof end;

notation

let c₁ be non empty set ;
let c₂ be Subset of c₁;
synonym denumerable c₂ for countable c₁;

end;

definition

let c₁ be non empty set ;
let c₂ be Subset of c₁;
redefine attr denumerable as a₂ is denumerable means :Def14: :: SUPINF_2:def 14
( a₂ is empty or ex b₁ being Function of NAT ,a₁ st a₂ = rng b₁ );
compatibility

proof end;

end;

:: deftheorem Def14 defines denumerable SUPINF_2:def 14 :

registration

cluster non empty V34 Element of K40(ExtREAL );
existence

proof end;

end;

definition

mode Denum_Set_of_R_EAL is non empty V34 Subset of ExtREAL ;

end;

definition

let c₁ be set ;
attr a₁ is nonnegative means :Def15: :: SUPINF_2:def 15
for b₁ being R_eal st b₁ in a₁ holds
0. <=' b₁;

end;

:: deftheorem Def15 defines nonnegative SUPINF_2:def 15 :

registration

cluster nonnegative Element of K40(ExtREAL );
existence

proof end;

end;

definition

mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL;

end;

definition

let c₁ be Denum_Set_of_R_EAL;
mode Num of c₁ -> Function of NAT , ExtREAL means :Def16: :: SUPINF_2:def 16
a₁ = rng a₂;
existence by Def14;

end;

:: deftheorem Def16 defines Num SUPINF_2:def 16 :

definition

let c₁ be Function of NAT , ExtREAL ;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> R_eal;
coherence

proof end;

end;

theorem Th53: :: SUPINF_2:53

for b₁ being Denum_Set_of_R_EAL
for b₂ being Num of b₁ ex b₃ being Function of NAT , ExtREAL st
( b₃ . 0 = b₂ . 0 & ( for b₄ being Nat
for b₅ being R_eal st b₅ = b₃ . b₄ holds
b₃ . (b₄ + 1) = b₅ + (b₂ . (b₄ + 1)) ) )

proof end;

definition

let c₁ be Denum_Set_of_R_EAL;
let c₂ be Num of c₁;
func Ser c₁,c₂ -> Function of NAT , ExtREAL means :Def17: :: SUPINF_2:def 17
( a₃ . 0 = a₂ . 0 & ( for b₁ being Nat
for b₂ being R_eal st b₂ = a₃ . b₁ holds
a₃ . (b₁ + 1) = b₂ + (a₂ . (b₁ + 1)) ) );
existence by Th53;
uniqueness

proof end;

end;

:: deftheorem Def17 defines Ser SUPINF_2:def 17 :

theorem Th54: :: SUPINF_2:54

for b₁ being Pos_Denum_Set_of_R_EAL
for b₂ being Num of b₁
for b₃ being Nat holds 0. <=' b₂ . b₃

proof end;

theorem Th55: :: SUPINF_2:55

for b₁ being Pos_Denum_Set_of_R_EAL
for b₂ being Num of b₁
for b₃ being Nat holds
( (Ser b₁,b₂) . b₃ <=' (Ser b₁,b₂) . (b₃ + 1) & 0. <=' (Ser b₁,b₂) . b₃ )

proof end;

theorem Th56: :: SUPINF_2:56

for b₁ being Pos_Denum_Set_of_R_EAL
for b₂ being Num of b₁
for b₃, b₄ being Nat holds (Ser b₁,b₂) . b₃ <=' (Ser b₁,b₂) . (b₃ + b₄)

proof end;

definition

let c₁ be Denum_Set_of_R_EAL;
mode Set_of_Series of c₁ -> non empty Subset of ExtREAL means :: SUPINF_2:def 18
ex b₁ being Num of a₁ st a₂ = rng (Ser a₁,b₁);
existence

proof end;

end;

:: deftheorem Def18 defines Set_of_Series SUPINF_2:def 18 :

Lemma60: for b₁ being Function of NAT , ExtREAL holds rng b₁ is non empty Subset of ExtREAL

proof end;

definition

let c₁ be Function of NAT , ExtREAL ;
redefine func rng as rng c₁ -> non empty Subset of ExtREAL ;
coherence by Lemma60;

end;

definition

let c₁ be Pos_Denum_Set_of_R_EAL;
let c₂ be Num of c₁;
func SUM c₁,c₂ -> R_eal equals :: SUPINF_2:def 19
sup (rng (Ser a₁,a₂));
coherence ;

end;

:: deftheorem Def19 defines SUM SUPINF_2:def 19 :

definition

let c₁ be Pos_Denum_Set_of_R_EAL;
let c₂ be Num of c₁;
pred c₁ is_sumable c₂ means :: SUPINF_2:def 20
SUM a₁,a₂ in REAL ;

end;

:: deftheorem Def20 defines is_sumable SUPINF_2:def 20 :

theorem Th57: :: SUPINF_2:57

for b₁ being Function of NAT , ExtREAL holds rng b₁ is Denum_Set_of_R_EAL by Def14;

definition

let c₁ be Function of NAT , ExtREAL ;
redefine func rng as rng c₁ -> Denum_Set_of_R_EAL;
coherence by Th57;

end;

definition

let c₁ be Function of NAT , ExtREAL ;
func Ser c₁ -> Function of NAT , ExtREAL means :Def21: :: SUPINF_2:def 21
for b₁ being Num of rng a₁ st b₁ = a₁ holds
a₂ = Ser (rng a₁),b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines Ser SUPINF_2:def 21 :

definition

let c₁ be set ;
let c₂ be Function of c₁, ExtREAL ;
attr a₂ is nonnegative means :Def22: :: SUPINF_2:def 22
rng a₂ is nonnegative;

end;

:: deftheorem Def22 defines nonnegative SUPINF_2:def 22 :

definition

let c₁ be Function of NAT , ExtREAL ;
func SUM c₁ -> R_eal equals :: SUPINF_2:def 23
sup (rng (Ser a₁));
coherence ;

end;

:: deftheorem Def23 defines SUM SUPINF_2:def 23 :

theorem Th58: :: SUPINF_2:58

for b₁ being non empty set
for b₂ being Function of b₁, ExtREAL holds
( b₂ is nonnegative iff for b₃ being Element of b₁ holds 0. <=' b₂ . b₃ )

proof end;

theorem Th59: :: SUPINF_2:59

for b₁ being Function of NAT , ExtREAL
for b₂ being Nat st b₁ is nonnegative holds
( (Ser b₁) . b₂ <=' (Ser b₁) . (b₂ + 1) & 0. <=' (Ser b₁) . b₂ )

proof end;

theorem Th60: :: SUPINF_2:60

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative holds
for b₂, b₃ being Nat holds (Ser b₁) . b₂ <=' (Ser b₁) . (b₂ + b₃)

proof end;

theorem Th61: :: SUPINF_2:61

for b₁, b₂ being Function of NAT , ExtREAL st b₁ is nonnegative & ( for b₃ being Nat holds b₁ . b₃ <=' b₂ . b₃ ) holds
for b₃ being Nat holds (Ser b₁) . b₃ <=' (Ser b₂) . b₃

proof end;

theorem Th62: :: SUPINF_2:62

for b₁, b₂ being Function of NAT , ExtREAL st b₁ is nonnegative & ( for b₃ being Nat holds b₁ . b₃ <=' b₂ . b₃ ) holds
SUM b₁ <=' SUM b₂

proof end;

theorem Th63: :: SUPINF_2:63

for b₁ being Function of NAT , ExtREAL holds
( (Ser b₁) . 0 = b₁ . 0 & ( for b₂ being Nat
for b₃ being R_eal st b₃ = (Ser b₁) . b₂ holds
(Ser b₁) . (b₂ + 1) = b₃ + (b₁ . (b₂ + 1)) ) )

proof end;

theorem Th64: :: SUPINF_2:64

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative & ex b₂ being Nat st b₁ . b₂ = +infty holds
SUM b₁ = +infty

proof end;

definition

let c₁ be Function of NAT , ExtREAL ;
attr a₁ is summable means :Def24: :: SUPINF_2:def 24
SUM a₁ in REAL ;

end;

:: deftheorem Def24 defines summable SUPINF_2:def 24 :

theorem Th65: :: SUPINF_2:65

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative & ex b₂ being Nat st b₁ . b₂ = +infty holds
not b₁ is summable

proof end;

theorem Th66: :: SUPINF_2:66

for b₁, b₂ being Function of NAT , ExtREAL st b₁ is nonnegative & ( for b₃ being Nat holds b₁ . b₃ <=' b₂ . b₃ ) & b₂ is summable holds
b₁ is summable

proof end;

theorem Th67: :: SUPINF_2:67

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative holds
for b₂ being Nat st ( for b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ = 0. ) holds
SUM b₁ = (Ser b₁) . b₂

proof end;

theorem Th68: :: SUPINF_2:68

for b₁ being Function of NAT , ExtREAL st ( for b₂ being Nat holds b₁ . b₂ in REAL ) holds
for b₂ being Nat holds (Ser b₁) . b₂ in REAL

proof end;

theorem Th69: :: SUPINF_2:69

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative & ex b₂ being Nat st
( ( for b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ = 0. ) & ( for b₃ being Nat st b₃ <= b₂ holds
not b₁ . b₃ = +infty ) ) holds
b₁ is summable

proof end;