Step |
Hyp |
Ref |
Expression |
1 |
|
cbvitg.1 |
⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 ) |
2 |
1
|
fvoveq1d |
⊢ ( 𝑥 = 𝑦 → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) |
3 |
|
eleq1w |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) |
4 |
3
|
anbi1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) ) ) |
5 |
4
|
ifbid |
⊢ ( 𝑥 = 𝑦 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) = if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) |
6 |
2 5
|
csbeq12dv |
⊢ ( 𝑥 = 𝑦 → ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) = ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) |
7 |
6
|
cbvmptv |
⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) = ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) |
8 |
7
|
fveq2i |
⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) |
9 |
8
|
oveq2i |
⊢ ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) |
10 |
9
|
a1i |
⊢ ( ⊤ → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) ) |
11 |
10
|
sumeq2sdv |
⊢ ( ⊤ → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) ) |
12 |
11
|
mptru |
⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) |
13 |
|
df-itg |
⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) |
14 |
|
df-itg |
⊢ ∫ 𝐴 𝐶 d 𝑦 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) |
15 |
12 13 14
|
3eqtr4i |
⊢ ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑦 |