Metamath Proof Explorer


Theorem itgposval

Description: The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblrelem.1 φ x A B
itgreval.2 φ x A B 𝐿 1
itgposval.3 φ x A 0 B
Assertion itgposval φ A B dx = 2 x if x A B 0

Proof

Step Hyp Ref Expression
1 iblrelem.1 φ x A B
2 itgreval.2 φ x A B 𝐿 1
3 itgposval.3 φ x A 0 B
4 1 2 itgrevallem1 φ A B dx = 2 x if x A 0 B B 0 2 x if x A 0 B B 0
5 3 ex φ x A 0 B
6 5 pm4.71rd φ x A 0 B x A
7 ancom 0 B x A x A 0 B
8 6 7 syl6rbb φ x A 0 B x A
9 8 ifbid φ if x A 0 B B 0 = if x A B 0
10 9 mpteq2dv φ x if x A 0 B B 0 = x if x A B 0
11 10 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A B 0
12 1 3 iblposlem φ 2 x if x A 0 B B 0 = 0
13 11 12 oveq12d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = 2 x if x A B 0 0
14 1 3 iblpos φ x A B 𝐿 1 x A B MblFn 2 x if x A B 0
15 2 14 mpbid φ x A B MblFn 2 x if x A B 0
16 15 simprd φ 2 x if x A B 0
17 16 recnd φ 2 x if x A B 0
18 17 subid1d φ 2 x if x A B 0 0 = 2 x if x A B 0
19 4 13 18 3eqtrd φ A B dx = 2 x if x A B 0