Metamath Proof Explorer


Theorem itgeq1

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgeq1 A = B A C dx = B C dx

Proof

Step Hyp Ref Expression
1 eleq2 A = B x A x B
2 1 anbi1d A = B x A 0 y x B 0 y
3 2 ifbid A = B if x A 0 y y 0 = if x B 0 y y 0
4 3 csbeq2dv A = B C i k / y if x A 0 y y 0 = C i k / y if x B 0 y y 0
5 4 mpteq2dv A = B x C i k / y if x A 0 y y 0 = x C i k / y if x B 0 y y 0
6 5 fveq2d A = B 2 x C i k / y if x A 0 y y 0 = 2 x C i k / y if x B 0 y y 0
7 6 oveq2d A = B i k 2 x C i k / y if x A 0 y y 0 = i k 2 x C i k / y if x B 0 y y 0
8 7 sumeq2sdv A = B k = 0 3 i k 2 x C i k / y if x A 0 y y 0 = k = 0 3 i k 2 x C i k / y if x B 0 y y 0
9 df-itg A C dx = k = 0 3 i k 2 x C i k / y if x A 0 y y 0
10 df-itg B C dx = k = 0 3 i k 2 x C i k / y if x B 0 y y 0
11 8 9 10 3eqtr4g A = B A C dx = B C dx