Metamath Proof Explorer


Theorem itgeq1

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

Ref Expression
Assertion itgeq1 ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 eleq2 ( 𝐴 = 𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
2 1 anbi1d ( 𝐴 = 𝐵 → ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) ↔ ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) ) )
3 2 ifbid ( 𝐴 = 𝐵 → if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
4 3 csbeq2dv ( 𝐴 = 𝐵 ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
5 4 mpteq2dv ( 𝐴 = 𝐵 → ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) )
6 5 fveq2d ( 𝐴 = 𝐵 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
7 6 oveq2d ( 𝐴 = 𝐵 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) )
8 7 sumeq2sdv ( 𝐴 = 𝐵 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) )
9 df-itg 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
10 df-itg 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 if ( ( 𝑥𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
11 8 9 10 3eqtr4g ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )