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

Theorem itgcnlem 23362
 Description: Expand out the sum in dfitg 23342. (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 2610 . . . 4 (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))
21dfitg 23342 . . 3 𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))))
3 nn0uz 11598 . . . . 5 0 = (ℤ‘0)
4 df-3 10957 . . . . 5 3 = (2 + 1)
5 oveq2 6557 . . . . . . 7 (𝑘 = 3 → (i↑𝑘) = (i↑3))
6 i3 12828 . . . . . . 7 (i↑3) = -i
75, 6syl6eq 2660 . . . . . 6 (𝑘 = 3 → (i↑𝑘) = -i)
86itgvallem 23357 . . . . . 6 (𝑘 = 3 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
97, 8oveq12d 6567 . . . . 5 (𝑘 = 3 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))))
10 ax-icn 9874 . . . . . . . 8 i ∈ ℂ
1110a1i 11 . . . . . . 7 (𝜑 → i ∈ ℂ)
12 expcl 12740 . . . . . . 7 ((i ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (i↑𝑘) ∈ ℂ)
1311, 12sylan 487 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (i↑𝑘) ∈ ℂ)
14 nn0z 11277 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
15 eqidd 2611 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))
16 eqidd 2611 . . . . . . . . 9 ((𝜑𝑥𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
17 itgcnlem.i . . . . . . . . 9 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
18 itgcnlem.v . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝐵𝑉)
1915, 16, 17, 18iblitg 23341 . . . . . . . 8 ((𝜑𝑘 ∈ ℤ) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)
2019recnd 9947 . . . . . . 7 ((𝜑𝑘 ∈ ℤ) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℂ)
2114, 20sylan2 490 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℂ)
2213, 21mulcld 9939 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) ∈ ℂ)
23 df-2 10956 . . . . . 6 2 = (1 + 1)
24 oveq2 6557 . . . . . . . 8 (𝑘 = 2 → (i↑𝑘) = (i↑2))
25 i2 12827 . . . . . . . 8 (i↑2) = -1
2624, 25syl6eq 2660 . . . . . . 7 (𝑘 = 2 → (i↑𝑘) = -1)
2725itgvallem 23357 . . . . . . 7 (𝑘 = 2 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
2826, 27oveq12d 6567 . . . . . 6 (𝑘 = 2 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))))
29 1e0p1 11428 . . . . . . 7 1 = (0 + 1)
30 oveq2 6557 . . . . . . . . 9 (𝑘 = 1 → (i↑𝑘) = (i↑1))
31 exp1 12728 . . . . . . . . . 10 (i ∈ ℂ → (i↑1) = i)
3210, 31ax-mp 5 . . . . . . . . 9 (i↑1) = i
3330, 32syl6eq 2660 . . . . . . . 8 (𝑘 = 1 → (i↑𝑘) = i)
3432itgvallem 23357 . . . . . . . 8 (𝑘 = 1 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))
3533, 34oveq12d 6567 . . . . . . 7 (𝑘 = 1 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))))
36 0z 11265 . . . . . . . . . 10 0 ∈ ℤ
37 iblmbf 23340 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴𝐵) ∈ 𝐿1 → (𝑥𝐴𝐵) ∈ MblFn)
3817, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
3938, 18mbfmptcl 23210 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
4039div1d 10672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝐵 / 1) = 𝐵)
4140fveq2d 6107 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (ℜ‘(𝐵 / 1)) = (ℜ‘𝐵))
4241ibllem 23337 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))
4342mpteq2dv 4673 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
4443fveq2d 6107 . . . . . . . . . . . . . 14 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))))
45 itgcnlem.r . . . . . . . . . . . . . 14 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
4644, 45syl6reqr 2663 . . . . . . . . . . . . 13 (𝜑𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))
4746oveq2d 6565 . . . . . . . . . . . 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 23361 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑥𝐴𝐵) ∈ 𝐿1 ↔ ((𝑥𝐴𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
5217, 51mpbid 221 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑥𝐴𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))
5352simp2d 1067 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ))
5453simpld 474 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ ℝ)
5554recnd 9947 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ℂ)
5655mulid2d 9937 . . . . . . . . . . . 12 (𝜑 → (1 · 𝑅) = 𝑅)
5747, 56eqtr3d 2646 . . . . . . . . . . 11 (𝜑 → (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) = 𝑅)
5857, 55eqeltrd 2688 . . . . . . . . . 10 (𝜑 → (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))) ∈ ℂ)
59 oveq2 6557 . . . . . . . . . . . . 13 (𝑘 = 0 → (i↑𝑘) = (i↑0))
60 exp0 12726 . . . . . . . . . . . . . 14 (i ∈ ℂ → (i↑0) = 1)
6110, 60ax-mp 5 . . . . . . . . . . . . 13 (i↑0) = 1
6259, 61syl6eq 2660 . . . . . . . . . . . 12 (𝑘 = 0 → (i↑𝑘) = 1)
6361itgvallem 23357 . . . . . . . . . . . 12 (𝑘 = 0 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))
6462, 63oveq12d 6567 . . . . . . . . . . 11 (𝑘 = 0 → ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))))
6564fsum1 14320 . . . . . . . . . 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 694 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)))))
6766, 57eqtrd 2644 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = 𝑅)
68 0nn0 11184 . . . . . . . 8 0 ∈ ℕ0
6967, 68jctil 558 . . . . . . 7 (𝜑 → (0 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...0)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = 𝑅))
70 imval 13695 . . . . . . . . . . . . . 14 (𝐵 ∈ ℂ → (ℑ‘𝐵) = (ℜ‘(𝐵 / i)))
7139, 70syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℑ‘𝐵) = (ℜ‘(𝐵 / i)))
7271ibllem 23337 . . . . . . . . . . . 12 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))
7372mpteq2dv 4673 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))
7473fveq2d 6107 . . . . . . . . . 10 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))
7549, 74syl5req 2657 . . . . . . . . 9 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) = 𝑇)
7675oveq2d 6565 . . . . . . . 8 (𝜑 → (i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))) = (i · 𝑇))
7776oveq2d 6565 . . . . . . 7 (𝜑 → (𝑅 + (i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))) = (𝑅 + (i · 𝑇)))
783, 29, 35, 22, 69, 77fsump1i 14342 . . . . . 6 (𝜑 → (1 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...1)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (𝑅 + (i · 𝑇))))
7939renegd 13797 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵))
80 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℂ
8180negnegi 10230 . . . . . . . . . . . . . . . . . . 19 --1 = 1
8281oveq2i 6560 . . . . . . . . . . . . . . . . . 18 (-𝐵 / --1) = (-𝐵 / 1)
8339negcld 10258 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → -𝐵 ∈ ℂ)
8483div1d 10672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (-𝐵 / 1) = -𝐵)
8582, 84syl5eq 2656 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (-𝐵 / --1) = -𝐵)
8680negcli 10228 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℂ
87 neg1ne0 11003 . . . . . . . . . . . . . . . . . . 19 -1 ≠ 0
88 div2neg 10627 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ ℂ ∧ -1 ∈ ℂ ∧ -1 ≠ 0) → (-𝐵 / --1) = (𝐵 / -1))
8986, 87, 88mp3an23 1408 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ ℂ → (-𝐵 / --1) = (𝐵 / -1))
9039, 89syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (-𝐵 / --1) = (𝐵 / -1))
9185, 90eqtr3d 2646 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → -𝐵 = (𝐵 / -1))
9291fveq2d 6107 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (ℜ‘-𝐵) = (ℜ‘(𝐵 / -1)))
9379, 92eqtr3d 2646 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → -(ℜ‘𝐵) = (ℜ‘(𝐵 / -1)))
9493ibllem 23337 . . . . . . . . . . . . 13 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))
9594mpteq2dv 4673 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))
9695fveq2d 6107 . . . . . . . . . . 11 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
9748, 96syl5eq 2656 . . . . . . . . . 10 (𝜑𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
9897oveq2d 6565 . . . . . . . . 9 (𝜑 → (-1 · 𝑆) = (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))))
9953simprd 478 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
10099recnd 9947 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
101100mulm1d 10361 . . . . . . . . 9 (𝜑 → (-1 · 𝑆) = -𝑆)
10298, 101eqtr3d 2646 . . . . . . . 8 (𝜑 → (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))) = -𝑆)
103102oveq2d 6565 . . . . . . 7 (𝜑 → ((𝑅 + (i · 𝑇)) + (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) = ((𝑅 + (i · 𝑇)) + -𝑆))
10452simp3d 1068 . . . . . . . . . . . 12 (𝜑 → (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))
105104simpld 474 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
106105recnd 9947 . . . . . . . . . 10 (𝜑𝑇 ∈ ℂ)
107 mulcl 9899 . . . . . . . . . 10 ((i ∈ ℂ ∧ 𝑇 ∈ ℂ) → (i · 𝑇) ∈ ℂ)
10810, 106, 107sylancr 694 . . . . . . . . 9 (𝜑 → (i · 𝑇) ∈ ℂ)
10955, 108addcld 9938 . . . . . . . 8 (𝜑 → (𝑅 + (i · 𝑇)) ∈ ℂ)
110109, 100negsubd 10277 . . . . . . 7 (𝜑 → ((𝑅 + (i · 𝑇)) + -𝑆) = ((𝑅 + (i · 𝑇)) − 𝑆))
11155, 108, 100addsubd 10292 . . . . . . 7 (𝜑 → ((𝑅 + (i · 𝑇)) − 𝑆) = ((𝑅𝑆) + (i · 𝑇)))
112103, 110, 1113eqtrd 2648 . . . . . 6 (𝜑 → ((𝑅 + (i · 𝑇)) + (-1 · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))) = ((𝑅𝑆) + (i · 𝑇)))
1133, 23, 28, 22, 78, 112fsump1i 14342 . . . . 5 (𝜑 → (2 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...2)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = ((𝑅𝑆) + (i · 𝑇))))
114 imval 13695 . . . . . . . . . . . . . 14 (-𝐵 ∈ ℂ → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i)))
11583, 114syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i)))
11639imnegd 13798 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵))
11710negnegi 10230 . . . . . . . . . . . . . . . . 17 --i = i
118117eqcomi 2619 . . . . . . . . . . . . . . . 16 i = --i
119118oveq2i 6560 . . . . . . . . . . . . . . 15 (-𝐵 / i) = (-𝐵 / --i)
12010negcli 10228 . . . . . . . . . . . . . . . . 17 -i ∈ ℂ
121 ine0 10344 . . . . . . . . . . . . . . . . . 18 i ≠ 0
12210, 121negne0i 10235 . . . . . . . . . . . . . . . . 17 -i ≠ 0
123 div2neg 10627 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ -i ∈ ℂ ∧ -i ≠ 0) → (-𝐵 / --i) = (𝐵 / -i))
124120, 122, 123mp3an23 1408 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℂ → (-𝐵 / --i) = (𝐵 / -i))
12539, 124syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (-𝐵 / --i) = (𝐵 / -i))
126119, 125syl5eq 2656 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (-𝐵 / i) = (𝐵 / -i))
127126fveq2d 6107 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (ℜ‘(-𝐵 / i)) = (ℜ‘(𝐵 / -i)))
128115, 116, 1273eqtr3d 2652 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → -(ℑ‘𝐵) = (ℜ‘(𝐵 / -i)))
129128ibllem 23337 . . . . . . . . . . 11 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))
130129mpteq2dv 4673 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))
131130fveq2d 6107 . . . . . . . . 9 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
13250, 131syl5eq 2656 . . . . . . . 8 (𝜑𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
133132oveq2d 6565 . . . . . . 7 (𝜑 → (-i · 𝑈) = (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))))
134104simprd 478 . . . . . . . . 9 (𝜑𝑈 ∈ ℝ)
135134recnd 9947 . . . . . . . 8 (𝜑𝑈 ∈ ℂ)
136 mulneg12 10347 . . . . . . . 8 ((i ∈ ℂ ∧ 𝑈 ∈ ℂ) → (-i · 𝑈) = (i · -𝑈))
13710, 135, 136sylancr 694 . . . . . . 7 (𝜑 → (-i · 𝑈) = (i · -𝑈))
138133, 137eqtr3d 2646 . . . . . 6 (𝜑 → (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))) = (i · -𝑈))
139138oveq2d 6565 . . . . 5 (𝜑 → (((𝑅𝑆) + (i · 𝑇)) + (-i · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))) = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)))
1403, 4, 9, 22, 113, 139fsump1i 14342 . . . 4 (𝜑 → (3 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈))))
141140simprd 478 . . 3 (𝜑 → Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))) = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)))
1422, 141syl5eq 2656 . 2 (𝜑 → ∫𝐴𝐵 d𝑥 = (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)))
14355, 100subcld 10271 . . 3 (𝜑 → (𝑅𝑆) ∈ ℂ)
144135negcld 10258 . . . 4 (𝜑 → -𝑈 ∈ ℂ)
145 mulcl 9899 . . . 4 ((i ∈ ℂ ∧ -𝑈 ∈ ℂ) → (i · -𝑈) ∈ ℂ)
14610, 144, 145sylancr 694 . . 3 (𝜑 → (i · -𝑈) ∈ ℂ)
147143, 108, 146addassd 9941 . 2 (𝜑 → (((𝑅𝑆) + (i · 𝑇)) + (i · -𝑈)) = ((𝑅𝑆) + ((i · 𝑇) + (i · -𝑈))))
14811, 106, 144adddid 9943 . . . 4 (𝜑 → (i · (𝑇 + -𝑈)) = ((i · 𝑇) + (i · -𝑈)))
149106, 135negsubd 10277 . . . . 5 (𝜑 → (𝑇 + -𝑈) = (𝑇𝑈))
150149oveq2d 6565 . . . 4 (𝜑 → (i · (𝑇 + -𝑈)) = (i · (𝑇𝑈)))
151148, 150eqtr3d 2646 . . 3 (𝜑 → ((i · 𝑇) + (i · -𝑈)) = (i · (𝑇𝑈)))
152151oveq2d 6565 . 2 (𝜑 → ((𝑅𝑆) + ((i · 𝑇) + (i · -𝑈))) = ((𝑅𝑆) + (i · (𝑇𝑈))))
153142, 147, 1523eqtrd 2648 1 (𝜑 → ∫𝐴𝐵 d𝑥 = ((𝑅𝑆) + (i · (𝑇𝑈))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816  ici 9817   + caddc 9818   · cmul 9820   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  2c2 10947  3c3 10948  ℕ0cn0 11169  ℤcz 11254  ...cfz 12197  ↑cexp 12722  ℜcre 13685  ℑcim 13686  Σcsu 14264  MblFncmbf 23189  ∫2citg2 23191  𝐿1cibl 23192  ∫citg 23193 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-mbf 23194  df-ibl 23197  df-itg 23198 This theorem is referenced by:  itgrevallem1  23367  itgcnval  23372
 Copyright terms: Public domain W3C validator