:: INTEGRA1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

:: deftheorem Def1 defines closed-interval INTEGRA1:def 1 :
for IT being Subset of REAL holds
( IT is closed-interval iff ex a, b being Real st
( a <= b & IT = [.a,b.] ) );

registration
cluster closed-interval Element of bool REAL ;
existence
ex b1 being Subset of REAL st b1 is closed-interval
proof end;
end;

theorem Th1: :: INTEGRA1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL holds A is compact
proof end;

theorem Th2: :: INTEGRA1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL holds not A is empty
proof end;

registration
cluster closed-interval -> non empty compact Element of bool REAL ;
coherence
for b1 being Subset of REAL st b1 is closed-interval holds
( not b1 is empty & b1 is compact )
by Th1, Th2;
end;

theorem Th3: :: INTEGRA1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL holds
( A is bounded_below & A is bounded_above )
proof end;

registration
cluster closed-interval -> bounded Element of bool REAL ;
coherence
for b1 being Subset of REAL st b1 is closed-interval holds
b1 is bounded
proof end;
end;

registration
cluster non empty bounded compact closed-interval Element of bool REAL ;
existence
ex b1 being Subset of REAL st b1 is closed-interval
proof end;
end;

theorem Th4: :: INTEGRA1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL ex a, b being Real st
( a <= b & a = inf A & b = sup A )
proof end;

theorem Th5: :: INTEGRA1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL holds A = [.(inf A),(sup A).]
proof end;

theorem Th6: :: INTEGRA1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for a1, a2, b1, b2 being real number st A = [.a1,b1.] & A = [.a2,b2.] holds
( a1 = a2 & b1 = b2 )
proof end;

definition
let A be non empty compact Subset of REAL ;
mode DivisionPoint of A -> non empty increasing FinSequence of REAL means :Def2: :: INTEGRA1:def 2
( rng it c= A & it . (len it) = sup A );
existence
ex b1 being non empty increasing FinSequence of REAL st
( rng b1 c= A & b1 . (len b1) = sup A )
proof end;
end;

:: deftheorem Def2 defines DivisionPoint INTEGRA1:def 2 :
for A being non empty compact Subset of REAL
for b2 being non empty increasing FinSequence of REAL holds
( b2 is DivisionPoint of A iff ( rng b2 c= A & b2 . (len b2) = sup A ) );

definition
let A be non empty compact Subset of REAL ;
func divs A -> set means :Def3: :: INTEGRA1:def 3
for x1 being set holds
( x1 in it iff x1 is DivisionPoint of A );
existence
ex b1 being set st
for x1 being set holds
( x1 in b1 iff x1 is DivisionPoint of A )
proof end;
uniqueness
for b1, b2 being set st ( for x1 being set holds
( x1 in b1 iff x1 is DivisionPoint of A ) ) & ( for x1 being set holds
( x1 in b2 iff x1 is DivisionPoint of A ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines divs INTEGRA1:def 3 :
for A being non empty compact Subset of REAL
for b2 being set holds
( b2 = divs A iff for x1 being set holds
( x1 in b2 iff x1 is DivisionPoint of A ) );

registration
let A be non empty compact Subset of REAL ;
cluster divs A -> non empty ;
coherence
not divs A is empty
proof end;
end;

definition
let A be non empty compact Subset of REAL ;
mode Division of A -> non empty set means :Def4: :: INTEGRA1:def 4
for x1 being set holds
( x1 in it iff x1 is DivisionPoint of A );
existence
ex b1 being non empty set st
for x1 being set holds
( x1 in b1 iff x1 is DivisionPoint of A )
proof end;
end;

:: deftheorem Def4 defines Division INTEGRA1:def 4 :
for A being non empty compact Subset of REAL
for b2 being non empty set holds
( b2 is Division of A iff for x1 being set holds
( x1 in b2 iff x1 is DivisionPoint of A ) );

registration
let A be non empty compact Subset of REAL ;
cluster non empty Division of A;
existence
not for b1 being Division of A holds b1 is empty
proof end;
end;

definition
let A be non empty compact Subset of REAL ;
let S be non empty Division of A;
:: original: Element
redefine mode Element of S -> DivisionPoint of A;
coherence
for b1 being Element of S holds b1 is DivisionPoint of A
by Def4;
end;

theorem :: INTEGRA1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: INTEGRA1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in dom D holds
D . i in A
proof end;

theorem Th9: :: INTEGRA1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in dom D & i <> 1 holds
( i - 1 in dom D & D . (i - 1) in A & i - 1 in NAT )
proof end;

definition
let A be closed-interval Subset of REAL ;
let S be non empty Division of A;
let D be Element of S;
let i be Nat;
assume A1: i in dom D ;
func divset D,i -> closed-interval Subset of REAL means :Def5: :: INTEGRA1:def 5
( inf it = inf A & sup it = D . i ) if i = 1
otherwise ( inf it = D . (i - 1) & sup it = D . i );
existence
( ( i = 1 implies ex b1 being closed-interval Subset of REAL st
( inf b1 = inf A & sup b1 = D . i ) ) & ( not i = 1 implies ex b1 being closed-interval Subset of REAL st
( inf b1 = D . (i - 1) & sup b1 = D . i ) ) )
proof end;
uniqueness
for b1, b2 being closed-interval Subset of REAL holds
( ( i = 1 & inf b1 = inf A & sup b1 = D . i & inf b2 = inf A & sup b2 = D . i implies b1 = b2 ) & ( not i = 1 & inf b1 = D . (i - 1) & sup b1 = D . i & inf b2 = D . (i - 1) & sup b2 = D . i implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being closed-interval Subset of REAL holds verum
;
;
end;

:: deftheorem Def5 defines divset INTEGRA1:def 5 :
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S
for i being Nat st i in dom D holds
for b5 being closed-interval Subset of REAL holds
( ( i = 1 implies ( b5 = divset D,i iff ( inf b5 = inf A & sup b5 = D . i ) ) ) & ( not i = 1 implies ( b5 = divset D,i iff ( inf b5 = D . (i - 1) & sup b5 = D . i ) ) ) );

theorem Th10: :: INTEGRA1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in dom D holds
divset D,i c= A
proof end;

definition
let A be Subset of REAL ;
func vol A -> Real equals :: INTEGRA1:def 6
(sup A) - (inf A);
correctness
coherence
(sup A) - (inf A) is Real
;
;
end;

:: deftheorem defines vol INTEGRA1:def 6 :
for A being Subset of REAL holds vol A = (sup A) - (inf A);

theorem Th11: :: INTEGRA1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty bounded Subset of REAL holds 0 <= vol A
proof end;

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
let S be non empty Division of A;
let D be Element of S;
func upper_volume f,D -> FinSequence of REAL means :Def7: :: INTEGRA1:def 7
( len it = len D & ( for i being Nat st i in Seg (len D) holds
it . i = (sup (rng (f | (divset D,i)))) * (vol (divset D,i)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in Seg (len D) holds
b1 . i = (sup (rng (f | (divset D,i)))) * (vol (divset D,i)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in Seg (len D) holds
b1 . i = (sup (rng (f | (divset D,i)))) * (vol (divset D,i)) ) & len b2 = len D & ( for i being Nat st i in Seg (len D) holds
b2 . i = (sup (rng (f | (divset D,i)))) * (vol (divset D,i)) ) holds
b1 = b2
proof end;
func lower_volume f,D -> FinSequence of REAL means :Def8: :: INTEGRA1:def 8
( len it = len D & ( for i being Nat st i in Seg (len D) holds
it . i = (inf (rng (f | (divset D,i)))) * (vol (divset D,i)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in Seg (len D) holds
b1 . i = (inf (rng (f | (divset D,i)))) * (vol (divset D,i)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in Seg (len D) holds
b1 . i = (inf (rng (f | (divset D,i)))) * (vol (divset D,i)) ) & len b2 = len D & ( for i being Nat st i in Seg (len D) holds
b2 . i = (inf (rng (f | (divset D,i)))) * (vol (divset D,i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines upper_volume INTEGRA1:def 7 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for S being non empty Division of A
for D being Element of S
for b5 being FinSequence of REAL holds
( b5 = upper_volume f,D iff ( len b5 = len D & ( for i being Nat st i in Seg (len D) holds
b5 . i = (sup (rng (f | (divset D,i)))) * (vol (divset D,i)) ) ) );

:: deftheorem Def8 defines lower_volume INTEGRA1:def 8 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for S being non empty Division of A
for D being Element of S
for b5 being FinSequence of REAL holds
( b5 = lower_volume f,D iff ( len b5 = len D & ( for i being Nat st i in Seg (len D) holds
b5 . i = (inf (rng (f | (divset D,i)))) * (vol (divset D,i)) ) ) );

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
let S be non empty Division of A;
let D be Element of S;
func upper_sum f,D -> Real equals :: INTEGRA1:def 9
Sum (upper_volume f,D);
correctness
coherence
Sum (upper_volume f,D) is Real
;
;
func lower_sum f,D -> Real equals :: INTEGRA1:def 10
Sum (lower_volume f,D);
correctness
coherence
Sum (lower_volume f,D) is Real
;
;
end;

:: deftheorem defines upper_sum INTEGRA1:def 9 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for S being non empty Division of A
for D being Element of S holds upper_sum f,D = Sum (upper_volume f,D);

:: deftheorem defines lower_sum INTEGRA1:def 10 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for S being non empty Division of A
for D being Element of S holds lower_sum f,D = Sum (lower_volume f,D);

definition
let A be closed-interval Subset of REAL ;
:: original: divs
redefine func divs A -> Division of A;
coherence
divs A is Division of A
proof end;
end;

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
func upper_sum_set f -> PartFunc of divs A, REAL means :Def11: :: INTEGRA1:def 11
( dom it = divs A & ( for D being Element of divs A st D in dom it holds
it . D = upper_sum f,D ) );
existence
ex b1 being PartFunc of divs A, REAL st
( dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = upper_sum f,D ) )
proof end;
uniqueness
for b1, b2 being PartFunc of divs A, REAL st dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = upper_sum f,D ) & dom b2 = divs A & ( for D being Element of divs A st D in dom b2 holds
b2 . D = upper_sum f,D ) holds
b1 = b2
proof end;
func lower_sum_set f -> PartFunc of divs A, REAL means :Def12: :: INTEGRA1:def 12
( dom it = divs A & ( for D being Element of divs A st D in dom it holds
it . D = lower_sum f,D ) );
existence
ex b1 being PartFunc of divs A, REAL st
( dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = lower_sum f,D ) )
proof end;
uniqueness
for b1, b2 being PartFunc of divs A, REAL st dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = lower_sum f,D ) & dom b2 = divs A & ( for D being Element of divs A st D in dom b2 holds
b2 . D = lower_sum f,D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines upper_sum_set INTEGRA1:def 11 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for b3 being PartFunc of divs A, REAL holds
( b3 = upper_sum_set f iff ( dom b3 = divs A & ( for D being Element of divs A st D in dom b3 holds
b3 . D = upper_sum f,D ) ) );

:: deftheorem Def12 defines lower_sum_set INTEGRA1:def 12 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for b3 being PartFunc of divs A, REAL holds
( b3 = lower_sum_set f iff ( dom b3 = divs A & ( for D being Element of divs A st D in dom b3 holds
b3 . D = lower_sum f,D ) ) );

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
pred f is_upper_integrable_on A means :Def13: :: INTEGRA1:def 13
rng (upper_sum_set f) is bounded_below;
pred f is_lower_integrable_on A means :Def14: :: INTEGRA1:def 14
rng (lower_sum_set f) is bounded_above;
end;

:: deftheorem Def13 defines is_upper_integrable_on INTEGRA1:def 13 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL holds
( f is_upper_integrable_on A iff rng (upper_sum_set f) is bounded_below );

:: deftheorem Def14 defines is_lower_integrable_on INTEGRA1:def 14 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL holds
( f is_lower_integrable_on A iff rng (lower_sum_set f) is bounded_above );

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
func upper_integral f -> Real equals :: INTEGRA1:def 15
inf (rng (upper_sum_set f));
correctness
coherence
inf (rng (upper_sum_set f)) is Real
;
;
end;

:: deftheorem defines upper_integral INTEGRA1:def 15 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL holds upper_integral f = inf (rng (upper_sum_set f));

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
func lower_integral f -> Real equals :: INTEGRA1:def 16
sup (rng (lower_sum_set f));
correctness
coherence
sup (rng (lower_sum_set f)) is Real
;
;
end;

:: deftheorem defines lower_integral INTEGRA1:def 16 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL holds lower_integral f = sup (rng (lower_sum_set f));

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
pred f is_integrable_on A means :Def17: :: INTEGRA1:def 17
( f is_upper_integrable_on A & f is_lower_integrable_on A & upper_integral f = lower_integral f );
end;

:: deftheorem Def17 defines is_integrable_on INTEGRA1:def 17 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL holds
( f is_integrable_on A iff ( f is_upper_integrable_on A & f is_lower_integrable_on A & upper_integral f = lower_integral f ) );

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
func integral f -> Real equals :: INTEGRA1:def 18
upper_integral f;
correctness
coherence
upper_integral f is Real
;
;
end;

:: deftheorem defines integral INTEGRA1:def 18 :
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL holds integral f = upper_integral f;

theorem Th12: :: INTEGRA1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f, g being PartFunc of X, REAL holds rng (f + g) c= (rng f) + (rng g)
proof end;

theorem Th13: :: INTEGRA1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being PartFunc of X, REAL st f is_bounded_below_on X holds
rng f is bounded_below
proof end;

theorem :: INTEGRA1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being PartFunc of X, REAL st rng f is bounded_below holds
f is_bounded_below_on X
proof end;

theorem Th15: :: INTEGRA1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being PartFunc of X, REAL st f is_bounded_above_on X holds
rng f is bounded_above
proof end;

theorem :: INTEGRA1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being PartFunc of X, REAL st rng f is bounded_above holds
f is_bounded_above_on X
proof end;

theorem :: INTEGRA1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being PartFunc of X, REAL st f is_bounded_on X holds
rng f is bounded
proof end;

theorem Th18: :: INTEGRA1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds chi A,A is_constant_on A
proof end;

theorem Th19: :: INTEGRA1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being non empty Subset of X holds rng (chi A,A) = {1}
proof end;

theorem Th20: :: INTEGRA1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being non empty Subset of X
for B being set st B meets dom (chi A,A) holds
rng ((chi A,A) | B) = {1}
proof end;

theorem Th21: :: INTEGRA1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in Seg (len D) holds
vol (divset D,i) = (lower_volume (chi A,A),D) . i
proof end;

theorem Th22: :: INTEGRA1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in Seg (len D) holds
vol (divset D,i) = (upper_volume (chi A,A),D) . i
proof end;

theorem :: INTEGRA1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being FinSequence of REAL st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
proof end;

theorem Th24: :: INTEGRA1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being FinSequence of REAL st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
proof end;

theorem Th25: :: INTEGRA1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S holds Sum (lower_volume (chi A,A),D) = vol A
proof end;

theorem Th26: :: INTEGRA1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S holds Sum (upper_volume (chi A,A),D) = vol A
proof end;

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
let S be non empty Division of A;
let D be Element of S;
:: original: upper_volume
redefine func upper_volume f,D -> non empty FinSequence of REAL ;
coherence
upper_volume f,D is non empty FinSequence of REAL
proof end;
end;

definition
let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
let S be non empty Division of A;
let D be Element of S;
:: original: lower_volume
redefine func lower_volume f,D -> non empty FinSequence of REAL ;
coherence
lower_volume f,D is non empty FinSequence of REAL
proof end;
end;

theorem Th27: :: INTEGRA1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_below_on A holds
(inf (rng f)) * (vol A) <= lower_sum f,D
proof end;

theorem :: INTEGRA1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S
for i being Nat st f is_bounded_above_on A & i in Seg (len D) holds
(sup (rng f)) * (vol (divset D,i)) >= (sup (rng (f | (divset D,i)))) * (vol (divset D,i))
proof end;

theorem Th29: :: INTEGRA1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_above_on A holds
upper_sum f,D <= (sup (rng f)) * (vol A)
proof end;

theorem Th30: :: INTEGRA1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_on A holds
lower_sum f,D <= upper_sum f,D
proof end;

definition
let x be non empty FinSequence of REAL ;
:: original: rng
redefine func rng x -> non empty finite Subset of REAL ;
coherence
rng x is non empty finite Subset of REAL
proof end;
end;

definition
let A be closed-interval Subset of REAL ;
let D be Element of divs A;
func delta D -> Real equals :: INTEGRA1:def 19
max (rng (upper_volume (chi A,A),D));
correctness
coherence
max (rng (upper_volume (chi A,A),D)) is Real
;
by XREAL_0:def 1;
end;

:: deftheorem defines delta INTEGRA1:def 19 :
for A being closed-interval Subset of REAL
for D being Element of divs A holds delta D = max (rng (upper_volume (chi A,A),D));

definition
let A be closed-interval Subset of REAL ;
let S be non empty Division of A;
let D1, D2 be Element of S;
pred D1 <= D2 means :Def20: :: INTEGRA1:def 20
( len D1 <= len D2 & rng D1 c= rng D2 );
end;

:: deftheorem Def20 defines <= INTEGRA1:def 20 :
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D1, D2 being Element of S holds
( D1 <= D2 iff ( len D1 <= len D2 & rng D1 c= rng D2 ) );

notation
let A be closed-interval Subset of REAL ;
let S be non empty Division of A;
let D1, D2 be Element of S;
synonym D2 >= D1 for D1 <= D2;
end;

theorem Th31: :: INTEGRA1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D1, D2 being Element of S st len D1 = 1 holds
D1 <= D2
proof end;

theorem Th32: :: INTEGRA1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st f is_bounded_above_on A & len D1 = 1 holds
upper_sum f,D1 >= upper_sum f,D2
proof end;

theorem Th33: :: INTEGRA1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st f is_bounded_below_on A & len D1 = 1 holds
lower_sum f,D1 <= lower_sum f,D2
proof end;

theorem :: INTEGRA1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in dom D holds
ex A1, A2 being closed-interval Subset of REAL st
( A1 = [.(inf A),(D . i).] & A2 = [.(D . i),(sup A).] & A = A1 \/ A2 )
proof end;

theorem Th35: :: INTEGRA1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D1, D2 being Element of S st i in dom D1 & D1 <= D2 holds
ex j being Nat st
( j in dom D2 & D1 . i = D2 . j )
proof end;

definition
let A be closed-interval Subset of REAL ;
let S be non empty Division of A;
let D1, D2 be Element of S;
let i be Nat;
assume A1: D1 <= D2 ;
func indx D2,D1,i -> Nat means :Def21: :: INTEGRA1:def 21
( it in dom D2 & D1 . i = D2 . it ) if i in dom D1
otherwise it = 0;
existence
( ( i in dom D1 implies ex b1 being Nat st
( b1 in dom D2 & D1 . i = D2 . b1 ) ) & ( not i in dom D1 implies ex b1 being Nat st b1 = 0 ) )
by A1, Th35;
uniqueness
for b1, b2 being Nat holds
( ( i in dom D1 & b1 in dom D2 & D1 . i = D2 . b1 & b2 in dom D2 & D1 . i = D2 . b2 implies b1 = b2 ) & ( not i in dom D1 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def21 defines indx INTEGRA1:def 21 :
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D1, D2 being Element of S
for i being Nat st D1 <= D2 holds
for b6 being Nat holds
( ( i in dom D1 implies ( b6 = indx D2,D1,i iff ( b6 in dom D2 & D1 . i = D2 . b6 ) ) ) & ( not i in dom D1 implies ( b6 = indx D2,D1,i iff b6 = 0 ) ) );

theorem Th36: :: INTEGRA1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being increasing FinSequence of REAL
for n being Nat st n <= len p holds
p /^ n is increasing FinSequence of REAL
proof end;

theorem Th37: :: INTEGRA1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being increasing FinSequence of REAL
for i, j being Nat st j in dom p & i <= j holds
mid p,i,j is increasing FinSequence of REAL
proof end;

theorem Th38: :: INTEGRA1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S
for i, j being Nat st i in dom D & j in dom D & i <= j holds
ex B being closed-interval Subset of REAL st
( inf B = (mid D,i,j) . 1 & sup B = (mid D,i,j) . (len (mid D,i,j)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is DivisionPoint of B )
proof end;

theorem Th39: :: INTEGRA1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being closed-interval Subset of REAL
for S being non empty Division of A
for S1 being non empty Division of B
for D being Element of S
for i, j being Nat st i in dom D & j in dom D & i <= j & D . i >= inf B & D . j = sup B holds
mid D,i,j is Element of S1
proof end;

definition
let p be FinSequence of REAL ;
func PartSums p -> FinSequence of REAL means :Def22: :: INTEGRA1:def 22
( len it = len p & ( for i being Nat st i in Seg (len p) holds
it . i = Sum (p | i) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len p & ( for i being Nat st i in Seg (len p) holds
b1 . i = Sum (p | i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len p & ( for i being Nat st i in Seg (len p) holds
b1 . i = Sum (p | i) ) & len b2 = len p & ( for i being Nat st i in Seg (len p) holds
b2 . i = Sum (p | i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines PartSums INTEGRA1:def 22 :
for p, b2 being FinSequence of REAL holds
( b2 = PartSums p iff ( len b2 = len p & ( for i being Nat st i in Seg (len p) holds
b2 . i = Sum (p | i) ) ) );

theorem Th40: :: INTEGRA1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 & f is_bounded_above_on A holds
for i being non empty Nat st i in dom D1 holds
Sum ((upper_volume f,D1) | i) >= Sum ((upper_volume f,D2) | (indx D2,D1,i))
proof end;

theorem Th41: :: INTEGRA1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 & f is_bounded_below_on A holds
for i being non empty Nat st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i))
proof end;

theorem Th42: :: INTEGRA1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S
for i being Nat st D1 <= D2 & i in dom D1 & f is_bounded_above_on A holds
(PartSums (upper_volume f,D1)) . i >= (PartSums (upper_volume f,D2)) . (indx D2,D1,i)
proof end;

theorem Th43: :: INTEGRA1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S
for i being Nat st D1 <= D2 & i in dom D1 & f is_bounded_below_on A holds
(PartSums (lower_volume f,D1)) . i <= (PartSums (lower_volume f,D2)) . (indx D2,D1,i)
proof end;

theorem Th44: :: INTEGRA1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for S being non empty Division of A
for D being Element of S holds (PartSums (upper_volume f,D)) . (len D) = upper_sum f,D
proof end;

theorem Th45: :: INTEGRA1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for S being non empty Division of A
for D being Element of S holds (PartSums (lower_volume f,D)) . (len D) = lower_sum f,D
proof end;

theorem Th46: :: INTEGRA1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 holds
indx D2,D1,(len D1) = len D2
proof end;

theorem Th47: :: INTEGRA1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 & f is_bounded_above_on A holds
upper_sum f,D2 <= upper_sum f,D1
proof end;

theorem Th48: :: INTEGRA1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 & f is_bounded_below_on A holds
lower_sum f,D2 >= lower_sum f,D1
proof end;

theorem Th49: :: INTEGRA1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for S being non empty Division of A
for D1, D2 being Element of S ex D being Element of S st
( D1 <= D & D2 <= D )
proof end;

theorem Th50: :: INTEGRA1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st f is_bounded_on A holds
lower_sum f,D1 <= upper_sum f,D2
proof end;

theorem Th51: :: INTEGRA1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A holds
upper_integral f >= lower_integral f
proof end;

theorem Th52: :: INTEGRA1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being Subset of REAL holds (- X) + (- Y) = - (X + Y)
proof end;

theorem Th53: :: INTEGRA1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being Subset of REAL st X is bounded_above & Y is bounded_above holds
X + Y is bounded_above
proof end;

theorem Th54: :: INTEGRA1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty Subset of REAL st X is bounded_above & Y is bounded_above holds
sup (X + Y) = (sup X) + (sup Y)
proof end;

theorem Th55: :: INTEGRA1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for f, g being Function of A, REAL
for S being non empty Division of A
for D being Element of S st i in Seg (len D) & f is_bounded_above_on A & g is_bounded_above_on A holds
(upper_volume (f + g),D) . i <= ((upper_volume f,D) . i) + ((upper_volume g,D) . i)
proof end;

theorem Th56: :: INTEGRA1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for A being closed-interval Subset of REAL
for f, g being Function of A, REAL
for S being non empty Division of A
for D being Element of S st i in Seg (len D) & f is_bounded_below_on A & g is_bounded_below_on A holds
((lower_volume f,D) . i) + ((lower_volume g,D) . i) <= (lower_volume (f + g),D) . i
proof end;

theorem Th57: :: INTEGRA1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f, g being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_above_on A & g is_bounded_above_on A holds
upper_sum (f + g),D <= (upper_sum f,D) + (upper_sum g,D)
proof end;

theorem Th58: :: INTEGRA1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f, g being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_below_on A & g is_bounded_below_on A holds
(lower_sum f,D) + (lower_sum g,D) <= lower_sum (f + g),D
proof end;

theorem :: INTEGRA1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed-interval Subset of REAL
for f, g being Function of A, REAL st f is_bounded_on A & g is_bounded_on A & f is_integrable_on A & g is_integrable_on A holds
( f + g is_integrable_on A & integral (f + g) = (integral f) + (integral g) )
proof end;