Metamath Proof Explorer

Theorem itgeq12i

Description: Equality inference for an integral. General version of itgeq1i and itgeq2i . (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypotheses itgeq12i.1 ⊢ 𝐴 = 𝐵
itgeq12i.2 ⊢ 𝐶 = 𝐷
Assertion itgeq12i ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥

Proof

Step Hyp Ref Expression
1 itgeq12i.1 ⊢ 𝐴 = 𝐵
2 itgeq12i.2 ⊢ 𝐶 = 𝐷
3 2 oveq1i ⊢ ( 𝐶 / ( i ↑ 𝑘 ) ) = ( 𝐷 / ( i ↑ 𝑘 ) )
4 3 fveq2i ⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) )
5 1 eleq2i ⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 )
6 5 anbi1i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) )
7 ifbi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
8 6 7 ax-mp ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
9 8 ax-gen ⊢ ∀ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
10 4 9 pm3.2i ⊢ ( ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ∧ ∀ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
11 csbeq2 ⊢ ( ∀ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) → ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
12 csbeq1 ⊢ ( ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) → ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
13 11 12 sylan9eqr ⊢ ( ( ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ∧ ∀ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) → ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
14 10 13 ax-mp ⊢ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
15 14 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
16 15 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) )
17 16 oveq2i ⊢ ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
18 17 sumeq2si ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
19 df-itg ⊢ ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
20 df-itg ⊢ ∫ 𝐵 𝐷 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
21 18 19 20 3eqtr4i ⊢ ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥