:: INTEGRA3 semantic presentation

Lemma1: for b₁ being Real
for b₂ being FinSequence of REAL st b₁ in dom b₂ holds
( 1 <= b₁ & b₁ <= len b₂ )

proof end;

Lemma2: for b₁ being Real holds b₁ - 1 <= b₁
by XREAL_1:148;

Lemma3: for b₁ being Nat holds (b₁ -' b₁) + 1 = 1

proof end;

Lemma4: for b₁ being Nat st 1 <= b₁ & b₁ <= 2 & not b₁ = 1 holds
b₁ = 2

proof end;

theorem Th1: :: INTEGRA3:1

for b₁ being closed-interval Subset of REAL
for b₂ being Element of divs b₁ st vol b₁ <> 0 holds
ex b₃ being Nat st
( b₃ in dom b₂ & vol (divset b₂,b₃) > 0 )

proof end;

theorem Th2: :: INTEGRA3:2

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

proof end;

theorem Th3: :: INTEGRA3:3

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Element of divs b₁ ex b₄ being Element of divs b₁ st
( b₂ <= b₄ & b₃ <= b₄ & rng b₄ = (rng b₂) \/ (rng b₃) )

proof end;

theorem Th4: :: INTEGRA3:4

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Element of divs b₁ st delta b₃ < min (rng (upper_volume (chi b₁,b₁),b₂)) holds
for b₄, b₅ being Real
for b₆ being Nat st b₆ in dom b₃ & b₄ in (rng b₂) /\ (divset b₃,b₆) & b₅ in (rng b₂) /\ (divset b₃,b₆) holds
b₄ = b₅

proof end;

theorem Th5: :: INTEGRA3:5

for b₁, b₂ being FinSequence of REAL st rng b₁ = rng b₂ & b₁ is increasing & b₂ is increasing holds
b₁ = b₂

proof end;

theorem Th6: :: INTEGRA3:6

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

proof end;

theorem Th7: :: INTEGRA3:7

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

proof end;

theorem Th8: :: INTEGRA3:8

for b₁ being closed-interval Subset of REAL
for b₂ being Element of divs b₁ holds delta b₂ >= 0

proof end;

Lemma13: for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL st b₂ is_bounded_on b₁ holds
sup (rng b₂) >= inf (rng b₂)

proof end;

Lemma14: for b₁, b₂ being closed-interval Subset of REAL
for b₃ being Function of b₁, REAL st b₃ is_bounded_on b₁ & b₂ c= b₁ holds
( inf (rng (b₃ | b₂)) >= inf (rng b₃) & inf (rng b₃) <= sup (rng (b₃ | b₂)) & sup (rng (b₃ | b₂)) <= sup (rng b₃) & inf (rng (b₃ | b₂)) <= sup (rng b₃) )

proof end;

Lemma15: for b₁ being Nat
for b₂ being closed-interval Subset of REAL
for b₃ being Element of divs b₂ st b₁ in dom b₃ holds
vol (divset b₃,b₁) <= delta b₃

proof end;

Lemma16: for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Nat
for b₄, b₅ being Element of divs b₂ st b₃ = (len b₄) - 1 & b₁ in divset b₄,(len b₄) & len b₄ >= 2 & b₄ <= b₅ & rng b₅ = (rng b₄) \/ {b₁} holds
rng (b₅ | (indx b₅,b₄,b₃)) = rng (b₄ | b₃)

proof end;

theorem Th9: :: INTEGRA3:9

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄, b₅ being Element of divs b₂ st b₁ in divset b₄,(len b₄) & len b₄ >= 2 & b₄ <= b₅ & rng b₅ = (rng b₄) \/ {b₁} & b₃ is_bounded_on b₂ holds
(Sum (lower_volume b₃,b₅)) - (Sum (lower_volume b₃,b₄)) <= ((sup (rng b₃)) - (inf (rng b₃))) * (delta b₄)

proof end;

theorem Th10: :: INTEGRA3:10

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄, b₅ being Element of divs b₂ st b₁ in divset b₄,(len b₄) & len b₄ >= 2 & b₄ <= b₅ & rng b₅ = (rng b₄) \/ {b₁} & b₃ is_bounded_on b₂ holds
(Sum (upper_volume b₃,b₄)) - (Sum (upper_volume b₃,b₅)) <= ((sup (rng b₃)) - (inf (rng b₃))) * (delta b₄)

proof end;

Lemma19: for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being PartFunc of b₂, REAL st vol b₂ <> 0 & b₁ in rng (lower_sum_set b₃) holds
ex b₄ being Element of divs b₂ st
( b₄ in dom (lower_sum_set b₃) & b₁ = (lower_sum_set b₃) . b₄ & b₄ . 1 > inf b₂ )

proof end;

theorem Th11: :: INTEGRA3:11

for b₁ being closed-interval Subset of REAL
for b₂ being Element of divs b₁
for b₃ being Real
for b₄, b₅ being Nat st b₄ in dom b₂ & b₅ in dom b₂ & b₄ <= b₅ & b₃ < (mid b₂,b₄,b₅) . 1 holds
ex b₆ being closed-interval Subset of REAL st
( b₃ = inf b₆ & 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;

Lemma21: for b₁ being closed-interval Subset of REAL
for b₂ being Element of divs b₁ st vol b₁ <> 0 & len b₂ = 1 holds
<*(inf b₁)*> ^ b₂ is non empty increasing FinSequence of REAL

proof end;

Lemma22: for b₁ being closed-interval Subset of REAL
for b₂ being Element of divs b₁ st inf b₁ < b₂ . 1 holds
<*(inf b₁)*> ^ b₂ is non empty increasing FinSequence of REAL

proof end;

Lemma23: for b₁ being closed-interval Subset of REAL
for b₂ being PartFunc of b₁, REAL
for b₃, b₄ being Element of divs b₁ st b₄ = <*(inf b₁)*> ^ b₃ holds
( ( for b₅ being Nat st b₅ in Seg (len b₃) holds
divset b₄,(b₅ + 1) = divset b₃,b₅ ) & upper_volume b₂,b₃ = (upper_volume b₂,b₄) /^ 1 & lower_volume b₂,b₃ = (lower_volume b₂,b₄) /^ 1 )

proof end;

Lemma24: for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Element of divs b₁ st b₃ = <*(inf b₁)*> ^ b₂ holds
vol (divset b₃,1) = 0

proof end;

Lemma25: for b₁ being closed-interval Subset of REAL
for b₂ being Function of b₁, REAL
for b₃, b₄ being Element of divs b₁ st b₄ = <*(inf b₁)*> ^ b₃ holds
delta b₄ = delta b₃

proof end;

theorem Th12: :: INTEGRA3:12

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄, b₅ being Element of divs b₂ st b₁ in divset b₄,(len b₄) & vol b₂ <> 0 & b₄ <= b₅ & rng b₅ = (rng b₄) \/ {b₁} & b₃ is_bounded_on b₂ & b₁ > inf b₂ holds
(Sum (lower_volume b₃,b₅)) - (Sum (lower_volume b₃,b₄)) <= ((sup (rng b₃)) - (inf (rng b₃))) * (delta b₄)

proof end;

theorem Th13: :: INTEGRA3:13

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Function of b₂, REAL
for b₄, b₅ being Element of divs b₂ st b₁ in divset b₄,(len b₄) & vol b₂ <> 0 & b₄ <= b₅ & rng b₅ = (rng b₄) \/ {b₁} & b₃ is_bounded_on b₂ & b₁ > inf b₂ holds
(Sum (upper_volume b₃,b₄)) - (Sum (upper_volume b₃,b₅)) <= ((sup (rng b₃)) - (inf (rng b₃))) * (delta b₄)

proof end;

theorem Th14: :: INTEGRA3:14

for b₁ being closed-interval Subset of REAL
for b₂, b₃ being Element of divs b₁
for b₄ being Real
for b₅, b₆ being Nat st b₅ in dom b₂ & b₆ in dom b₂ & b₅ <= b₆ & b₂ <= b₃ & b₄ < (mid b₃,(indx b₃,b₂,b₅),(indx b₃,b₂,b₆)) . 1 holds
ex b₇ being closed-interval Subset of REAL ex b₈, b₉ being Element of divs b₇ st
( b₄ = inf b₇ & sup b₇ = b₉ . (len b₉) & sup b₇ = b₈ . (len b₈) & b₈ <= b₉ & b₈ = mid b₂,b₅,b₆ & b₉ = mid b₃,(indx b₃,b₂,b₅),(indx b₃,b₂,b₆) )

proof end;

theorem Th15: :: INTEGRA3:15

for b₁ being Real
for b₂ being closed-interval Subset of REAL
for b₃ being Element of divs b₂ st b₁ in rng b₃ holds
( b₃ . 1 <= b₁ & b₁ <= b₃ . (len b₃) )

proof end;

theorem Th16: :: INTEGRA3:16

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

proof end;

theorem Th17: :: INTEGRA3:17

for b₁ being Nat
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₁ in dom b₄ holds
inf (rng (b₃ | (divset b₄,b₁))) <= sup (rng b₃)

proof end;

theorem Th18: :: INTEGRA3:18

for b₁ being Nat
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₁ in dom b₄ holds
sup (rng (b₃ | (divset b₄,b₁))) >= inf (rng b₃)

proof end;

theorem Th19: :: INTEGRA3:19

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_to_0 & vol b₁ <> 0 holds
( lower_sum b₂,b₃ is convergent & lim (lower_sum b₂,b₃) = lower_integral b₂ )

proof end;

theorem Th20: :: INTEGRA3:20

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_to_0 & vol b₁ <> 0 holds
( upper_sum b₂,b₃ is convergent & lim (upper_sum b₂,b₃) = upper_integral b₂ )

proof end;