Theorem itgeq1f

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

	Ref	Expression
Hypotheses	itgeq1f.1	⊢ Ⅎ 𝑥 𝐴
	itgeq1f.2	⊢ Ⅎ 𝑥 𝐵
Assertion	itgeq1f	⊢ ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgeq1f.1	⊢ Ⅎ 𝑥 𝐴
2		itgeq1f.2	⊢ Ⅎ 𝑥 𝐵
3		eqid	⊢ ℝ = ℝ
4	1 2	nfeq	⊢ Ⅎ 𝑥 𝐴 = 𝐵
5		eleq2	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
6	5	anbi1d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ) )
7	6	ifbid	⊢ ( 𝐴 = 𝐵 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
8	7	a1d	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ ℝ → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
9	4 8	ralrimi	⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
10		mpteq12	⊢ ( ( ℝ = ℝ ∧ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
11	3 9 10	sylancr	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
12	11	fveq2d	⊢ ( 𝐴 = 𝐵 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
13	12	oveq2d	⊢ ( 𝐴 = 𝐵 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
14	13	sumeq2sdv	⊢ ( 𝐴 = 𝐵 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
15		eqid	⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
16	15	dfitg	⊢ ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
17	15	dfitg	⊢ ∫ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
18	14 16 17	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )