:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received December 7, 1999

:: Copyright (c) 1999-2017 Association of Mizar Users

theorem :: INTEGRA2:1

for A being non empty closed_interval Subset of REAL

for x being Real holds

( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )

for x being Real holds

( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )

proof end;

LM: for p being FinSequence of REAL st ( for n being Nat st n in dom p & n + 1 in dom p holds

p . n <= p . (n + 1) ) holds

for i, j being Nat st i in dom p & j in dom p & i <= j holds

p . i <= p . j

proof end;

definition

let IT be FinSequence of REAL ;

( IT is non-decreasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) )

end;
redefine attr IT is non-decreasing means :Def1: :: INTEGRA2:def 1

for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1);

compatibility for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1);

( IT is non-decreasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) )

proof end;

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

for IT being FinSequence of REAL holds

( IT is non-decreasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) );

for IT being FinSequence of REAL holds

( IT is non-decreasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) );

registration

ex b_{1} being FinSequence of REAL st b_{1} is non-decreasing
end;

cluster Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued non-decreasing V56() FinSequence-like FinSubsequence-like for FinSequence of REAL ;

existence ex b

proof end;

theorem :: INTEGRA2:2

for p being non-decreasing FinSequence of REAL

for i, j being Nat st i in dom p & j in dom p & i <= j holds

p . i <= p . j

for i, j being Nat st i in dom p & j in dom p & i <= j holds

p . i <= p . j

proof end;

theorem :: INTEGRA2:3

for p being FinSequence of REAL ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent

proof end;

theorem :: INTEGRA2:4

for D being non empty set

for f being FinSequence of D

for k1, k2, k3 being Nat st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds

(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)

for f being FinSequence of D

for k1, k2, k3 being Nat st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds

(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)

proof end;

definition

let A be real-membered set ;

let x be Real;

:: original: **

redefine func x ** A -> Subset of REAL;

coherence

x ** A is Subset of REAL by MEMBERED:3;

end;
let x be Real;

:: original: **

redefine func x ** A -> Subset of REAL;

coherence

x ** A is Subset of REAL by MEMBERED:3;

theorem :: INTEGRA2:5

for X, Y being non empty set

for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds

(f | Y) | Y is bounded_above

for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds

(f | Y) | Y is bounded_above

proof end;

theorem :: INTEGRA2:6

for X, Y being non empty set

for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds

(f | Y) | Y is bounded_below

for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds

(f | Y) | Y is bounded_below

proof end;

theorem :: INTEGRA2:7

theorem :: INTEGRA2:9

for r being Real

for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds

r ** X is bounded_above

for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds

r ** X is bounded_above

proof end;

theorem :: INTEGRA2:10

for r being Real

for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds

r ** X is bounded_below

for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds

r ** X is bounded_below

proof end;

theorem :: INTEGRA2:11

for r being Real

for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds

r ** X is bounded_below

for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds

r ** X is bounded_below

proof end;

theorem :: INTEGRA2:12

for r being Real

for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds

r ** X is bounded_above

for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds

r ** X is bounded_above

proof end;

theorem Th13: :: INTEGRA2:13

for r being Real

for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds

upper_bound (r ** X) = r * (upper_bound X)

for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds

upper_bound (r ** X) = r * (upper_bound X)

proof end;

theorem Th14: :: INTEGRA2:14

for r being Real

for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds

lower_bound (r ** X) = r * (upper_bound X)

for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds

lower_bound (r ** X) = r * (upper_bound X)

proof end;

theorem Th15: :: INTEGRA2:15

for r being Real

for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds

lower_bound (r ** X) = r * (lower_bound X)

for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds

lower_bound (r ** X) = r * (lower_bound X)

proof end;

theorem Th16: :: INTEGRA2:16

for r being Real

for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds

upper_bound (r ** X) = r * (lower_bound X)

for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds

upper_bound (r ** X) = r * (lower_bound X)

proof end;

theorem Th17: :: INTEGRA2:17

for r being Real

for X being non empty set

for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)

for X being non empty set

for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)

proof end;

theorem Th18: :: INTEGRA2:18

for r being Real

for X, Z being non empty set

for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))

for X, Z being non empty set

for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))

proof end;

theorem Th19: :: INTEGRA2:19

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r >= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)

proof end;

theorem Th20: :: INTEGRA2:20

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r <= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r <= 0 holds

(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)

proof end;

theorem Th21: :: INTEGRA2:21

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r >= 0 holds

(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r >= 0 holds

(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)

proof end;

theorem Th22: :: INTEGRA2:22

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r <= 0 holds

(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded & r <= 0 holds

(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)

proof end;

theorem Th23: :: INTEGRA2:23

for r being Real

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)

proof end;

theorem Th24: :: INTEGRA2:24

for r being Real

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds

(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds

(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)

proof end;

theorem Th25: :: INTEGRA2:25

for r being Real

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds

(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds

(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

proof end;

theorem Th26: :: INTEGRA2:26

for r being Real

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

for i being Nat

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

proof end;

theorem Th27: :: INTEGRA2:27

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_above & r >= 0 holds

upper_sum ((r (#) f),D) = r * (upper_sum (f,D))

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_above & r >= 0 holds

upper_sum ((r (#) f),D) = r * (upper_sum (f,D))

proof end;

theorem Th28: :: INTEGRA2:28

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_above & r <= 0 holds

lower_sum ((r (#) f),D) = r * (upper_sum (f,D))

proof end;

theorem Th29: :: INTEGRA2:29

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_below & r >= 0 holds

lower_sum ((r (#) f),D) = r * (lower_sum (f,D))

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_below & r >= 0 holds

lower_sum ((r (#) f),D) = r * (lower_sum (f,D))

proof end;

theorem Th30: :: INTEGRA2:30

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_below & r <= 0 holds

upper_sum ((r (#) f),D) = r * (lower_sum (f,D))

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A st f | A is bounded_below & r <= 0 holds

upper_sum ((r (#) f),D) = r * (lower_sum (f,D))

proof end;

theorem Th31: :: INTEGRA2:31

for r being Real

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded & f is integrable holds

( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded & f is integrable holds

( r (#) f is integrable & integral (r (#) f) = r * (integral f) )

proof end;

theorem Th32: :: INTEGRA2:32

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds

f . x >= 0 ) holds

integral f >= 0

for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds

f . x >= 0 ) holds

integral f >= 0

proof end;

theorem Th33: :: INTEGRA2:33

for A being non empty closed_interval Subset of REAL

for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds

( f - g is integrable & integral (f - g) = (integral f) - (integral g) )

for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds

( f - g is integrable & integral (f - g) = (integral f) - (integral g) )

proof end;

theorem :: INTEGRA2:34

for A being non empty closed_interval Subset of REAL

for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds

f . x >= g . x ) holds

integral f >= integral g

for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds

f . x >= g . x ) holds

integral f >= integral g

proof end;

theorem :: INTEGRA2:35

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded holds

rng (upper_sum_set f) is bounded_below

for f being Function of A,REAL st f | A is bounded holds

rng (upper_sum_set f) is bounded_below

proof end;

theorem :: INTEGRA2:36

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f | A is bounded holds

rng (lower_sum_set f) is bounded_above

for f being Function of A,REAL st f | A is bounded holds

rng (lower_sum_set f) is bounded_above

proof end;

definition
end;

definition

let A be non empty closed_interval Subset of REAL;

let T be DivSequence of A;

let i be Nat;

:: original: .

redefine func T . i -> Division of A;

coherence

T . i is Division of A

end;
let T be DivSequence of A;

let i be Nat;

:: original: .

redefine func T . i -> Division of A;

coherence

T . i is Division of A

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let f be PartFunc of A,REAL;

let T be DivSequence of A;

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = upper_sum (f,(T . i))

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = upper_sum (f,(T . i)) ) & ( for i being Nat holds b_{2} . i = upper_sum (f,(T . i)) ) holds

b_{1} = b_{2}

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = lower_sum (f,(T . i))

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = lower_sum (f,(T . i)) ) & ( for i being Nat holds b_{2} . i = lower_sum (f,(T . i)) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of A,REAL;

let T be DivSequence of A;

func upper_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 2

for i being Nat holds it . i = upper_sum (f,(T . i));

existence for i being Nat holds it . i = upper_sum (f,(T . i));

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

func lower_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 3

for i being Nat holds it . i = lower_sum (f,(T . i));

existence for i being Nat holds it . i = lower_sum (f,(T . i));

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines upper_sum INTEGRA2:def 2 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for T being DivSequence of A

for b_{4} being Real_Sequence holds

( b_{4} = upper_sum (f,T) iff for i being Nat holds b_{4} . i = upper_sum (f,(T . i)) );

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for T being DivSequence of A

for b

( b

:: deftheorem defines lower_sum INTEGRA2:def 3 :

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for T being DivSequence of A

for b_{4} being Real_Sequence holds

( b_{4} = lower_sum (f,T) iff for i being Nat holds b_{4} . i = lower_sum (f,(T . i)) );

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for T being DivSequence of A

for b

( b

theorem :: INTEGRA2:37

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st D1 <= D2 holds

for j being Nat st j in dom D2 holds

ex i being Nat st

( i in dom D1 & divset (D2,j) c= divset (D1,i) )

for D1, D2 being Division of A st D1 <= D2 holds

for j being Nat st j in dom D2 holds

ex i being Nat st

( i in dom D1 & divset (D2,j) c= divset (D1,i) )

proof end;

theorem :: INTEGRA2:39

for A being Subset of REAL

for a, x being Real st x in a ** A holds

ex b being Real st

( b in A & x = a * b )

for a, x being Real st x in a ** A holds

ex b being Real st

( b in A & x = a * b )

proof end;

:: missing, 2008.06.10