Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(ℜ‘(𝐵 /
(i↑𝑘))) =
(ℜ‘(𝐵 /
(i↑𝑘))) |
2 | 1 | dfitg 24667 |
. . 3
⊢
∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))),
0)))) |
3 | | nn0uz 12476 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
4 | | df-3 11894 |
. . . . 5
⊢ 3 = (2 +
1) |
5 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑘 = 3 → (i↑𝑘) = (i↑3)) |
6 | | i3 13772 |
. . . . . . 7
⊢
(i↑3) = -i |
7 | 5, 6 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑘 = 3 → (i↑𝑘) = -i) |
8 | 6 | itgvallem 24682 |
. . . . . 6
⊢ (𝑘 = 3 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -i))),
(ℜ‘(𝐵 / -i)),
0)))) |
9 | 7, 8 | oveq12d 7231 |
. . . . 5
⊢ (𝑘 = 3 → ((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (-i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))) |
10 | | ax-icn 10788 |
. . . . . . . 8
⊢ i ∈
ℂ |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → i ∈
ℂ) |
12 | | expcl 13653 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝑘
∈ ℕ0) → (i↑𝑘) ∈ ℂ) |
13 | 11, 12 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(i↑𝑘) ∈
ℂ) |
14 | | nn0z 12200 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
15 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) |
16 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))) |
17 | | itgcnlem.i |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
18 | | itgcnlem.v |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
19 | 15, 16, 17, 18 | iblitg 24666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
20 | 19 | recnd 10861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℂ) |
21 | 14, 20 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℂ) |
22 | 13, 21 | mulcld 10853 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) ∈ ℂ) |
23 | | df-2 11893 |
. . . . . 6
⊢ 2 = (1 +
1) |
24 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑘 = 2 → (i↑𝑘) = (i↑2)) |
25 | | i2 13771 |
. . . . . . . 8
⊢
(i↑2) = -1 |
26 | 24, 25 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 = 2 → (i↑𝑘) = -1) |
27 | 25 | itgvallem 24682 |
. . . . . . 7
⊢ (𝑘 = 2 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -1))),
(ℜ‘(𝐵 / -1)),
0)))) |
28 | 26, 27 | oveq12d 7231 |
. . . . . 6
⊢ (𝑘 = 2 → ((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (-1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) |
29 | | 1e0p1 12335 |
. . . . . . 7
⊢ 1 = (0 +
1) |
30 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (i↑𝑘) = (i↑1)) |
31 | | exp1 13641 |
. . . . . . . . . 10
⊢ (i ∈
ℂ → (i↑1) = i) |
32 | 10, 31 | ax-mp 5 |
. . . . . . . . 9
⊢
(i↑1) = i |
33 | 30, 32 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑘 = 1 → (i↑𝑘) = i) |
34 | 32 | itgvallem 24682 |
. . . . . . . 8
⊢ (𝑘 = 1 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / i))),
(ℜ‘(𝐵 / i)),
0)))) |
35 | 33, 34 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑘 = 1 → ((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))) |
36 | | 0z 12187 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
37 | | itgcnlem.r |
. . . . . . . . . . . . . 14
⊢ 𝑅 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) |
38 | | iblmbf 24665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
39 | 17, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
40 | 39, 18 | mbfmptcl 24533 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
41 | 40 | div1d 11600 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 1) = 𝐵) |
42 | 41 | fveq2d 6721 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / 1)) = (ℜ‘𝐵)) |
43 | 42 | ibllem 24662 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)) |
44 | 43 | mpteq2dv 5151 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)) = (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘𝐵)),
(ℜ‘𝐵),
0))) |
45 | 44 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))) |
46 | 37, 45 | eqtr4id 2797 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / 1))),
(ℜ‘(𝐵 / 1)),
0)))) |
47 | 46 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 · 𝑅) = (1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))) |
48 | | itgcnlem.s |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) |
49 | | itgcnlem.t |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) |
50 | | itgcnlem.u |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑈 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) |
51 | 37, 48, 49, 50, 18 | iblcnlem 24686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |
52 | 17, 51 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))) |
53 | 52 | simp2d 1145 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ)) |
54 | 53 | simpld 498 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ ℝ) |
55 | 54 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℂ) |
56 | 55 | mulid2d 10851 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 · 𝑅) = 𝑅) |
57 | 47, 56 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) = 𝑅) |
58 | 57, 55 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) ∈
ℂ) |
59 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (i↑𝑘) = (i↑0)) |
60 | | exp0 13639 |
. . . . . . . . . . . . . 14
⊢ (i ∈
ℂ → (i↑0) = 1) |
61 | 10, 60 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(i↑0) = 1 |
62 | 59, 61 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (i↑𝑘) = 1) |
63 | 61 | itgvallem 24682 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / 1))),
(ℜ‘(𝐵 / 1)),
0)))) |
64 | 62, 63 | oveq12d 7231 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))) |
65 | 64 | fsum1 15311 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) ∈ ℂ)
→ Σ𝑘 ∈
(0...0)((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))) |
66 | 36, 58, 65 | sylancr 590 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) = (1
· (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))) |
67 | 66, 57 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) = 𝑅) |
68 | | 0nn0 12105 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
69 | 67, 68 | jctil 523 |
. . . . . . 7
⊢ (𝜑 → (0 ∈
ℕ0 ∧ Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) = 𝑅)) |
70 | | imval 14670 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) =
(ℜ‘(𝐵 /
i))) |
71 | 40, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) = (ℜ‘(𝐵 / i))) |
72 | 71 | ibllem 24662 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)) |
73 | 72 | mpteq2dv 5151 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) |
74 | 73 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))) |
75 | 49, 74 | eqtr2id 2791 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) = 𝑇) |
76 | 75 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝜑 → (i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))) = (i ·
𝑇)) |
77 | 76 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → (𝑅 + (i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))) = (𝑅 + (i · 𝑇))) |
78 | 3, 29, 35, 22, 69, 77 | fsump1i 15333 |
. . . . . 6
⊢ (𝜑 → (1 ∈
ℕ0 ∧ Σ𝑘 ∈ (0...1)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) =
(𝑅 + (i · 𝑇)))) |
79 | 40 | renegd 14772 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵)) |
80 | | ax-1cn 10787 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ |
81 | 80 | negnegi 11148 |
. . . . . . . . . . . . . . . . . . 19
⊢ --1 =
1 |
82 | 81 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . 18
⊢ (-𝐵 / --1) = (-𝐵 / 1) |
83 | 40 | negcld 11176 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
84 | 83 | div1d 11600 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / 1) = -𝐵) |
85 | 82, 84 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = -𝐵) |
86 | 80 | negcli 11146 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℂ |
87 | | neg1ne0 11946 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ≠
0 |
88 | | div2neg 11555 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℂ ∧ -1 ∈
ℂ ∧ -1 ≠ 0) → (-𝐵 / --1) = (𝐵 / -1)) |
89 | 86, 87, 88 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ ℂ → (-𝐵 / --1) = (𝐵 / -1)) |
90 | 40, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = (𝐵 / -1)) |
91 | 85, 90 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 = (𝐵 / -1)) |
92 | 91 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = (ℜ‘(𝐵 / -1))) |
93 | 79, 92 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘𝐵) = (ℜ‘(𝐵 / -1))) |
94 | 93 | ibllem 24662 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)) |
95 | 94 | mpteq2dv 5151 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) |
96 | 95 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))) |
97 | 48, 96 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -1))),
(ℜ‘(𝐵 / -1)),
0)))) |
98 | 97 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝜑 → (-1 · 𝑆) = (-1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) |
99 | 53 | simprd 499 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
100 | 99 | recnd 10861 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
101 | 100 | mulm1d 11284 |
. . . . . . . . 9
⊢ (𝜑 → (-1 · 𝑆) = -𝑆) |
102 | 98, 101 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (-1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))) = -𝑆) |
103 | 102 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 + (i · 𝑇)) + (-1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) = ((𝑅 + (i · 𝑇)) + -𝑆)) |
104 | 52 | simp3d 1146 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) |
105 | 104 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℝ) |
106 | 105 | recnd 10861 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ ℂ) |
107 | | mulcl 10813 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝑇
∈ ℂ) → (i · 𝑇) ∈ ℂ) |
108 | 10, 106, 107 | sylancr 590 |
. . . . . . . . 9
⊢ (𝜑 → (i · 𝑇) ∈
ℂ) |
109 | 55, 108 | addcld 10852 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 + (i · 𝑇)) ∈ ℂ) |
110 | 109, 100 | negsubd 11195 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 + (i · 𝑇)) + -𝑆) = ((𝑅 + (i · 𝑇)) − 𝑆)) |
111 | 55, 108, 100 | addsubd 11210 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 + (i · 𝑇)) − 𝑆) = ((𝑅 − 𝑆) + (i · 𝑇))) |
112 | 103, 110,
111 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → ((𝑅 + (i · 𝑇)) + (-1 ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) = ((𝑅 − 𝑆) + (i · 𝑇))) |
113 | 3, 23, 28, 22, 78, 112 | fsump1i 15333 |
. . . . 5
⊢ (𝜑 → (2 ∈
ℕ0 ∧ Σ𝑘 ∈ (0...2)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) =
((𝑅 − 𝑆) + (i · 𝑇)))) |
114 | | imval 14670 |
. . . . . . . . . . . . . 14
⊢ (-𝐵 ∈ ℂ →
(ℑ‘-𝐵) =
(ℜ‘(-𝐵 /
i))) |
115 | 83, 114 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i))) |
116 | 40 | imnegd 14773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵)) |
117 | 10 | negnegi 11148 |
. . . . . . . . . . . . . . . . 17
⊢ --i =
i |
118 | 117 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
⊢ i =
--i |
119 | 118 | oveq2i 7224 |
. . . . . . . . . . . . . . 15
⊢ (-𝐵 / i) = (-𝐵 / --i) |
120 | 10 | negcli 11146 |
. . . . . . . . . . . . . . . . 17
⊢ -i ∈
ℂ |
121 | | ine0 11267 |
. . . . . . . . . . . . . . . . . 18
⊢ i ≠
0 |
122 | 10, 121 | negne0i 11153 |
. . . . . . . . . . . . . . . . 17
⊢ -i ≠
0 |
123 | | div2neg 11555 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℂ ∧ -i ∈
ℂ ∧ -i ≠ 0) → (-𝐵 / --i) = (𝐵 / -i)) |
124 | 120, 122,
123 | mp3an23 1455 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℂ → (-𝐵 / --i) = (𝐵 / -i)) |
125 | 40, 124 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --i) = (𝐵 / -i)) |
126 | 119, 125 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / i) = (𝐵 / -i)) |
127 | 126 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(-𝐵 / i)) = (ℜ‘(𝐵 / -i))) |
128 | 115, 116,
127 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐵) = (ℜ‘(𝐵 / -i))) |
129 | 128 | ibllem 24662 |
. . . . . . . . . . 11
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)) |
130 | 129 | mpteq2dv 5151 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) |
131 | 130 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))) |
132 | 50, 131 | syl5eq 2790 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -i))),
(ℜ‘(𝐵 / -i)),
0)))) |
133 | 132 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → (-i · 𝑈) = (-i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))) |
134 | 104 | simprd 499 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ℝ) |
135 | 134 | recnd 10861 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ ℂ) |
136 | | mulneg12 11270 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝑈
∈ ℂ) → (-i · 𝑈) = (i · -𝑈)) |
137 | 10, 135, 136 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (-i · 𝑈) = (i · -𝑈)) |
138 | 133, 137 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (-i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))) = (i ·
-𝑈)) |
139 | 138 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 → (((𝑅 − 𝑆) + (i · 𝑇)) + (-i ·
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))) = (((𝑅 − 𝑆) + (i · 𝑇)) + (i · -𝑈))) |
140 | 3, 4, 9, 22, 113, 139 | fsump1i 15333 |
. . . 4
⊢ (𝜑 → (3 ∈
ℕ0 ∧ Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) =
(((𝑅 − 𝑆) + (i · 𝑇)) + (i · -𝑈)))) |
141 | 140 | simprd 499 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑𝑘)))),
(ℜ‘(𝐵 /
(i↑𝑘))), 0)))) =
(((𝑅 − 𝑆) + (i · 𝑇)) + (i · -𝑈))) |
142 | 2, 141 | syl5eq 2790 |
. 2
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (((𝑅 − 𝑆) + (i · 𝑇)) + (i · -𝑈))) |
143 | 55, 100 | subcld 11189 |
. . 3
⊢ (𝜑 → (𝑅 − 𝑆) ∈ ℂ) |
144 | 135 | negcld 11176 |
. . . 4
⊢ (𝜑 → -𝑈 ∈ ℂ) |
145 | | mulcl 10813 |
. . . 4
⊢ ((i
∈ ℂ ∧ -𝑈
∈ ℂ) → (i · -𝑈) ∈ ℂ) |
146 | 10, 144, 145 | sylancr 590 |
. . 3
⊢ (𝜑 → (i · -𝑈) ∈
ℂ) |
147 | 143, 108,
146 | addassd 10855 |
. 2
⊢ (𝜑 → (((𝑅 − 𝑆) + (i · 𝑇)) + (i · -𝑈)) = ((𝑅 − 𝑆) + ((i · 𝑇) + (i · -𝑈)))) |
148 | 11, 106, 144 | adddid 10857 |
. . . 4
⊢ (𝜑 → (i · (𝑇 + -𝑈)) = ((i · 𝑇) + (i · -𝑈))) |
149 | 106, 135 | negsubd 11195 |
. . . . 5
⊢ (𝜑 → (𝑇 + -𝑈) = (𝑇 − 𝑈)) |
150 | 149 | oveq2d 7229 |
. . . 4
⊢ (𝜑 → (i · (𝑇 + -𝑈)) = (i · (𝑇 − 𝑈))) |
151 | 148, 150 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → ((i · 𝑇) + (i · -𝑈)) = (i · (𝑇 − 𝑈))) |
152 | 151 | oveq2d 7229 |
. 2
⊢ (𝜑 → ((𝑅 − 𝑆) + ((i · 𝑇) + (i · -𝑈))) = ((𝑅 − 𝑆) + (i · (𝑇 − 𝑈)))) |
153 | 142, 147,
152 | 3eqtrd 2781 |
1
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((𝑅 − 𝑆) + (i · (𝑇 − 𝑈)))) |