Metamath Proof Explorer


Theorem itgrevallem1

Description: Lemma for itgposval and itgreval . (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
Assertion itgrevallem1 φ A B dx = 2 x if x A 0 B B 0 2 x if x A 0 B B 0

Proof

Step Hyp Ref Expression
1 iblrelem.1 φ x A B
2 itgreval.2 φ x A B 𝐿 1
3 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
4 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
5 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
6 eqid 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
7 3 4 5 6 1 2 itgcnlem φ A B dx = 2 x if x A 0 B B 0 - 2 x if x A 0 B B 0 + i 2 x if x A 0 B B 0 2 x if x A 0 B B 0
8 1 rered φ x A B = B
9 8 ibllem φ if x A 0 B B 0 = if x A 0 B B 0
10 9 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B B 0
11 10 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
12 8 negeqd φ x A B = B
13 12 ibllem φ if x A 0 B B 0 = if x A 0 B B 0
14 13 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B B 0
15 14 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0
16 11 15 oveq12d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0 2 x if x A 0 B B 0
17 1 reim0d φ x A B = 0
18 17 itgvallem3 φ 2 x if x A 0 B B 0 = 0
19 17 negeqd φ x A B = 0
20 neg0 0 = 0
21 19 20 syl6eq φ x A B = 0
22 21 itgvallem3 φ 2 x if x A 0 B B 0 = 0
23 18 22 oveq12d φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = 0 0
24 0m0e0 0 0 = 0
25 23 24 syl6eq φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = 0
26 25 oveq2d φ i 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = i 0
27 it0e0 i 0 = 0
28 26 27 syl6eq φ i 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = 0
29 16 28 oveq12d φ 2 x if x A 0 B B 0 - 2 x if x A 0 B B 0 + i 2 x if x A 0 B B 0 2 x if x A 0 B B 0 = 2 x if x A 0 B B 0 - 2 x if x A 0 B B 0 + 0
30 1 iblrelem φ x A B 𝐿 1 x A B MblFn 2 x if x A 0 B B 0 2 x if x A 0 B B 0
31 2 30 mpbid φ x A B MblFn 2 x if x A 0 B B 0 2 x if x A 0 B B 0
32 31 simp2d φ 2 x if x A 0 B B 0
33 31 simp3d φ 2 x if x A 0 B B 0
34 32 33 resubcld φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0
35 34 recnd φ 2 x if x A 0 B B 0 2 x if x A 0 B B 0
36 35 addid1d φ 2 x if x A 0 B B 0 - 2 x if x A 0 B B 0 + 0 = 2 x if x A 0 B B 0 2 x if x A 0 B B 0
37 7 29 36 3eqtrd φ A B dx = 2 x if x A 0 B B 0 2 x if x A 0 B B 0