:: INTEGRA4 semantic presentation

theorem Th1: :: INTEGRA4:1

for b₁ being closed-interval Subset of REAL
for b₂ being Element of divs b₁ st vol b₁ = 0 holds
len b₂ = 1

proof end;

theorem Th2: :: INTEGRA4:2

for b₁ being closed-interval Subset of REAL holds
( chi b₁,b₁ is_integrable_on b₁ & integral (chi b₁,b₁) = vol b₁ )

proof end;

theorem Th3: :: INTEGRA4:3

for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃ being Real holds
( ( b₂ is total & rng b₂ = {b₃} ) iff b₂ = b₃ (#) (chi b₁,b₁) )

proof end;

theorem Th4: :: INTEGRA4:4

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being Real st rng b₂ = {b₃} holds
( b₂ is_integrable_on b₁ & integral b₂ = b₃ * (vol b₁) )

proof end;

theorem Th5: :: INTEGRA4:5

for b₁ being closed-interval Subset of REAL
for b₂ being Real ex b₃ being Function of b₁, REAL st
( rng b₃ = {b₂} & b₃ is_bounded_on b₁ )

proof end;

Lemma6: for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of divs b₁ st vol b₁ = 0 holds
( b₂ is_upper_integrable_on b₁ & upper_integral b₂ = 0 )

proof end;

Lemma7: for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of divs b₁ st vol b₁ = 0 holds
( b₂ is_lower_integrable_on b₁ & lower_integral b₂ = 0 )

proof end;

theorem Th6: :: INTEGRA4:6

for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃ being Element of divs b₁ st vol b₁ = 0 holds
( b₂ is_integrable_on b₁ & integral b₂ = 0 )

proof end;

theorem Th7: :: INTEGRA4:7

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ & b₂ is_integrable_on b₁ holds
ex b₃ being Real st
( inf (rng b₂) <= b₃ & b₃ <= sup (rng b₂) & integral b₂ = b₃ * (vol b₁) )

proof end;

theorem Th8: :: INTEGRA4:8

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being DivSequence of b₁ st b₂ is_bounded_on b₁ & delta b₃ is convergent & lim (delta b₃) = 0 holds
( lower_sum b₂,b₃ is convergent & lim (lower_sum b₂,b₃) = lower_integral b₂ )

proof end;

theorem Th9: :: INTEGRA4:9

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃ being DivSequence of b₁ st b₂ is_bounded_on b₁ & delta b₃ is convergent & lim (delta b₃) = 0 holds
( upper_sum b₂,b₃ is convergent & lim (upper_sum b₂,b₃) = upper_integral b₂ )

proof end;

theorem Th10: :: INTEGRA4:10

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ holds
( b₂ is_upper_integrable_on b₁ & b₂ is_lower_integrable_on b₁ )

proof end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be Element of divs c₁;
let c₃ be Nat;
pred c₂ divide_into_equal c₃ means :Def1: :: INTEGRA4:def 1
( len a₂ = a₃ & ( for b₁ being Nat st b₁ in dom a₂ holds
a₂ . b₁ = (inf a₁) + (((vol a₁) / (len a₂)) * b₁) ) );

end;

:: deftheorem Def1 defines divide_into_equal INTEGRA4:def 1 :

Lemma13: for b₁ being closed-interval Subset of REAL
for b₂ being Nat st b₂ > 0 & vol b₁ > 0 holds
ex b₃ being Element of divs b₁ st
( len b₃ = b₂ & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = (inf b₁) + (((vol b₁) / b₂) * b₄) ) )

proof end;

Lemma14: for b₁ being closed-interval Subset of REAL st vol b₁ > 0 holds
ex b₂ being DivSequence of b₁ st
( delta b₂ is convergent & lim (delta b₂) = 0 )

proof end;

Lemma15: for b₁ being closed-interval Subset of REAL st vol b₁ = 0 holds
ex b₂ being DivSequence of b₁ st
( delta b₂ is convergent & lim (delta b₂) = 0 )

proof end;

theorem Th11: :: INTEGRA4:11

for b₁ being closed-interval Subset of REAL ex b₂ being DivSequence of b₁ st
( delta b₂ is convergent & lim (delta b₂) = 0 )

proof end;

theorem Th12: :: INTEGRA4:12

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ holds
( b₂ is_integrable_on b₁ iff for b₃ being DivSequence of b₁ st delta b₃ is convergent & lim (delta b₃) = 0 holds
(lim (upper_sum b₂,b₃)) - (lim (lower_sum b₂,b₃)) = 0 )

proof end;

theorem Th13: :: INTEGRA4:13

for b₁ being non empty set
for b₂ being Function of b₁, REAL holds
( max+ b₂ is total & max- b₂ is total )

proof end;

theorem Th14: :: INTEGRA4:14

for b₁ being non empty set
for b₂ being set
for b₃ being PartFunc of b₁, REAL st b₃ is_bounded_above_on b₂ holds
max+ b₃ is_bounded_above_on b₂

proof end;

theorem Th15: :: INTEGRA4:15

for b₁ being non empty set
for b₂ being set
for b₃ being PartFunc of b₁, REAL holds max+ b₃ is_bounded_below_on b₂

proof end;

theorem Th16: :: INTEGRA4:16

for b₁ being non empty set
for b₂ being set
for b₃ being PartFunc of b₁, REAL st b₃ is_bounded_below_on b₂ holds
max- b₃ is_bounded_above_on b₂

proof end;

theorem Th17: :: INTEGRA4:17

for b₁ being non empty set
for b₂ being set
for b₃ being PartFunc of b₁, REAL holds max- b₃ is_bounded_below_on b₂

proof end;

theorem Th18: :: INTEGRA4:18

for b₁ being closed-interval Subset of REAL
for b₂ being set
for b₃ being PartFunc of b₁, REAL st b₃ is_bounded_above_on b₁ holds
rng (b₃ | b₂) is bounded_above

proof end;

theorem Th19: :: INTEGRA4:19

for b₁ being closed-interval Subset of REAL
for b₂ being set
for b₃ being PartFunc of b₁, REAL st b₃ is_bounded_below_on b₁ holds
rng (b₃ | b₂) is bounded_below

proof end;

theorem Th20: :: INTEGRA4:20

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ & b₂ is_integrable_on b₁ holds
max+ b₂ is_integrable_on b₁

proof end;

theorem Th21: :: INTEGRA4:21

for b₁ being non empty set
for b₂ being PartFunc of b₁, REAL holds max- b₂ = max+ (- b₂)

proof end;

theorem Th22: :: INTEGRA4:22

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ & b₂ is_integrable_on b₁ holds
max- b₂ is_integrable_on b₁

proof end;

theorem Th23: :: INTEGRA4:23

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

proof end;

theorem Th24: :: INTEGRA4:24

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL st ( for b₄, b₅ being Real st b₄ in b₂ & b₅ in b₂ holds
abs ((b₃ . b₄) - (b₃ . b₅)) <= b₁ ) holds
(sup (rng b₃)) - (inf (rng b₃)) <= b₁

proof end;

theorem Th25: :: INTEGRA4:25

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃, b₄ being Function of b₂, REAL st b₃ is_bounded_on b₂ & b₁ >= 0 & ( for b₅, b₆ being Real st b₅ in b₂ & b₆ in b₂ holds
abs ((b₄ . b₅) - (b₄ . b₆)) <= b₁ * (abs ((b₃ . b₅) - (b₃ . b₆))) ) holds
(sup (rng b₄)) - (inf (rng b₄)) <= b₁ * ((sup (rng b₃)) - (inf (rng b₃)))

proof end;

theorem Th26: :: INTEGRA4:26

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃, b₄, b₅ being Function of b₂, REAL st b₃ is_bounded_on b₂ & b₄ is_bounded_on b₂ & b₁ >= 0 & ( for b₆, b₇ being Real st b₆ in b₂ & b₇ in b₂ holds
abs ((b₅ . b₆) - (b₅ . b₇)) <= b₁ * ((abs ((b₃ . b₆) - (b₃ . b₇))) + (abs ((b₄ . b₆) - (b₄ . b₇)))) ) holds
(sup (rng b₅)) - (inf (rng b₅)) <= b₁ * (((sup (rng b₃)) - (inf (rng b₃))) + ((sup (rng b₄)) - (inf (rng b₄))))

proof end;

theorem Th27: :: INTEGRA4:27

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃, b₄ being Function of b₂, REAL st b₃ is_bounded_on b₂ & b₃ is_integrable_on b₂ & b₄ is_bounded_on b₂ & b₁ > 0 & ( for b₅, b₆ being Real st b₅ in b₂ & b₆ in b₂ holds
abs ((b₄ . b₅) - (b₄ . b₆)) <= b₁ * (abs ((b₃ . b₅) - (b₃ . b₆))) ) holds
b₄ is_integrable_on b₂

proof end;

theorem Th28: :: INTEGRA4:28

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃, b₄, b₅ being Function of b₂, REAL st b₃ is_bounded_on b₂ & b₃ is_integrable_on b₂ & b₄ is_bounded_on b₂ & b₄ is_integrable_on b₂ & b₅ is_bounded_on b₂ & b₁ > 0 & ( for b₆, b₇ being Real st b₆ in b₂ & b₇ in b₂ holds
abs ((b₅ . b₆) - (b₅ . b₇)) <= b₁ * ((abs ((b₃ . b₆) - (b₃ . b₇))) + (abs ((b₄ . b₆) - (b₄ . b₇)))) ) holds
b₅ is_integrable_on b₂

proof end;

theorem Th29: :: INTEGRA4:29

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

proof end;

theorem Th30: :: INTEGRA4:30

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ & b₂ is_integrable_on b₁ & not 0 in rng b₂ & b₂ ^ is_bounded_on b₁ holds
b₂ ^ is_integrable_on b₁

proof end;