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