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

 Description: Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
Hypotheses
Ref Expression
itgadd.2 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
itgadd.4 (𝜑 → (𝑥𝐴𝐶) ∈ 𝐿1)
Assertion
Ref Expression
ibladd (𝜑 → (𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑉   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

StepHypRef Expression
1 itgadd.2 . . . . . . 7 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
2 eqid 2760 . . . . . . . 8 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
3 eqid 2760 . . . . . . . 8 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))
4 eqid 2760 . . . . . . . 8 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))
5 eqid 2760 . . . . . . . 8 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))
6 itgadd.1 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐵𝑉)
72, 3, 4, 5, 6iblcnlem 23754 . . . . . . 7 (𝜑 → ((𝑥𝐴𝐵) ∈ 𝐿1 ↔ ((𝑥𝐴𝐵) ∈ MblFn ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) ∈ ℝ) ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) ∈ ℝ))))
81, 7mpbid 222 . . . . . 6 (𝜑 → ((𝑥𝐴𝐵) ∈ MblFn ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) ∈ ℝ) ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) ∈ ℝ)))
98simp1d 1137 . . . . 5 (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
109, 6mbfdm2 23604 . . . 4 (𝜑𝐴 ∈ dom vol)
11 itgadd.3 . . . 4 ((𝜑𝑥𝐴) → 𝐶𝑉)
12 eqidd 2761 . . . 4 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐵))
13 eqidd 2761 . . . 4 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐴𝐶))
1410, 6, 11, 12, 13offval2 7079 . . 3 (𝜑 → ((𝑥𝐴𝐵) ∘𝑓 + (𝑥𝐴𝐶)) = (𝑥𝐴 ↦ (𝐵 + 𝐶)))
15 itgadd.4 . . . . . 6 (𝜑 → (𝑥𝐴𝐶) ∈ 𝐿1)
16 eqid 2760 . . . . . . 7 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐶)), (ℜ‘𝐶), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐶)), (ℜ‘𝐶), 0)))
17 eqid 2760 . . . . . . 7 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐶)), -(ℜ‘𝐶), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐶)), -(ℜ‘𝐶), 0)))
18 eqid 2760 . . . . . . 7 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐶)), (ℑ‘𝐶), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐶)), (ℑ‘𝐶), 0)))
19 eqid 2760 . . . . . . 7 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐶)), -(ℑ‘𝐶), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐶)), -(ℑ‘𝐶), 0)))
2016, 17, 18, 19, 11iblcnlem 23754 . . . . . 6 (𝜑 → ((𝑥𝐴𝐶) ∈ 𝐿1 ↔ ((𝑥𝐴𝐶) ∈ MblFn ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐶)), (ℜ‘𝐶), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐶)), -(ℜ‘𝐶), 0))) ∈ ℝ) ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐶)), (ℑ‘𝐶), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐶)), -(ℑ‘𝐶), 0))) ∈ ℝ))))
2115, 20mpbid 222 . . . . 5 (𝜑 → ((𝑥𝐴𝐶) ∈ MblFn ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐶)), (ℜ‘𝐶), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐶)), -(ℜ‘𝐶), 0))) ∈ ℝ) ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐶)), (ℑ‘𝐶), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐶)), -(ℑ‘𝐶), 0))) ∈ ℝ)))
2221simp1d 1137 . . . 4 (𝜑 → (𝑥𝐴𝐶) ∈ MblFn)
239, 22mbfadd 23627 . . 3 (𝜑 → ((𝑥𝐴𝐵) ∘𝑓 + (𝑥𝐴𝐶)) ∈ MblFn)
2414, 23eqeltrrd 2840 . 2 (𝜑 → (𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)
259, 6mbfmptcl 23603 . . . . 5 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
2625recld 14133 . . . 4 ((𝜑𝑥𝐴) → (ℜ‘𝐵) ∈ ℝ)
2722, 11mbfmptcl 23603 . . . . 5 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
2827recld 14133 . . . 4 ((𝜑𝑥𝐴) → (ℜ‘𝐶) ∈ ℝ)
2925, 27readdd 14153 . . . 4 ((𝜑𝑥𝐴) → (ℜ‘(𝐵 + 𝐶)) = ((ℜ‘𝐵) + (ℜ‘𝐶)))
3025ismbfcn2 23605 . . . . . 6 (𝜑 → ((𝑥𝐴𝐵) ∈ MblFn ↔ ((𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn ∧ (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)))
319, 30mpbid 222 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn ∧ (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn))
3231simpld 477 . . . 4 (𝜑 → (𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
3327ismbfcn2 23605 . . . . . 6 (𝜑 → ((𝑥𝐴𝐶) ∈ MblFn ↔ ((𝑥𝐴 ↦ (ℜ‘𝐶)) ∈ MblFn ∧ (𝑥𝐴 ↦ (ℑ‘𝐶)) ∈ MblFn)))
3422, 33mpbid 222 . . . . 5 (𝜑 → ((𝑥𝐴 ↦ (ℜ‘𝐶)) ∈ MblFn ∧ (𝑥𝐴 ↦ (ℑ‘𝐶)) ∈ MblFn))
3534simpld 477 . . . 4 (𝜑 → (𝑥𝐴 ↦ (ℜ‘𝐶)) ∈ MblFn)
368simp2d 1138 . . . . 5 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) ∈ ℝ))
3736simpld 477 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) ∈ ℝ)
3821simp2d 1138 . . . . 5 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐶)), (ℜ‘𝐶), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐶)), -(ℜ‘𝐶), 0))) ∈ ℝ))
3938simpld 477 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘𝐶)), (ℜ‘𝐶), 0))) ∈ ℝ)
4026, 28, 29, 32, 35, 37, 39ibladdlem 23785 . . 3 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 + 𝐶))), (ℜ‘(𝐵 + 𝐶)), 0))) ∈ ℝ)
4126renegcld 10649 . . . 4 ((𝜑𝑥𝐴) → -(ℜ‘𝐵) ∈ ℝ)
4228renegcld 10649 . . . 4 ((𝜑𝑥𝐴) → -(ℜ‘𝐶) ∈ ℝ)
4329negeqd 10467 . . . . 5 ((𝜑𝑥𝐴) → -(ℜ‘(𝐵 + 𝐶)) = -((ℜ‘𝐵) + (ℜ‘𝐶)))
4426recnd 10260 . . . . . 6 ((𝜑𝑥𝐴) → (ℜ‘𝐵) ∈ ℂ)
4528recnd 10260 . . . . . 6 ((𝜑𝑥𝐴) → (ℜ‘𝐶) ∈ ℂ)
4644, 45negdid 10597 . . . . 5 ((𝜑𝑥𝐴) → -((ℜ‘𝐵) + (ℜ‘𝐶)) = (-(ℜ‘𝐵) + -(ℜ‘𝐶)))
4743, 46eqtrd 2794 . . . 4 ((𝜑𝑥𝐴) → -(ℜ‘(𝐵 + 𝐶)) = (-(ℜ‘𝐵) + -(ℜ‘𝐶)))
4826, 32mbfneg 23616 . . . 4 (𝜑 → (𝑥𝐴 ↦ -(ℜ‘𝐵)) ∈ MblFn)
4928, 35mbfneg 23616 . . . 4 (𝜑 → (𝑥𝐴 ↦ -(ℜ‘𝐶)) ∈ MblFn)
5036simprd 482 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) ∈ ℝ)
5138simprd 482 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘𝐶)), -(ℜ‘𝐶), 0))) ∈ ℝ)
5241, 42, 47, 48, 49, 50, 51ibladdlem 23785 . . 3 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘(𝐵 + 𝐶))), -(ℜ‘(𝐵 + 𝐶)), 0))) ∈ ℝ)
5340, 52jca 555 . 2 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 + 𝐶))), (ℜ‘(𝐵 + 𝐶)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘(𝐵 + 𝐶))), -(ℜ‘(𝐵 + 𝐶)), 0))) ∈ ℝ))
5425imcld 14134 . . . 4 ((𝜑𝑥𝐴) → (ℑ‘𝐵) ∈ ℝ)
5527imcld 14134 . . . 4 ((𝜑𝑥𝐴) → (ℑ‘𝐶) ∈ ℝ)
5625, 27imaddd 14154 . . . 4 ((𝜑𝑥𝐴) → (ℑ‘(𝐵 + 𝐶)) = ((ℑ‘𝐵) + (ℑ‘𝐶)))
5731simprd 482 . . . 4 (𝜑 → (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
5834simprd 482 . . . 4 (𝜑 → (𝑥𝐴 ↦ (ℑ‘𝐶)) ∈ MblFn)
598simp3d 1139 . . . . 5 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) ∈ ℝ))
6059simpld 477 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) ∈ ℝ)
6121simp3d 1139 . . . . 5 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐶)), (ℑ‘𝐶), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐶)), -(ℑ‘𝐶), 0))) ∈ ℝ))
6261simpld 477 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘𝐶)), (ℑ‘𝐶), 0))) ∈ ℝ)
6354, 55, 56, 57, 58, 60, 62ibladdlem 23785 . . 3 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘(𝐵 + 𝐶))), (ℑ‘(𝐵 + 𝐶)), 0))) ∈ ℝ)
6454renegcld 10649 . . . 4 ((𝜑𝑥𝐴) → -(ℑ‘𝐵) ∈ ℝ)
6555renegcld 10649 . . . 4 ((𝜑𝑥𝐴) → -(ℑ‘𝐶) ∈ ℝ)
6656negeqd 10467 . . . . 5 ((𝜑𝑥𝐴) → -(ℑ‘(𝐵 + 𝐶)) = -((ℑ‘𝐵) + (ℑ‘𝐶)))
6754recnd 10260 . . . . . 6 ((𝜑𝑥𝐴) → (ℑ‘𝐵) ∈ ℂ)
6855recnd 10260 . . . . . 6 ((𝜑𝑥𝐴) → (ℑ‘𝐶) ∈ ℂ)
6967, 68negdid 10597 . . . . 5 ((𝜑𝑥𝐴) → -((ℑ‘𝐵) + (ℑ‘𝐶)) = (-(ℑ‘𝐵) + -(ℑ‘𝐶)))
7066, 69eqtrd 2794 . . . 4 ((𝜑𝑥𝐴) → -(ℑ‘(𝐵 + 𝐶)) = (-(ℑ‘𝐵) + -(ℑ‘𝐶)))
7154, 57mbfneg 23616 . . . 4 (𝜑 → (𝑥𝐴 ↦ -(ℑ‘𝐵)) ∈ MblFn)
7255, 58mbfneg 23616 . . . 4 (𝜑 → (𝑥𝐴 ↦ -(ℑ‘𝐶)) ∈ MblFn)
7359simprd 482 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) ∈ ℝ)
7461simprd 482 . . . 4 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘𝐶)), -(ℑ‘𝐶), 0))) ∈ ℝ)
7564, 65, 70, 71, 72, 73, 74ibladdlem 23785 . . 3 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘(𝐵 + 𝐶))), -(ℑ‘(𝐵 + 𝐶)), 0))) ∈ ℝ)
7663, 75jca 555 . 2 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘(𝐵 + 𝐶))), (ℑ‘(𝐵 + 𝐶)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘(𝐵 + 𝐶))), -(ℑ‘(𝐵 + 𝐶)), 0))) ∈ ℝ))
77 eqid 2760 . . 3 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 + 𝐶))), (ℜ‘(𝐵 + 𝐶)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 + 𝐶))), (ℜ‘(𝐵 + 𝐶)), 0)))
78 eqid 2760 . . 3 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘(𝐵 + 𝐶))), -(ℜ‘(𝐵 + 𝐶)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘(𝐵 + 𝐶))), -(ℜ‘(𝐵 + 𝐶)), 0)))
79 eqid 2760 . . 3 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘(𝐵 + 𝐶))), (ℑ‘(𝐵 + 𝐶)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘(𝐵 + 𝐶))), (ℑ‘(𝐵 + 𝐶)), 0)))
80 eqid 2760 . . 3 (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘(𝐵 + 𝐶))), -(ℑ‘(𝐵 + 𝐶)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘(𝐵 + 𝐶))), -(ℑ‘(𝐵 + 𝐶)), 0)))
81 ovexd 6843 . . 3 ((𝜑𝑥𝐴) → (𝐵 + 𝐶) ∈ V)
8277, 78, 79, 80, 81iblcnlem 23754 . 2 (𝜑 → ((𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1 ↔ ((𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘(𝐵 + 𝐶))), (ℜ‘(𝐵 + 𝐶)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℜ‘(𝐵 + 𝐶))), -(ℜ‘(𝐵 + 𝐶)), 0))) ∈ ℝ) ∧ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℑ‘(𝐵 + 𝐶))), (ℑ‘(𝐵 + 𝐶)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(ℑ‘(𝐵 + 𝐶))), -(ℑ‘(𝐵 + 𝐶)), 0))) ∈ ℝ))))
8324, 53, 76, 82mpbir3and 1428 1 (𝜑 → (𝑥𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1)