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 𝑥 ) |