:: INTEGRA1 semantic presentation

definition

let c₁ be Subset of REAL ;
attr a₁ is closed-interval means :Def1: :: INTEGRA1:def 1
ex b₁, b₂ being Real st
( b₁ <= b₂ & a₁ = [.b₁,b₂.] );

end;

:: deftheorem Def1 defines closed-interval INTEGRA1:def 1 :

registration

cluster closed-interval Element of bool REAL ;
existence

proof end;

end;

theorem Th1: :: INTEGRA1:1

for b₁ being closed-interval Subset of REAL holds b₁ is compact

proof end;

theorem Th2: :: INTEGRA1:2

for b₁ being closed-interval Subset of REAL holds not b₁ is empty

proof end;

registration

cluster closed-interval -> non empty compact Element of bool REAL ;
coherence by Th1, Th2;

end;

theorem Th3: :: INTEGRA1:3

for b₁ being closed-interval Subset of REAL holds
( b₁ is bounded_below & b₁ is bounded_above )

proof end;

registration

cluster closed-interval -> bounded Element of bool REAL ;
coherence

proof end;

end;

registration

cluster non empty bounded compact closed-interval Element of bool REAL ;
existence

proof end;

end;

theorem Th4: :: INTEGRA1:4

for b₁ being closed-interval Subset of REAL ex b₂, b₃ being Real st
( b₂ <= b₃ & b₂ = inf b₁ & b₃ = sup b₁ )

proof end;

theorem Th5: :: INTEGRA1:5

for b₁ being closed-interval Subset of REAL holds b₁ = [.(inf b₁),(sup b₁).]

proof end;

theorem Th6: :: INTEGRA1:6

for b₁ being closed-interval Subset of REAL
for b₂, b₃, b₄, b₅ being real number st b₁ = [.b₂,b₄.] & b₁ = [.b₃,b₅.] holds
( b₂ = b₃ & b₄ = b₅ )

proof end;

definition

let c₁ be non empty compact Subset of REAL ;
mode DivisionPoint of c₁ -> non empty increasing FinSequence of REAL means :Def2: :: INTEGRA1:def 2
( rng a₂ c= a₁ & a₂ . (len a₂) = sup a₁ );
existence

proof end;

end;

:: deftheorem Def2 defines DivisionPoint INTEGRA1:def 2 :

definition

let c₁ be non empty compact Subset of REAL ;
func divs c₁ -> set means :Def3: :: INTEGRA1:def 3
for b₁ being set holds
( b₁ in a₂ iff b₁ is DivisionPoint of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines divs INTEGRA1:def 3 :

registration

let c₁ be non empty compact Subset of REAL ;
cluster divs a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty compact Subset of REAL ;
mode Division of c₁ -> non empty set means :Def4: :: INTEGRA1:def 4
for b₁ being set holds
( b₁ in a₂ iff b₁ is DivisionPoint of a₁ );
existence

proof end;

end;

:: deftheorem Def4 defines Division INTEGRA1:def 4 :

registration

let c₁ be non empty compact Subset of REAL ;
cluster non empty Division of a₁;
existence

proof end;

end;

definition

let c₁ be non empty compact Subset of REAL ;
let c₂ be non empty Division of c₁;
redefine mode Element as Element of c₂ -> DivisionPoint of a₁;
coherence by Def4;

end;

theorem Th7: :: INTEGRA1:7

canceled;

theorem Th8: :: INTEGRA1:8

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄ being Element of b₃ st b₁ in dom b₄ holds
b₄ . b₁ in b₂

proof end;

theorem Th9: :: INTEGRA1:9

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄ being Element of b₃ st b₁ in dom b₄ & b₁ <> 1 holds
( b₁ - 1 in dom b₄ & b₄ . (b₁ - 1) in b₂ & b₁ - 1 in NAT )

proof end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be non empty Division of c₁;
let c₃ be Element of c₂;
let c₄ be Nat;
assume E13: c₄ in dom c₃ ;
func divset c₃,c₄ -> closed-interval Subset of REAL means :Def5: :: INTEGRA1:def 5
( inf a₅ = inf a₁ & sup a₅ = a₃ . a₄ ) if a₄ = 1
otherwise ( inf a₅ = a₃ . (a₄ - 1) & sup a₅ = a₃ . a₄ );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def5 defines divset INTEGRA1:def 5 :

theorem Th10: :: INTEGRA1:10

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄ being Element of b₃ st b₁ in dom b₄ holds
divset b₄,b₁ c= b₂

proof end;

definition

let c₁ be Subset of REAL ;
func vol c₁ -> Real equals :: INTEGRA1:def 6
(sup a₁) - (inf a₁);
correctness ;

end;

:: deftheorem Def6 defines vol INTEGRA1:def 6 :

theorem Th11: :: INTEGRA1:11

for b₁ being non empty bounded Subset of REAL holds 0 <= vol b₁

proof end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be non empty Division of c₁;
let c₄ be Element of c₃;
func upper_volume c₂,c₄ -> FinSequence of REAL means :Def7: :: INTEGRA1:def 7
( len a₅ = len a₄ & ( for b₁ being Nat st b₁ in Seg (len a₄) holds
a₅ . b₁ = (sup (rng (a₂ | (divset a₄,b₁)))) * (vol (divset a₄,b₁)) ) );
existence

proof end;

uniqueness

proof end;

func lower_volume c₂,c₄ -> FinSequence of REAL means :Def8: :: INTEGRA1:def 8
( len a₅ = len a₄ & ( for b₁ being Nat st b₁ in Seg (len a₄) holds
a₅ . b₁ = (inf (rng (a₂ | (divset a₄,b₁)))) * (vol (divset a₄,b₁)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines upper_volume INTEGRA1:def 7 :

:: deftheorem Def8 defines lower_volume INTEGRA1:def 8 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be non empty Division of c₁;
let c₄ be Element of c₃;
func upper_sum c₂,c₄ -> Real equals :: INTEGRA1:def 9
Sum (upper_volume a₂,a₄);
correctness ;
func lower_sum c₂,c₄ -> Real equals :: INTEGRA1:def 10
Sum (lower_volume a₂,a₄);
correctness ;

end;

:: deftheorem Def9 defines upper_sum INTEGRA1:def 9 :

:: deftheorem Def10 defines lower_sum INTEGRA1:def 10 :

definition

let c₁ be closed-interval Subset of REAL ;
redefine func divs as divs c₁ -> Division of a₁;
coherence

proof end;

end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
func upper_sum_set c₂ -> PartFunc of divs a₁, REAL means :Def11: :: INTEGRA1:def 11
( dom a₃ = divs a₁ & ( for b₁ being Element of divs a₁ st b₁ in dom a₃ holds
a₃ . b₁ = upper_sum a₂,b₁ ) );
existence

proof end;

uniqueness

proof end;

func lower_sum_set c₂ -> PartFunc of divs a₁, REAL means :Def12: :: INTEGRA1:def 12
( dom a₃ = divs a₁ & ( for b₁ being Element of divs a₁ st b₁ in dom a₃ holds
a₃ . b₁ = lower_sum a₂,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines upper_sum_set INTEGRA1:def 11 :

:: deftheorem Def12 defines lower_sum_set INTEGRA1:def 12 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
pred c₂ is_upper_integrable_on c₁ means :Def13: :: INTEGRA1:def 13
rng (upper_sum_set a₂) is bounded_below;
pred c₂ is_lower_integrable_on c₁ means :Def14: :: INTEGRA1:def 14
rng (lower_sum_set a₂) is bounded_above;

end;

:: deftheorem Def13 defines is_upper_integrable_on INTEGRA1:def 13 :

:: deftheorem Def14 defines is_lower_integrable_on INTEGRA1:def 14 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
func upper_integral c₂ -> Real equals :: INTEGRA1:def 15
inf (rng (upper_sum_set a₂));
correctness ;

end;

:: deftheorem Def15 defines upper_integral INTEGRA1:def 15 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
func lower_integral c₂ -> Real equals :: INTEGRA1:def 16
sup (rng (lower_sum_set a₂));
correctness ;

end;

:: deftheorem Def16 defines lower_integral INTEGRA1:def 16 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
pred c₂ is_integrable_on c₁ means :Def17: :: INTEGRA1:def 17
( a₂ is_upper_integrable_on a₁ & a₂ is_lower_integrable_on a₁ & upper_integral a₂ = lower_integral a₂ );

end;

:: deftheorem Def17 defines is_integrable_on INTEGRA1:def 17 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
func integral c₂ -> Real equals :: INTEGRA1:def 18
upper_integral a₂;
correctness ;

end;

:: deftheorem Def18 defines integral INTEGRA1:def 18 :

theorem Th12: :: INTEGRA1:12

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, REAL holds rng (b₂ + b₃) c= (rng b₂) + (rng b₃)

proof end;

theorem Th13: :: INTEGRA1:13

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st b₂ is_bounded_below_on b₁ holds
rng b₂ is bounded_below

proof end;

theorem Th14: :: INTEGRA1:14

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st rng b₂ is bounded_below holds
b₂ is_bounded_below_on b₁

proof end;

theorem Th15: :: INTEGRA1:15

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st b₂ is_bounded_above_on b₁ holds
rng b₂ is bounded_above

proof end;

theorem Th16: :: INTEGRA1:16

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st rng b₂ is bounded_above holds
b₂ is_bounded_above_on b₁

proof end;

theorem Th17: :: INTEGRA1:17

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL st b₂ is_bounded_on b₁ holds
rng b₂ is bounded

proof end;

theorem Th18: :: INTEGRA1:18

for b₁ being non empty set holds chi b₁,b₁ is_constant_on b₁

proof end;

theorem Th19: :: INTEGRA1:19

for b₁ being non empty set
for b₂ being non empty Subset of b₁ holds rng (chi b₂,b₂) = {1}

proof end;

theorem Th20: :: INTEGRA1:20

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃ being set st b₃ meets dom (chi b₂,b₂) holds
rng ((chi b₂,b₂) | b₃) = {1}

proof end;

theorem Th21: :: INTEGRA1:21

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄ being Element of b₃ st b₁ in Seg (len b₄) holds
vol (divset b₄,b₁) = (lower_volume (chi b₂,b₂),b₄) . b₁

proof end;

theorem Th22: :: INTEGRA1:22

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄ being Element of b₃ st b₁ in Seg (len b₄) holds
vol (divset b₄,b₁) = (upper_volume (chi b₂,b₂),b₄) . b₁

proof end;

theorem Th23: :: INTEGRA1:23

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₁ = len b₃ & ( for b₄ being Nat st b₄ in dom b₁ holds
b₃ . b₄ = (b₁ /. b₄) + (b₂ /. b₄) ) holds
Sum b₃ = (Sum b₁) + (Sum b₂)

proof end;

theorem Th24: :: INTEGRA1:24

for b₁, b₂, b₃ being FinSequence of REAL st len b₁ = len b₂ & len b₁ = len b₃ & ( for b₄ being Nat st b₄ in dom b₁ holds
b₃ . b₄ = (b₁ /. b₄) - (b₂ /. b₄) ) holds
Sum b₃ = (Sum b₁) - (Sum b₂)

proof end;

theorem Th25: :: INTEGRA1:25

for b₁ being closed-interval Subset of REAL
for b₂ being non empty Division of b₁
for b₃ being Element of b₂ holds Sum (lower_volume (chi b₁,b₁),b₃) = vol b₁

proof end;

theorem Th26: :: INTEGRA1:26

for b₁ being closed-interval Subset of REAL
for b₂ being non empty Division of b₁
for b₃ being Element of b₂ holds Sum (upper_volume (chi b₁,b₁),b₃) = vol b₁

proof end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be non empty Division of c₁;
let c₄ be Element of c₃;
redefine func upper_volume as upper_volume c₂,c₄ -> non empty FinSequence of REAL ;
coherence

proof end;

end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be non empty Division of c₁;
let c₄ be Element of c₃;
redefine func lower_volume as lower_volume c₂,c₄ -> non empty FinSequence of REAL ;
coherence

proof end;

end;

theorem Th27: :: INTEGRA1:27

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄ being Element of b₃ st b₂ is_bounded_below_on b₁ holds
(inf (rng b₂)) * (vol b₁) <= lower_sum b₂,b₄

proof end;

theorem Th28: :: INTEGRA1:28

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄ being Element of b₃
for b₅ being Nat st b₂ is_bounded_above_on b₁ & b₅ in Seg (len b₄) holds
(sup (rng b₂)) * (vol (divset b₄,b₅)) >= (sup (rng (b₂ | (divset b₄,b₅)))) * (vol (divset b₄,b₅))

proof end;

theorem Th29: :: INTEGRA1:29

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄ being Element of b₃ st b₂ is_bounded_above_on b₁ holds
upper_sum b₂,b₄ <= (sup (rng b₂)) * (vol b₁)

proof end;

theorem Th30: :: INTEGRA1:30

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄ being Element of b₃ st b₂ is_bounded_on b₁ holds
lower_sum b₂,b₄ <= upper_sum b₂,b₄

proof end;

definition

let c₁ be non empty FinSequence of REAL ;
redefine func rng as rng c₁ -> non empty finite Subset of REAL ;
coherence

proof end;

end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be Element of divs c₁;
func delta c₂ -> Real equals :: INTEGRA1:def 19
max (rng (upper_volume (chi a₁,a₁),a₂));
correctness by XREAL_0:def 1;

end;

:: deftheorem Def19 defines delta INTEGRA1:def 19 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be non empty Division of c₁;
let c₃, c₄ be Element of c₂;
pred c₃ <= c₄ means :Def20: :: INTEGRA1:def 20
( len a₃ <= len a₄ & rng a₃ c= rng a₄ );

end;

:: deftheorem Def20 defines <= INTEGRA1:def 20 :

notation

let c₁ be closed-interval Subset of REAL ;
let c₂ be non empty Division of c₁;
let c₃, c₄ be Element of c₂;
synonym c₄ >= c₃ for c₃ <= c₄;

end;

theorem Th31: :: INTEGRA1:31

for b₁ being closed-interval Subset of REAL
for b₂ being non empty Division of b₁
for b₃, b₄ being Element of b₂ st len b₃ = 1 holds
b₃ <= b₄

proof end;

theorem Th32: :: INTEGRA1:32

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃ st b₂ is_bounded_above_on b₁ & len b₄ = 1 holds
upper_sum b₂,b₄ >= upper_sum b₂,b₅

proof end;

theorem Th33: :: INTEGRA1:33

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃ st b₂ is_bounded_below_on b₁ & len b₄ = 1 holds
lower_sum b₂,b₄ <= lower_sum b₂,b₅

proof end;

theorem Th34: :: INTEGRA1:34

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄ being Element of b₃ st b₁ in dom b₄ holds
ex b₅, b₆ being closed-interval Subset of REAL st
( b₅ = [.(inf b₂),(b₄ . b₁).] & b₆ = [.(b₄ . b₁),(sup b₂).] & b₂ = b₅ \/ b₆ )

proof end;

theorem Th35: :: INTEGRA1:35

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₂
for b₄, b₅ being Element of b₃ st b₁ in dom b₄ & b₄ <= b₅ holds
ex b₆ being Nat st
( b₆ in dom b₅ & b₄ . b₁ = b₅ . b₆ )

proof end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be non empty Division of c₁;
let c₃, c₄ be Element of c₂;
let c₅ be Nat;
assume E42: c₃ <= c₄ ;
func indx c₄,c₃,c₅ -> Nat means :Def21: :: INTEGRA1:def 21
( a₆ in dom a₄ & a₃ . a₅ = a₄ . a₆ ) if a₅ in dom a₃
otherwise a₆ = 0;
existence by E42, Th35;
uniqueness

proof end;

correctness ;

end;

:: deftheorem Def21 defines indx INTEGRA1:def 21 :

theorem Th36: :: INTEGRA1:36

for b₁ being increasing FinSequence of REAL
for b₂ being Nat st b₂ <= len b₁ holds
b₁ /^ b₂ is increasing FinSequence of REAL

proof end;

theorem Th37: :: INTEGRA1:37

for b₁ being increasing FinSequence of REAL
for b₂, b₃ being Nat st b₃ in dom b₁ & b₂ <= b₃ holds
mid b₁,b₂,b₃ is increasing FinSequence of REAL

proof end;

theorem Th38: :: INTEGRA1:38

for b₁ being closed-interval Subset of REAL
for b₂ being non empty Division of b₁
for b₃ being Element of b₂
for b₄, b₅ being Nat st b₄ in dom b₃ & b₅ in dom b₃ & b₄ <= b₅ holds
ex b₆ being closed-interval Subset of REAL st
( inf b₆ = (mid b₃,b₄,b₅) . 1 & sup b₆ = (mid b₃,b₄,b₅) . (len (mid b₃,b₄,b₅)) & len (mid b₃,b₄,b₅) = (b₅ - b₄) + 1 & mid b₃,b₄,b₅ is DivisionPoint of b₆ )

proof end;

theorem Th39: :: INTEGRA1:39

for b₁, b₂ being closed-interval Subset of REAL
for b₃ being non empty Division of b₁
for b₄ being non empty Division of b₂
for b₅ being Element of b₃
for b₆, b₇ being Nat st b₆ in dom b₅ & b₇ in dom b₅ & b₆ <= b₇ & b₅ . b₆ >= inf b₂ & b₅ . b₇ = sup b₂ holds
mid b₅,b₆,b₇ is Element of b₄

proof end;

definition

let c₁ be FinSequence of REAL ;
func PartSums c₁ -> FinSequence of REAL means :Def22: :: INTEGRA1:def 22
( len a₂ = len a₁ & ( for b₁ being Nat st b₁ in Seg (len a₁) holds
a₂ . b₁ = Sum (a₁ | b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines PartSums INTEGRA1:def 22 :

theorem Th40: :: INTEGRA1:40

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃ st b₄ <= b₅ & b₂ is_bounded_above_on b₁ holds
for b₆ being non empty Nat st b₆ in dom b₄ holds
Sum ((upper_volume b₂,b₄) | b₆) >= Sum ((upper_volume b₂,b₅) | (indx b₅,b₄,b₆))

proof end;

theorem Th41: :: INTEGRA1:41

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃ st b₄ <= b₅ & b₂ is_bounded_below_on b₁ holds
for b₆ being non empty Nat st b₆ in dom b₄ holds
Sum ((lower_volume b₂,b₄) | b₆) <= Sum ((lower_volume b₂,b₅) | (indx b₅,b₄,b₆))

proof end;

theorem Th42: :: INTEGRA1:42

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃
for b₆ being Nat st b₄ <= b₅ & b₆ in dom b₄ & b₂ is_bounded_above_on b₁ holds
(PartSums (upper_volume b₂,b₄)) . b₆ >= (PartSums (upper_volume b₂,b₅)) . (indx b₅,b₄,b₆)

proof end;

theorem Th43: :: INTEGRA1:43

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃
for b₆ being Nat st b₄ <= b₅ & b₆ in dom b₄ & b₂ is_bounded_below_on b₁ holds
(PartSums (lower_volume b₂,b₄)) . b₆ <= (PartSums (lower_volume b₂,b₅)) . (indx b₅,b₄,b₆)

proof end;

theorem Th44: :: INTEGRA1:44

for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃ being non empty Division of b₁
for b₄ being Element of b₃ holds (PartSums (upper_volume b₂,b₄)) . (len b₄) = upper_sum b₂,b₄

proof end;

theorem Th45: :: INTEGRA1:45

for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃ being non empty Division of b₁
for b₄ being Element of b₃ holds (PartSums (lower_volume b₂,b₄)) . (len b₄) = lower_sum b₂,b₄

proof end;

theorem Th46: :: INTEGRA1:46

for b₁ being closed-interval Subset of REAL
for b₂ being non empty Division of b₁
for b₃, b₄ being Element of b₂ st b₃ <= b₄ holds
indx b₄,b₃,(len b₃) = len b₄

proof end;

theorem Th47: :: INTEGRA1:47

proof end;

theorem Th48: :: INTEGRA1:48

proof end;

theorem Th49: :: INTEGRA1:49

for b₁ being closed-interval Subset of REAL
for b₂ being non empty Division of b₁
for b₃, b₄ being Element of b₂ ex b₅ being Element of b₂ st
( b₃ <= b₅ & b₄ <= b₅ )

proof end;

theorem Th50: :: INTEGRA1:50

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being non empty Division of b₁
for b₄, b₅ being Element of b₃ st b₂ is_bounded_on b₁ holds
lower_sum b₂,b₄ <= upper_sum b₂,b₅

proof end;

theorem Th51: :: INTEGRA1:51

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ holds
upper_integral b₂ >= lower_integral b₂

proof end;

theorem Th52: :: INTEGRA1:52

for b₁, b₂ being Subset of REAL holds (- b₁) + (- b₂) = - (b₁ + b₂)

proof end;

theorem Th53: :: INTEGRA1:53

for b₁, b₂ being Subset of REAL st b₁ is bounded_above & b₂ is bounded_above holds
b₁ + b₂ is bounded_above

proof end;

theorem Th54: :: INTEGRA1:54

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

proof end;

theorem Th55: :: INTEGRA1:55

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃, b₄ being Function of b₂, REAL
for b₅ being non empty Division of b₂
for b₆ being Element of b₅ st b₁ in Seg (len b₆) & b₃ is_bounded_above_on b₂ & b₄ is_bounded_above_on b₂ holds
(upper_volume (b₃ + b₄),b₆) . b₁ <= ((upper_volume b₃,b₆) . b₁) + ((upper_volume b₄,b₆) . b₁)

proof end;

theorem Th56: :: INTEGRA1:56

for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃, b₄ being Function of b₂, REAL
for b₅ being non empty Division of b₂
for b₆ being Element of b₅ st b₁ in Seg (len b₆) & b₃ is_bounded_below_on b₂ & b₄ is_bounded_below_on b₂ holds
((lower_volume b₃,b₆) . b₁) + ((lower_volume b₄,b₆) . b₁) <= (lower_volume (b₃ + b₄),b₆) . b₁

proof end;

theorem Th57: :: INTEGRA1:57

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Function of b₁, REAL
for b₄ being non empty Division of b₁
for b₅ being Element of b₄ st b₂ is_bounded_above_on b₁ & b₃ is_bounded_above_on b₁ holds
upper_sum (b₂ + b₃),b₅ <= (upper_sum b₂,b₅) + (upper_sum b₃,b₅)

proof end;

theorem Th58: :: INTEGRA1:58

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Function of b₁, REAL
for b₄ being non empty Division of b₁
for b₅ being Element of b₄ st b₂ is_bounded_below_on b₁ & b₃ is_bounded_below_on b₁ holds
(lower_sum b₂,b₅) + (lower_sum b₃,b₅) <= lower_sum (b₂ + b₃),b₅

proof end;

theorem Th59: :: INTEGRA1:59

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Function of b₁, REAL st b₂ is_bounded_on b₁ & b₃ is_bounded_on b₁ & b₂ is_integrable_on b₁ & b₃ is_integrable_on b₁ holds
( b₂ + b₃ is_integrable_on b₁ & integral (b₂ + b₃) = (integral b₂) + (integral b₃) )

proof end;