Metamath Proof Explorer


Theorem itgeq12dv

Description: Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017)

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

Proof

Step Hyp Ref Expression
1 itgeq12dv.2 ( 𝜑𝐴 = 𝐵 )
2 itgeq12dv.1 ( ( 𝜑𝑥𝐴 ) → 𝐶 = 𝐷 )
3 2 fvoveq1d ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
4 3 breq2d ( ( 𝜑𝑥𝐴 ) → ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) )
5 4 pm5.32da ( 𝜑 → ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ) )
6 1 eleq2d ( 𝜑 → ( 𝑥𝐴𝑥𝐵 ) )
7 6 anbi1d ( 𝜑 → ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ) )
8 5 7 bitrd ( 𝜑 → ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ) )
9 3 adantrr ( ( 𝜑 ∧ ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
10 eqidd ( ( 𝜑 ∧ ¬ ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ) → 0 = 0 )
11 8 9 10 ifbieq12d2 ( 𝜑 → if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
12 11 mpteq2dv ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
13 12 fveq2d ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
14 13 oveq2d ( 𝜑 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
15 14 sumeq2sdv ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
16 eqid ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
17 16 dfitg 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
18 eqid ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) )
19 18 dfitg 𝐵 𝐷 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
20 15 17 19 3eqtr4g ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )