Metamath Proof Explorer

Theorem itgeq12sdv

Description: Equality theorem for an integral. Deduction form. General version of itgeq1d and itgeq2sdv . (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypotheses itgeq12sdv.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
itgeq12sdv.2 ⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion itgeq12sdv ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgeq12sdv.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
2 itgeq12sdv.2 ⊢ ( 𝜑 → 𝐶 = 𝐷 )
3 2 oveq1d ⊢ ( 𝜑 → ( 𝐶 / ( i ↑ 𝑘 ) ) = ( 𝐷 / ( i ↑ 𝑘 ) ) )
4 3 fveq2d ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
5 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
6 5 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) ) )
7 6 ifbid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
8 4 7 csbeq12dv ⊢ ( 𝜑 → ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
9 8 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) )
10 9 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
11 10 oveq2d ⊢ ( 𝜑 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) )
12 11 sumeq2sdv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 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 3eqtr4g ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )