:: INTEGRA2 semantic presentation

theorem Th1: :: INTEGRA2:1

for b₁ being closed-interval Subset of REAL
for b₂ being real number holds
( b₂ in b₁ iff ( inf b₁ <= b₂ & b₂ <= sup b₁ ) )

proof end;

definition

let c₁ be FinSequence of REAL ;
attr a₁ is non-decreasing means :Def1: :: INTEGRA2:def 1
for b₁ being Nat st b₁ in dom a₁ & b₁ + 1 in dom a₁ holds
a₁ . b₁ <= a₁ . (b₁ + 1);

end;

:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :

registration

cluster non-decreasing FinSequence of REAL ;
existence

proof end;

end;

theorem Th2: :: INTEGRA2:2

for b₁ being non-decreasing FinSequence of REAL
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & b₂ <= b₃ holds
b₁ . b₂ <= b₁ . b₃

proof end;

theorem Th3: :: INTEGRA2:3

for b₁ being FinSequence of REAL ex b₂ being non-decreasing FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent

proof end;

theorem Th4: :: INTEGRA2:4

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄, b₅ being Nat st 1 <= b₃ & b₅ <= len b₂ & b₃ <= b₄ & b₄ < b₅ holds
(mid b₂,b₃,b₄) ^ (mid b₂,(b₄ + 1),b₅) = mid b₂,b₃,b₅

proof end;

definition

let c₁ be Subset of REAL ;
let c₂ be real number ;
func c₂ * c₁ -> Subset of REAL means :Def2: :: INTEGRA2:def 2
for b₁ being Real holds
( b₁ in a₃ iff ex b₂ being Real st
( b₂ in a₁ & b₁ = a₂ * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines * INTEGRA2:def 2 :

theorem Th5: :: INTEGRA2:5

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL st b₃ is_bounded_above_on b₁ & b₂ c= b₁ holds
b₃ | b₂ is_bounded_above_on b₂

proof end;

theorem Th6: :: INTEGRA2:6

for b₁, b₂ being non empty set
for b₃ being PartFunc of b₁, REAL st b₃ is_bounded_below_on b₁ & b₂ c= b₁ holds
b₃ | b₂ is_bounded_below_on b₂

proof end;

theorem Th7: :: INTEGRA2:7

for b₁ being Real
for b₂ being non empty Subset of REAL holds not b₁ * b₂ is empty

proof end;

theorem Th8: :: INTEGRA2:8

for b₁ being Real
for b₂ being Subset of REAL holds b₁ * b₂ = { (b₁ * b₃) where B is Real : b₃ in b₂ }

proof end;

theorem Th9: :: INTEGRA2:9

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_above & 0 <= b₁ holds
b₁ * b₂ is bounded_above

proof end;

theorem Th10: :: INTEGRA2:10

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_above & b₁ <= 0 holds
b₁ * b₂ is bounded_below

proof end;

theorem Th11: :: INTEGRA2:11

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_below & 0 <= b₁ holds
b₁ * b₂ is bounded_below

proof end;

theorem Th12: :: INTEGRA2:12

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_below & b₁ <= 0 holds
b₁ * b₂ is bounded_above

proof end;

theorem Th13: :: INTEGRA2:13

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_above & 0 <= b₁ holds
sup (b₁ * b₂) = b₁ * (sup b₂)

proof end;

theorem Th14: :: INTEGRA2:14

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_above & b₁ <= 0 holds
inf (b₁ * b₂) = b₁ * (sup b₂)

proof end;

theorem Th15: :: INTEGRA2:15

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_below & 0 <= b₁ holds
inf (b₁ * b₂) = b₁ * (inf b₂)

proof end;

theorem Th16: :: INTEGRA2:16

for b₁ being Real
for b₂ being non empty Subset of REAL st b₂ is bounded_below & b₁ <= 0 holds
sup (b₁ * b₂) = b₁ * (inf b₂)

proof end;

theorem Th17: :: INTEGRA2:17

for b₁ being Real
for b₂ being non empty set
for b₃ being Function of b₂, REAL holds rng (b₁ (#) b₃) = b₁ * (rng b₃)

proof end;

theorem Th18: :: INTEGRA2:18

for b₁ being Real
for b₂, b₃ being non empty set
for b₄ being PartFunc of b₂, REAL holds rng (b₁ (#) (b₄ | b₃)) = b₁ * (rng (b₄ | b₃))

proof end;

theorem Th19: :: INTEGRA2:19

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄ being Element of divs b₂ st b₃ is_bounded_on b₂ & b₁ >= 0 holds
(upper_sum_set (b₁ (#) b₃)) . b₄ >= (b₁ * (inf (rng b₃))) * (vol b₂)

proof end;

theorem Th20: :: INTEGRA2:20

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄ being Element of divs b₂ st b₃ is_bounded_on b₂ & b₁ <= 0 holds
(upper_sum_set (b₁ (#) b₃)) . b₄ >= (b₁ * (sup (rng b₃))) * (vol b₂)

proof end;

theorem Th21: :: INTEGRA2:21

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄ being Element of divs b₂ st b₃ is_bounded_on b₂ & b₁ >= 0 holds
(lower_sum_set (b₁ (#) b₃)) . b₄ <= (b₁ * (sup (rng b₃))) * (vol b₂)

proof end;

theorem Th22: :: INTEGRA2:22

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄ being Element of divs b₂ st b₃ is_bounded_on b₂ & b₁ <= 0 holds
(lower_sum_set (b₁ (#) b₃)) . b₄ <= (b₁ * (inf (rng b₃))) * (vol b₂)

proof end;

theorem Th23: :: INTEGRA2:23

for b₁ being Real
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₆ in Seg (len b₅) & b₃ is_bounded_above_on b₂ & b₁ >= 0 holds
(upper_volume (b₁ (#) b₃),b₅) . b₆ = b₁ * ((upper_volume b₃,b₅) . b₆)

proof end;

theorem Th24: :: INTEGRA2:24

for b₁ being Real
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₆ in Seg (len b₅) & b₃ is_bounded_above_on b₂ & b₁ <= 0 holds
(lower_volume (b₁ (#) b₃),b₅) . b₆ = b₁ * ((upper_volume b₃,b₅) . b₆)

proof end;

theorem Th25: :: INTEGRA2:25

for b₁ being Real
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₆ in Seg (len b₅) & b₃ is_bounded_below_on b₂ & b₁ >= 0 holds
(lower_volume (b₁ (#) b₃),b₅) . b₆ = b₁ * ((lower_volume b₃,b₅) . b₆)

proof end;

theorem Th26: :: INTEGRA2:26

for b₁ being Real
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₆ in Seg (len b₅) & b₃ is_bounded_below_on b₂ & b₁ <= 0 holds
(upper_volume (b₁ (#) b₃),b₅) . b₆ = b₁ * ((lower_volume b₃,b₅) . b₆)

proof end;

theorem Th27: :: INTEGRA2:27

for b₁ being Real
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₂ & b₁ >= 0 holds
upper_sum (b₁ (#) b₃),b₅ = b₁ * (upper_sum b₃,b₅)

proof end;

theorem Th28: :: INTEGRA2:28

for b₁ being Real
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₂ & b₁ <= 0 holds
lower_sum (b₁ (#) b₃),b₅ = b₁ * (upper_sum b₃,b₅)

proof end;

theorem Th29: :: INTEGRA2:29

for b₁ being Real
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₂ & b₁ >= 0 holds
lower_sum (b₁ (#) b₃),b₅ = b₁ * (lower_sum b₃,b₅)

proof end;

theorem Th30: :: INTEGRA2:30

for b₁ being Real
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₂ & b₁ <= 0 holds
upper_sum (b₁ (#) b₃),b₅ = b₁ * (lower_sum b₃,b₅)

proof end;

theorem Th31: :: INTEGRA2:31

for b₁ being Real
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
( b₁ (#) b₃ is_integrable_on b₂ & integral (b₁ (#) b₃) = b₁ * (integral b₃) )

proof end;

theorem Th32: :: INTEGRA2:32

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₁ & ( for b₃ being Real st b₃ in b₁ holds
b₂ . b₃ >= 0 ) holds
integral b₂ >= 0

proof end;

theorem Th33: :: INTEGRA2:33

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₁ & integral (b₂ - b₃) = (integral b₂) - (integral b₃) )

proof end;

theorem Th34: :: INTEGRA2:34

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₁ & ( for b₄ being Real st b₄ in b₁ holds
b₂ . b₄ >= b₃ . b₄ ) holds
integral b₂ >= integral b₃

proof end;

theorem Th35: :: INTEGRA2:35

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ holds
rng (upper_sum_set b₂) is bounded_below

proof end;

theorem Th36: :: INTEGRA2:36

for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ holds
rng (lower_sum_set b₂) is bounded_above

proof end;

definition

let c₁ be closed-interval Subset of REAL ;
mode DivSequence of a₁ is Function of NAT , divs a₁;

end;

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be DivSequence of c₁;
func delta c₂ -> Real_Sequence means :: INTEGRA2:def 3
for b₁ being Nat holds a₃ . b₁ = delta (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines delta INTEGRA2:def 3 :

definition

let c₁ be closed-interval Subset of REAL ;
let c₂ be PartFunc of c₁, REAL ;
let c₃ be DivSequence of c₁;
func upper_sum c₂,c₃ -> Real_Sequence means :: INTEGRA2:def 4
for b₁ being Nat holds a₄ . b₁ = upper_sum a₂,(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

func lower_sum c₂,c₃ -> Real_Sequence means :: INTEGRA2:def 5
for b₁ being Nat holds a₄ . b₁ = lower_sum a₂,(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines upper_sum INTEGRA2:def 4 :

:: deftheorem Def5 defines lower_sum INTEGRA2:def 5 :

theorem Th37: :: INTEGRA2:37

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Element of divs b₁ st b₂ <= b₃ holds
for b₄ being Nat st b₄ in dom b₃ holds
ex b₅ being Nat st
( b₅ in dom b₂ & divset b₃,b₄ c= divset b₂,b₅ )

proof end;

theorem Th38: :: INTEGRA2:38

for b₁, b₂ being non empty finite Subset of REAL st b₁ c= b₂ holds
max b₁ <= max b₂

proof end;

theorem Th39: :: INTEGRA2:39

for b₁, b₂ being non empty finite Subset of REAL st ex b₃ being Real st
( b₃ in b₂ & max b₁ <= b₃ ) holds
max b₁ <= max b₂

proof end;

theorem Th40: :: INTEGRA2:40

for b₁, b₂ being closed-interval Subset of REAL st b₁ c= b₂ holds
vol b₁ <= vol b₂

proof end;

theorem Th41: :: INTEGRA2:41

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Element of divs b₁ st b₂ <= b₃ holds
delta b₂ >= delta b₃

proof end;