Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
⊢ ℝ =
ℝ |
2 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))) → 𝑥 ∈ 𝐴) |
3 | 2 | con3i 150 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘))))) |
4 | 3 | iffalsed 4097 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = 0) |
5 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 𝑥 ∈ 𝐴) |
6 | 5 | con3i 150 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘))))) |
7 | 6 | iffalsed 4097 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = 0) |
8 | 4, 7 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
9 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝐵 = 𝐶 → (𝐵 / (i↑𝑘)) = (𝐶 / (i↑𝑘))) |
10 | 9 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝐵 = 𝐶 → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
11 | 10 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐶 → (0 ≤ (ℜ‘(𝐵 / (i↑𝑘))) ↔ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘))))) |
12 | 11 | anbi2d 740 |
. . . . . . . . . 10
⊢ (𝐵 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))))) |
13 | 12, 10 | ifbieq1d 4109 |
. . . . . . . . 9
⊢ (𝐵 = 𝐶 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
14 | 8, 13 | ja 173 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 → 𝐵 = 𝐶) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
15 | 14 | a1d 25 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 → 𝐵 = 𝐶) → (𝑥 ∈ ℝ → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
16 | 15 | ralimi2 2949 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
17 | | mpteq12 4736 |
. . . . . 6
⊢ ((ℝ
= ℝ ∧ ∀𝑥
∈ ℝ if((𝑥 ∈
𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0) =
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0)) →
(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))),
0))) |
18 | 1, 16, 17 | sylancr 695 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
19 | 18 | fveq2d 6195 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) |
20 | 19 | oveq2d 6666 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) =
((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))) |
21 | 20 | sumeq2sdv 14435 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) =
Σ𝑘 ∈
(0...3)((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))) |
22 | | eqid 2622 |
. . 3
⊢
(ℜ‘(𝐵 /
(i↑𝑘))) =
(ℜ‘(𝐵 /
(i↑𝑘))) |
23 | 22 | dfitg 23536 |
. 2
⊢
∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))),
0)))) |
24 | | eqid 2622 |
. . 3
⊢
(ℜ‘(𝐶 /
(i↑𝑘))) =
(ℜ‘(𝐶 /
(i↑𝑘))) |
25 | 24 | dfitg 23536 |
. 2
⊢
∫𝐴𝐶 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))),
0)))) |
26 | 21, 23, 25 | 3eqtr4g 2681 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥) |