Metamath Proof Explorer


Theorem cniccibl

Description: A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion cniccibl A B F : A B cn F 𝐿 1

Proof

Step Hyp Ref Expression
1 iccmbl A B A B dom vol
2 cnmbf A B dom vol F : A B cn F MblFn
3 1 2 stoic3 A B F : A B cn F MblFn
4 simp3 A B F : A B cn F : A B cn
5 cncff F : A B cn F : A B
6 fdm F : A B dom F = A B
7 4 5 6 3syl A B F : A B cn dom F = A B
8 7 fveq2d A B F : A B cn vol dom F = vol A B
9 iccvolcl A B vol A B
10 9 3adant3 A B F : A B cn vol A B
11 8 10 eqeltrd A B F : A B cn vol dom F
12 cniccbdd A B F : A B cn x y A B F y x
13 7 raleqdv A B F : A B cn y dom F F y x y A B F y x
14 13 rexbidv A B F : A B cn x y dom F F y x x y A B F y x
15 12 14 mpbird A B F : A B cn x y dom F F y x
16 bddibl F MblFn vol dom F x y dom F F y x F 𝐿 1
17 3 11 15 16 syl3anc A B F : A B cn F 𝐿 1