Metamath Proof Explorer


Theorem itgvallem3

Description: Lemma for itgposval and itgreval . (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis itgvallem3.1 φ x A B = 0
Assertion itgvallem3 φ 2 x if x A 0 B B 0 = 0

Proof

Step Hyp Ref Expression
1 itgvallem3.1 φ x A B = 0
2 1 adantrr φ x A 0 B B = 0
3 2 ifeq1da φ if x A 0 B B 0 = if x A 0 B 0 0
4 ifid if x A 0 B 0 0 = 0
5 3 4 syl6eq φ if x A 0 B B 0 = 0
6 5 mpteq2dv φ x if x A 0 B B 0 = x 0
7 fconstmpt × 0 = x 0
8 6 7 syl6eqr φ x if x A 0 B B 0 = × 0
9 8 fveq2d φ 2 x if x A 0 B B 0 = 2 × 0
10 itg20 2 × 0 = 0
11 9 10 syl6eq φ 2 x if x A 0 B B 0 = 0