Step | Hyp | Ref
| Expression |
1 | | cbvitgvw2.1 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) |
2 | 1 | fvoveq1d 7467 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (ℜ‘(𝐶 / (i↑𝑡))) = (ℜ‘(𝐷 / (i↑𝑡)))) |
3 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
4 | | cbvitgvw2.2 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) |
5 | 3, 4 | eleq12d 2832 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵)) |
6 | 5 | anbi1d 630 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣) ↔ (𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣))) |
7 | 6 | ifbid 4571 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0) = if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0)) |
8 | 2, 7 | csbeq12dv 3924 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0) = ⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0)) |
9 | 8 | cbvmptv 5282 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0)) = (𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0)) |
10 | 9 | fveq2i 6922 |
. . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦
⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0))) = (∫2‘(𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0))) |
11 | 10 | oveq2i 7456 |
. . . . 5
⊢
((i↑𝑡) ·
(∫2‘(𝑥
∈ ℝ ↦ ⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0)))) = ((i↑𝑡) · (∫2‘(𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0)))) |
12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ ((i↑𝑡) ·
(∫2‘(𝑥
∈ ℝ ↦ ⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0)))) = ((i↑𝑡) · (∫2‘(𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0))))) |
13 | 12 | sumeq2sdv 15747 |
. . 3
⊢ (⊤
→ Σ𝑡 ∈
(0...3)((i↑𝑡) ·
(∫2‘(𝑥
∈ ℝ ↦ ⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0)))) = Σ𝑡 ∈ (0...3)((i↑𝑡) · (∫2‘(𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0))))) |
14 | 13 | mptru 1544 |
. 2
⊢
Σ𝑡 ∈
(0...3)((i↑𝑡) ·
(∫2‘(𝑥
∈ ℝ ↦ ⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0)))) = Σ𝑡 ∈ (0...3)((i↑𝑡) · (∫2‘(𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0)))) |
15 | | df-itg 25670 |
. 2
⊢
∫𝐴𝐶 d𝑥 = Σ𝑡 ∈ (0...3)((i↑𝑡) · (∫2‘(𝑥 ∈ ℝ ↦
⦋(ℜ‘(𝐶 / (i↑𝑡))) / 𝑣⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣), 𝑣, 0)))) |
16 | | df-itg 25670 |
. 2
⊢
∫𝐵𝐷 d𝑦 = Σ𝑡 ∈ (0...3)((i↑𝑡) · (∫2‘(𝑦 ∈ ℝ ↦
⦋(ℜ‘(𝐷 / (i↑𝑡))) / 𝑣⦌if((𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣), 𝑣, 0)))) |
17 | 14, 15, 16 | 3eqtr4i 2772 |
1
⊢
∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦 |