MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itgcnlem Structured version   Visualization version   GIF version

Theorem itgcnlem 23306
Description: Expand out the sum in dfitg 23286. (Contributed by Mario Carneiro, 1-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
itgcnlem.r 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
itgcnlem.s 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))
itgcnlem.t 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))
itgcnlem.u 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))
itgcnlem.v ((𝜑𝑥𝐴) → 𝐵𝑉)
itgcnlem.i (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
Assertion
Ref Expression
itgcnlem (𝜑 → ∫𝐴𝐵 d𝑥 = ((𝑅𝑆) + (i · (𝑇𝑈))))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝑉
Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥)   𝑇(𝑥)   𝑈(𝑥)

Proof of Theorem itgcnlem
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 eqid 2609 . . . 4 (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))
21dfitg 23286 . . 3 𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))))
3 nn0uz 11556 . . . . 5 0 = (ℤ‘0)
4 df-3 10929 . . . . 5 3 = (2 + 1)
5 oveq2 6534 . . . . . . 7 (𝑘 = 3 → (i↑𝑘) = (i↑3))
6 i3 12785 . . . . . . 7 (i↑3) = -i
75, 6syl6eq 2659 . . . . . 6 (𝑘 = 3 → (i↑𝑘) = -i)
86itgvallem 23301 . . . . . 6 (𝑘 = 3 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
97, 8oveq12d 6544 . . . . 5 (𝑘 = 3 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))))
10 ax-icn 9851 . . . . . . . 8 i ∈ ℂ
1110a1i 11 . . . . . . 7 (𝜑 → i ∈ ℂ)
12 expcl 12697 . . . . . . 7 ((i ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (i↑𝑘) ∈ ℂ)
1311, 12sylan 486 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (i↑𝑘) ∈ ℂ)
14 nn0z 11235 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
15 eqidd 2610 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))
16 eqidd 2610 . . . . . . . . 9 ((𝜑𝑥𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
17 itgcnlem.i . . . . . . . . 9 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
18 itgcnlem.v . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝐵𝑉)
1915, 16, 17, 18iblitg 23285 . . . . . . . 8 ((𝜑𝑘 ∈ ℤ) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)
2019recnd 9924 . . . . . . 7 ((𝜑𝑘 ∈ ℤ) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℂ)
2114, 20sylan2 489 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℂ)
2213, 21mulcld 9916 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) ∈ ℂ)
23 df-2 10928 . . . . . 6 2 = (1 + 1)
24 oveq2 6534 . . . . . . . 8 (𝑘 = 2 → (i↑𝑘) = (i↑2))
25 i2 12784 . . . . . . . 8 (i↑2) = -1
2624, 25syl6eq 2659 . . . . . . 7 (𝑘 = 2 → (i↑𝑘) = -1)
2725itgvallem 23301 . . . . . . 7 (𝑘 = 2 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
2826, 27oveq12d 6544 . . . . . 6 (𝑘 = 2 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))))
29 1e0p1 11386 . . . . . . 7 1 = (0 + 1)
30 oveq2 6534 . . . . . . . . 9 (𝑘 = 1 → (i↑𝑘) = (i↑1))
31 exp1 12685 . . . . . . . . . 10 (i ∈ ℂ → (i↑1) = i)
3210, 31ax-mp 5 . . . . . . . . 9 (i↑1) = i
3330, 32syl6eq 2659 . . . . . . . 8 (𝑘 = 1 → (i↑𝑘) = i)
3432itgvallem 23301 . . . . . . . 8 (𝑘 = 1 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))
3533, 34oveq12d 6544 . . . . . . 7 (𝑘 = 1 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))))
36 0z 11223 . . . . . . . . . 10 0 ∈ ℤ
37 iblmbf 23284 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴𝐵) ∈ 𝐿1 → (𝑥𝐴𝐵) ∈ MblFn)
3817, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
3938, 18mbfmptcl 23154 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
4039div1d 10644 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 1) = 𝐵)
4140fveq2d 6091 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (ℜ‘(𝐵 / 1)) = (ℜ‘𝐵))
4241ibllem 23281 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))
4342mpteq2dv 4667 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
4443fveq2d 6091 . . . . . . . . . . . . . 14 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))))
45 itgcnlem.r . . . . . . . . . . . . . 14 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
4644, 45syl6reqr 2662 . . . . . . . . . . . . 13 (𝜑𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))
4746oveq2d 6542 . . . . . . . . . . . 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)))
5145, 48, 49, 50, 18iblcnlem 23305 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑥𝐴𝐵) ∈ 𝐿1 ↔ ((𝑥𝐴𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
5217, 51mpbid 220 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑥𝐴𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))
5352simp2d 1066 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ))
5453simpld 473 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ ℝ)
5554recnd 9924 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ℂ)
5655mulid2d 9914 . . . . . . . . . . . 12 (𝜑 → (1 · 𝑅) = 𝑅)
5747, 56eqtr3d 2645 . . . . . . . . . . 11 (𝜑 → (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) = 𝑅)
5857, 55eqeltrd 2687 . . . . . . . . . 10 (𝜑 → (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) ∈ ℂ)
59 oveq2 6534 . . . . . . . . . . . . 13 (𝑘 = 0 → (i↑𝑘) = (i↑0))
60 exp0 12683 . . . . . . . . . . . . . 14 (i ∈ ℂ → (i↑0) = 1)
6110, 60ax-mp 5 . . . . . . . . . . . . 13 (i↑0) = 1
6259, 61syl6eq 2659 . . . . . . . . . . . 12 (𝑘 = 0 → (i↑𝑘) = 1)
6361itgvallem 23301 . . . . . . . . . . . 12 (𝑘 = 0 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))
6462, 63oveq12d 6544 . . . . . . . . . . 11 (𝑘 = 0 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))))
6564fsum1 14268 . . . . . . . . . 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)))))
6636, 58, 65sylancr 693 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))))
6766, 57eqtrd 2643 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = 𝑅)
68 0nn0 11156 . . . . . . . 8 0 ∈ ℕ0
6967, 68jctil 557 . . . . . . 7 (𝜑 → (0 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = 𝑅))
70 imval 13643 . . . . . . . . . . . . . 14 (𝐵 ∈ ℂ → (ℑ‘𝐵) = (ℜ‘(𝐵 / i)))
7139, 70syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℑ‘𝐵) = (ℜ‘(𝐵 / i)))
7271ibllem 23281 . . . . . . . . . . . 12 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))
7372mpteq2dv 4667 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))
7473fveq2d 6091 . . . . . . . . . 10 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))
7549, 74syl5req 2656 . . . . . . . . 9 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) = 𝑇)
7675oveq2d 6542 . . . . . . . 8 (𝜑 → (i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))) = (i · 𝑇))
7776oveq2d 6542 . . . . . . 7 (𝜑 → (𝑅 + (i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))) = (𝑅 + (i · 𝑇)))
783, 29, 35, 22, 69, 77fsump1i 14290 . . . . . 6 (𝜑 → (1 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...1)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (𝑅 + (i · 𝑇))))
7939renegd 13745 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵))
80 ax-1cn 9850 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℂ
8180negnegi 10202 . . . . . . . . . . . . . . . . . . 19 --1 = 1
8281oveq2i 6537 . . . . . . . . . . . . . . . . . 18 (-𝐵 / --1) = (-𝐵 / 1)
8339negcld 10230 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → -𝐵 ∈ ℂ)
8483div1d 10644 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (-𝐵 / 1) = -𝐵)
8582, 84syl5eq 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (-𝐵 / --1) = -𝐵)
8680negcli 10200 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℂ
87 neg1ne0 10975 . . . . . . . . . . . . . . . . . . 19 -1 ≠ 0
88 div2neg 10599 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ ℂ ∧ -1 ∈ ℂ ∧ -1 ≠ 0) → (-𝐵 / --1) = (𝐵 / -1))
8986, 87, 88mp3an23 1407 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ ℂ → (-𝐵 / --1) = (𝐵 / -1))
9039, 89syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (-𝐵 / --1) = (𝐵 / -1))
9185, 90eqtr3d 2645 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → -𝐵 = (𝐵 / -1))
9291fveq2d 6091 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (ℜ‘-𝐵) = (ℜ‘(𝐵 / -1)))
9379, 92eqtr3d 2645 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → -(ℜ‘𝐵) = (ℜ‘(𝐵 / -1)))
9493ibllem 23281 . . . . . . . . . . . . 13 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))
9594mpteq2dv 4667 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))
9695fveq2d 6091 . . . . . . . . . . 11 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
9748, 96syl5eq 2655 . . . . . . . . . 10 (𝜑𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
9897oveq2d 6542 . . . . . . . . 9 (𝜑 → (-1 · 𝑆) = (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))))
9953simprd 477 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
10099recnd 9924 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
101100mulm1d 10333 . . . . . . . . 9 (𝜑 → (-1 · 𝑆) = -𝑆)
10298, 101eqtr3d 2645 . . . . . . . 8 (𝜑 → (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))) = -𝑆)
103102oveq2d 6542 . . . . . . 7 (𝜑 → ((𝑅 + (i · 𝑇)) + (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) = ((𝑅 + (i · 𝑇)) + -𝑆))
10452simp3d 1067 . . . . . . . . . . . 12 (𝜑 → (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))
105104simpld 473 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
106105recnd 9924 . . . . . . . . . 10 (𝜑𝑇 ∈ ℂ)
107 mulcl 9876 . . . . . . . . . 10 ((i ∈ ℂ ∧ 𝑇 ∈ ℂ) → (i · 𝑇) ∈ ℂ)
10810, 106, 107sylancr 693 . . . . . . . . 9 (𝜑 → (i · 𝑇) ∈ ℂ)
10955, 108addcld 9915 . . . . . . . 8 (𝜑 → (𝑅 + (i · 𝑇)) ∈ ℂ)
110109, 100negsubd 10249 . . . . . . 7 (𝜑 → ((𝑅 + (i · 𝑇)) + -𝑆) = ((𝑅 + (i · 𝑇)) − 𝑆))
11155, 108, 100addsubd 10264 . . . . . . 7 (𝜑 → ((𝑅 + (i · 𝑇)) − 𝑆) = ((𝑅𝑆) + (i · 𝑇)))
112103, 110, 1113eqtrd 2647 . . . . . 6 (𝜑 → ((𝑅 + (i · 𝑇)) + (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) = ((𝑅𝑆) + (i · 𝑇)))
1133, 23, 28, 22, 78, 112fsump1i 14290 . . . . 5 (𝜑 → (2 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...2)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = ((𝑅𝑆) + (i · 𝑇))))
114 imval 13643 . . . . . . . . . . . . . 14 (-𝐵 ∈ ℂ → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i)))
11583, 114syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i)))
11639imnegd 13746 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵))
11710negnegi 10202 . . . . . . . . . . . . . . . . 17 --i = i
118117eqcomi 2618 . . . . . . . . . . . . . . . 16 i = --i
119118oveq2i 6537 . . . . . . . . . . . . . . 15 (-𝐵 / i) = (-𝐵 / --i)
12010negcli 10200 . . . . . . . . . . . . . . . . 17 -i ∈ ℂ
121 ine0 10316 . . . . . . . . . . . . . . . . . 18 i ≠ 0
12210, 121negne0i 10207 . . . . . . . . . . . . . . . . 17 -i ≠ 0
123 div2neg 10599 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ -i ∈ ℂ ∧ -i ≠ 0) → (-𝐵 / --i) = (𝐵 / -i))
124120, 122, 123mp3an23 1407 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℂ → (-𝐵 / --i) = (𝐵 / -i))
12539, 124syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (-𝐵 / --i) = (𝐵 / -i))
126119, 125syl5eq 2655 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (-𝐵 / i) = (𝐵 / -i))
127126fveq2d 6091 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℜ‘(-𝐵 / i)) = (ℜ‘(𝐵 / -i)))
128115, 116, 1273eqtr3d 2651 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → -(ℑ‘𝐵) = (ℜ‘(𝐵 / -i)))
129128ibllem 23281 . . . . . . . . . . 11 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))
130129mpteq2dv 4667 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))
131130fveq2d 6091 . . . . . . . . 9 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
13250, 131syl5eq 2655 . . . . . . . 8 (𝜑𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
133132oveq2d 6542 . . . . . . 7 (𝜑 → (-i · 𝑈) = (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))))
134104simprd 477 . . . . . . . . 9 (𝜑𝑈 ∈ ℝ)
135134recnd 9924 . . . . . . . 8 (𝜑𝑈 ∈ ℂ)
136 mulneg12 10319 . . . . . . . 8 ((i ∈ ℂ ∧ 𝑈 ∈ ℂ) → (-i · 𝑈) = (i · -𝑈))
13710, 135, 136sylancr 693 . . . . . . 7 (𝜑 → (-i · 𝑈) = (i · -𝑈))
138133, 137eqtr3d 2645 . . . . . 6 (𝜑 → (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))) = (i · -𝑈))
139138oveq2d 6542 . . . . 5 (𝜑 → (((𝑅𝑆) + (i · 𝑇)) + (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))) = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)))
1403, 4, 9, 22, 113, 139fsump1i 14290 . . . 4 (𝜑 → (3 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈))))
141140simprd 477 . . 3 (𝜑 → Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)))
1422, 141syl5eq 2655 . 2 (𝜑 → ∫𝐴𝐵 d𝑥 = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)))
14355, 100subcld 10243 . . 3 (𝜑 → (𝑅𝑆) ∈ ℂ)
144135negcld 10230 . . . 4 (𝜑 → -𝑈 ∈ ℂ)
145 mulcl 9876 . . . 4 ((i ∈ ℂ ∧ -𝑈 ∈ ℂ) → (i · -𝑈) ∈ ℂ)
14610, 144, 145sylancr 693 . . 3 (𝜑 → (i · -𝑈) ∈ ℂ)
147143, 108, 146addassd 9918 . 2 (𝜑 → (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)) = ((𝑅𝑆) + ((i · 𝑇) + (i · -𝑈))))
14811, 106, 144adddid 9920 . . . 4 (𝜑 → (i · (𝑇 + -𝑈)) = ((i · 𝑇) + (i · -𝑈)))
149106, 135negsubd 10249 . . . . 5 (𝜑 → (𝑇 + -𝑈) = (𝑇𝑈))
150149oveq2d 6542 . . . 4 (𝜑 → (i · (𝑇 + -𝑈)) = (i · (𝑇𝑈)))
151148, 150eqtr3d 2645 . . 3 (𝜑 → ((i · 𝑇) + (i · -𝑈)) = (i · (𝑇𝑈)))
152151oveq2d 6542 . 2 (𝜑 → ((𝑅𝑆) + ((i · 𝑇) + (i · -𝑈))) = ((𝑅𝑆) + (i · (𝑇𝑈))))
153142, 147, 1523eqtrd 2647 1 (𝜑 → ∫𝐴𝐵 d𝑥 = ((𝑅𝑆) + (i · (𝑇𝑈))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  ifcif 4035   class class class wbr 4577  cmpt 4637  cfv 5789  (class class class)co 6526  cc 9790  cr 9791  0cc0 9792  1c1 9793  ici 9794   + caddc 9795   · cmul 9797  cle 9931  cmin 10117  -cneg 10118   / cdiv 10535  2c2 10919  3c3 10920  0cn0 11141  cz 11212  ...cfz 12154  cexp 12679  cre 13633  cim 13634  Σcsu 14212  MblFncmbf 23133  2citg2 23135  𝐿1cibl 23136  citg 23137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-n0 11142  df-z 11213  df-uz 11522  df-rp 11667  df-fz 12155  df-fzo 12292  df-fl 12412  df-mod 12488  df-seq 12621  df-exp 12680  df-hash 12937  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-clim 14015  df-sum 14213  df-mbf 23138  df-ibl 23141  df-itg 23142
This theorem is referenced by:  itgrevallem1  23311  itgcnval  23316
  Copyright terms: Public domain W3C validator