Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anclem6 Structured version   Visualization version   GIF version

Theorem ftc1anclem6 36011
Description: Lemma for ftc1anc 36014- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued 𝐹. (Contributed by Brendan Leahy, 31-May-2018.)
Hypotheses
Ref Expression
ftc1anc.g 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
ftc1anc.a (𝜑𝐴 ∈ ℝ)
ftc1anc.b (𝜑𝐵 ∈ ℝ)
ftc1anc.le (𝜑𝐴𝐵)
ftc1anc.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1anc.d (𝜑𝐷 ⊆ ℝ)
ftc1anc.i (𝜑𝐹 ∈ 𝐿1)
ftc1anc.f (𝜑𝐹:𝐷⟶ℂ)
Assertion
Ref Expression
ftc1anclem6 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌)
Distinct variable groups:   𝑓,𝑔,𝑡,𝑥,𝐴   𝐵,𝑓,𝑔,𝑡,𝑥   𝐷,𝑓,𝑔,𝑡,𝑥   𝑓,𝐹,𝑔,𝑡,𝑥   𝜑,𝑓,𝑔,𝑡,𝑥   𝑓,𝐺,𝑔   𝑓,𝑌,𝑔,𝑡,𝑥
Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anclem6
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 rphalfcl 12862 . . 3 (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ+)
2 ftc1anc.g . . . 4 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
3 ftc1anc.a . . . 4 (𝜑𝐴 ∈ ℝ)
4 ftc1anc.b . . . 4 (𝜑𝐵 ∈ ℝ)
5 ftc1anc.le . . . 4 (𝜑𝐴𝐵)
6 ftc1anc.s . . . 4 (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
7 ftc1anc.d . . . 4 (𝜑𝐷 ⊆ ℝ)
8 ftc1anc.i . . . 4 (𝜑𝐹 ∈ 𝐿1)
9 ftc1anc.f . . . 4 (𝜑𝐹:𝐷⟶ℂ)
102, 3, 4, 5, 6, 7, 8, 9ftc1anclem5 36010 . . 3 ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2))
111, 10sylan2 594 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2))
12 eqid 2737 . . . . 5 (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) d𝑡)
13 ax-icn 11035 . . . . . . . 8 i ∈ ℂ
14 ine0 11515 . . . . . . . 8 i ≠ 0
1513, 14reccli 11810 . . . . . . 7 (1 / i) ∈ ℂ
1615a1i 11 . . . . . 6 (𝜑 → (1 / i) ∈ ℂ)
179ffvelcdmda 7021 . . . . . 6 ((𝜑𝑦𝐷) → (𝐹𝑦) ∈ ℂ)
189feqmptd 6897 . . . . . . 7 (𝜑𝐹 = (𝑦𝐷 ↦ (𝐹𝑦)))
1918, 8eqeltrrd 2839 . . . . . 6 (𝜑 → (𝑦𝐷 ↦ (𝐹𝑦)) ∈ 𝐿1)
20 divrec2 11755 . . . . . . . . . 10 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹𝑦) / i) = ((1 / i) · (𝐹𝑦)))
2113, 14, 20mp3an23 1453 . . . . . . . . 9 ((𝐹𝑦) ∈ ℂ → ((𝐹𝑦) / i) = ((1 / i) · (𝐹𝑦)))
2217, 21syl 17 . . . . . . . 8 ((𝜑𝑦𝐷) → ((𝐹𝑦) / i) = ((1 / i) · (𝐹𝑦)))
2322mpteq2dva 5196 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ ((𝐹𝑦) / i)) = (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))))
24 iblmbf 25037 . . . . . . . . 9 ((𝑦𝐷 ↦ (𝐹𝑦)) ∈ 𝐿1 → (𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn)
2519, 24syl 17 . . . . . . . 8 (𝜑 → (𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn)
26 2fveq3 6834 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (ℜ‘(𝐹𝑦)) = (ℜ‘(𝐹𝑥)))
2726cbvmptv 5209 . . . . . . . . . . . . . . 15 (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) = (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥)))
2827eleq1i 2828 . . . . . . . . . . . . . 14 ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn)
2917recld 15004 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐷) → (ℜ‘(𝐹𝑦)) ∈ ℝ)
3029recnd 11108 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐷) → (ℜ‘(𝐹𝑦)) ∈ ℂ)
3130adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn) ∧ 𝑦𝐷) → (ℜ‘(𝐹𝑦)) ∈ ℂ)
3228biimpri 227 . . . . . . . . . . . . . . . 16 ((𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn → (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn)
3332adantl 483 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn) → (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn)
3431, 33mbfneg 24919 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn) → (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn)
3528, 34sylan2b 595 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn)
369ffvelcdmda 7021 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐷) → (𝐹𝑥) ∈ ℂ)
3736recld 15004 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐷) → (ℜ‘(𝐹𝑥)) ∈ ℝ)
3837recnd 11108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → (ℜ‘(𝐹𝑥)) ∈ ℂ)
3938negnegd 11428 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → --(ℜ‘(𝐹𝑥)) = (ℜ‘(𝐹𝑥)))
4039mpteq2dva 5196 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) = (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))))
4140, 27eqtr4di 2795 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) = (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))))
4241adantr 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) = (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))))
43 negex 11324 . . . . . . . . . . . . . . . 16 -(ℜ‘(𝐹𝑥)) ∈ V
4443a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) ∧ 𝑥𝐷) → -(ℜ‘(𝐹𝑥)) ∈ V)
4526negeqd 11320 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → -(ℜ‘(𝐹𝑦)) = -(ℜ‘(𝐹𝑥)))
4645cbvmptv 5209 . . . . . . . . . . . . . . . . . 18 (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) = (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥)))
4746eleq1i 2828 . . . . . . . . . . . . . . . . 17 ((𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥))) ∈ MblFn)
4847biimpi 215 . . . . . . . . . . . . . . . 16 ((𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn → (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥))) ∈ MblFn)
4948adantl 483 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥))) ∈ MblFn)
5044, 49mbfneg 24919 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) ∈ MblFn)
5142, 50eqeltrrd 2839 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn)
5235, 51impbida 799 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn))
53 divcl 11744 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹𝑦) / i) ∈ ℂ)
54 imre 14918 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑦) / i) ∈ ℂ → (ℑ‘((𝐹𝑦) / i)) = (ℜ‘(-i · ((𝐹𝑦) / i))))
5553, 54syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (ℑ‘((𝐹𝑦) / i)) = (ℜ‘(-i · ((𝐹𝑦) / i))))
5613, 14, 55mp3an23 1453 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ ℂ → (ℑ‘((𝐹𝑦) / i)) = (ℜ‘(-i · ((𝐹𝑦) / i))))
5713, 14, 53mp3an23 1453 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ ℂ → ((𝐹𝑦) / i) ∈ ℂ)
58 mulneg1 11516 . . . . . . . . . . . . . . . . . . 19 ((i ∈ ℂ ∧ ((𝐹𝑦) / i) ∈ ℂ) → (-i · ((𝐹𝑦) / i)) = -(i · ((𝐹𝑦) / i)))
5913, 57, 58sylancr 588 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ ℂ → (-i · ((𝐹𝑦) / i)) = -(i · ((𝐹𝑦) / i)))
60 divcan2 11746 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (i · ((𝐹𝑦) / i)) = (𝐹𝑦))
6113, 14, 60mp3an23 1453 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ ℂ → (i · ((𝐹𝑦) / i)) = (𝐹𝑦))
6261negeqd 11320 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ ℂ → -(i · ((𝐹𝑦) / i)) = -(𝐹𝑦))
6359, 62eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((𝐹𝑦) ∈ ℂ → (-i · ((𝐹𝑦) / i)) = -(𝐹𝑦))
6463fveq2d 6833 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ ℂ → (ℜ‘(-i · ((𝐹𝑦) / i))) = (ℜ‘-(𝐹𝑦)))
65 reneg 14935 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ ℂ → (ℜ‘-(𝐹𝑦)) = -(ℜ‘(𝐹𝑦)))
6656, 64, 653eqtrd 2781 . . . . . . . . . . . . . . 15 ((𝐹𝑦) ∈ ℂ → (ℑ‘((𝐹𝑦) / i)) = -(ℜ‘(𝐹𝑦)))
6717, 66syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐷) → (ℑ‘((𝐹𝑦) / i)) = -(ℜ‘(𝐹𝑦)))
6867mpteq2dva 5196 . . . . . . . . . . . . 13 (𝜑 → (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) = (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))))
6968eleq1d 2822 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn ↔ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn))
7052, 69bitr4d 282 . . . . . . . . . . 11 (𝜑 → ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn))
71 imval 14917 . . . . . . . . . . . . . 14 ((𝐹𝑦) ∈ ℂ → (ℑ‘(𝐹𝑦)) = (ℜ‘((𝐹𝑦) / i)))
7217, 71syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝐷) → (ℑ‘(𝐹𝑦)) = (ℜ‘((𝐹𝑦) / i)))
7372mpteq2dva 5196 . . . . . . . . . . . 12 (𝜑 → (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) = (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))))
7473eleq1d 2822 . . . . . . . . . . 11 (𝜑 → ((𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn))
7570, 74anbi12d 632 . . . . . . . . . 10 (𝜑 → (((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn) ↔ ((𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn)))
76 ancom 462 . . . . . . . . . 10 (((𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn) ↔ ((𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn))
7775, 76bitrdi 287 . . . . . . . . 9 (𝜑 → (((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn) ↔ ((𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn)))
7817ismbfcn2 24907 . . . . . . . . 9 (𝜑 → ((𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn ↔ ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn)))
7917, 57syl 17 . . . . . . . . . 10 ((𝜑𝑦𝐷) → ((𝐹𝑦) / i) ∈ ℂ)
8079ismbfcn2 24907 . . . . . . . . 9 (𝜑 → ((𝑦𝐷 ↦ ((𝐹𝑦) / i)) ∈ MblFn ↔ ((𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn)))
8177, 78, 803bitr4d 311 . . . . . . . 8 (𝜑 → ((𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn ↔ (𝑦𝐷 ↦ ((𝐹𝑦) / i)) ∈ MblFn))
8225, 81mpbid 231 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ ((𝐹𝑦) / i)) ∈ MblFn)
8323, 82eqeltrrd 2839 . . . . . 6 (𝜑 → (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))) ∈ MblFn)
8416, 17, 19, 83iblmulc2nc 35998 . . . . 5 (𝜑 → (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))) ∈ 𝐿1)
85 mulcl 11060 . . . . . . 7 (((1 / i) ∈ ℂ ∧ (𝐹𝑦) ∈ ℂ) → ((1 / i) · (𝐹𝑦)) ∈ ℂ)
8615, 17, 85sylancr 588 . . . . . 6 ((𝜑𝑦𝐷) → ((1 / i) · (𝐹𝑦)) ∈ ℂ)
8786fmpttd 7049 . . . . 5 (𝜑 → (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))):𝐷⟶ℂ)
8812, 3, 4, 5, 6, 7, 84, 87ftc1anclem5 36010 . . . 4 ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2))
891, 88sylan2 594 . . 3 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2))
909ffvelcdmda 7021 . . . . . . . . . . . 12 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
91 0cnd 11073 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
9290, 91ifclda 4512 . . . . . . . . . . 11 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
93 imval 14917 . . . . . . . . . . 11 (if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(if(𝑡𝐷, (𝐹𝑡), 0) / i)))
9492, 93syl 17 . . . . . . . . . 10 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(if(𝑡𝐷, (𝐹𝑡), 0) / i)))
95 fveq2 6829 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑡 → (𝐹𝑦) = (𝐹𝑡))
9695oveq2d 7357 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑡 → ((1 / i) · (𝐹𝑦)) = ((1 / i) · (𝐹𝑡)))
97 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))) = (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))
98 ovex 7374 . . . . . . . . . . . . . . . 16 ((1 / i) · (𝐹𝑡)) ∈ V
9996, 97, 98fvmpt 6935 . . . . . . . . . . . . . . 15 (𝑡𝐷 → ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) = ((1 / i) · (𝐹𝑡)))
10099adantl 483 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐷) → ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) = ((1 / i) · (𝐹𝑡)))
101 divrec2 11755 . . . . . . . . . . . . . . . 16 (((𝐹𝑡) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹𝑡) / i) = ((1 / i) · (𝐹𝑡)))
10213, 14, 101mp3an23 1453 . . . . . . . . . . . . . . 15 ((𝐹𝑡) ∈ ℂ → ((𝐹𝑡) / i) = ((1 / i) · (𝐹𝑡)))
10390, 102syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐷) → ((𝐹𝑡) / i) = ((1 / i) · (𝐹𝑡)))
104100, 103eqtr4d 2780 . . . . . . . . . . . . 13 ((𝜑𝑡𝐷) → ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) = ((𝐹𝑡) / i))
105104ifeq1da 4508 . . . . . . . . . . . 12 (𝜑 → if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0) = if(𝑡𝐷, ((𝐹𝑡) / i), 0))
106 ovif 7438 . . . . . . . . . . . . 13 (if(𝑡𝐷, (𝐹𝑡), 0) / i) = if(𝑡𝐷, ((𝐹𝑡) / i), (0 / i))
10713, 14div0i 11814 . . . . . . . . . . . . . 14 (0 / i) = 0
108 ifeq2 4482 . . . . . . . . . . . . . 14 ((0 / i) = 0 → if(𝑡𝐷, ((𝐹𝑡) / i), (0 / i)) = if(𝑡𝐷, ((𝐹𝑡) / i), 0))
109107, 108ax-mp 5 . . . . . . . . . . . . 13 if(𝑡𝐷, ((𝐹𝑡) / i), (0 / i)) = if(𝑡𝐷, ((𝐹𝑡) / i), 0)
110106, 109eqtri 2765 . . . . . . . . . . . 12 (if(𝑡𝐷, (𝐹𝑡), 0) / i) = if(𝑡𝐷, ((𝐹𝑡) / i), 0)
111105, 110eqtr4di 2795 . . . . . . . . . . 11 (𝜑 → if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0) = (if(𝑡𝐷, (𝐹𝑡), 0) / i))
112111fveq2d 6833 . . . . . . . . . 10 (𝜑 → (ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡𝐷, (𝐹𝑡), 0) / i)))
11394, 112eqtr4d 2780 . . . . . . . . 9 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)))
114113fvoveq1d 7363 . . . . . . . 8 (𝜑 → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))
115114mpteq2dv 5198 . . . . . . 7 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡)))))
116115fveq2d 6833 . . . . . 6 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))))
117116breq1d 5106 . . . . 5 (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
118117rexbidv 3172 . . . 4 (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
119118adantr 482 . . 3 ((𝜑𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
12089, 119mpbird 257 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2))
121 reeanv 3214 . . 3 (∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) ↔ (∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
122 eleq1w 2820 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (𝑥𝐷𝑡𝐷))
123 fveq2 6829 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
124122, 123ifbieq1d 4501 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → if(𝑥𝐷, (𝐹𝑥), 0) = if(𝑡𝐷, (𝐹𝑡), 0))
125124fveq2d 6833 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
126 eqid 2737 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))
127 fvex 6842 . . . . . . . . . . . . . 14 (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
128125, 126, 127fvmpt 6935 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
129128fvoveq1d 7363 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
130129mpteq2ia 5199 . . . . . . . . . . 11 (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
131130fveq2i 6832 . . . . . . . . . 10 (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
132 rembl 24809 . . . . . . . . . . . . . . . . 17 ℝ ∈ dom vol
133132a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℝ ∈ dom vol)
134 0cnd 11073 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝑥𝐷) → 0 ∈ ℂ)
13536, 134ifclda 4512 . . . . . . . . . . . . . . . . 17 (𝜑 → if(𝑥𝐷, (𝐹𝑥), 0) ∈ ℂ)
136135adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐷) → if(𝑥𝐷, (𝐹𝑥), 0) ∈ ℂ)
137 eldifn 4078 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥𝐷)
138137adantl 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥𝐷)
139138iffalsed 4488 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥𝐷, (𝐹𝑥), 0) = 0)
1409feqmptd 6897 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥𝐷 ↦ (𝐹𝑥)))
141 iftrue 4483 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐷 → if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥))
142141mpteq2ia 5199 . . . . . . . . . . . . . . . . . 18 (𝑥𝐷 ↦ if(𝑥𝐷, (𝐹𝑥), 0)) = (𝑥𝐷 ↦ (𝐹𝑥))
143140, 142eqtr4di 2795 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 = (𝑥𝐷 ↦ if(𝑥𝐷, (𝐹𝑥), 0)))
144143, 8eqeltrrd 2839 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝐷 ↦ if(𝑥𝐷, (𝐹𝑥), 0)) ∈ 𝐿1)
1457, 133, 136, 139, 144iblss2 25075 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐷, (𝐹𝑥), 0)) ∈ 𝐿1)
146135adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐷, (𝐹𝑥), 0) ∈ ℂ)
147146iblcn 25068 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐷, (𝐹𝑥), 0)) ∈ 𝐿1 ↔ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)))
148145, 147mpbid 231 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1))
149148simpld 496 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
150146recld 15004 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ∈ ℝ)
151150fmpttd 7049 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
152149, 151jca 513 . . . . . . . . . . . 12 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
153 ftc1anclem4 36009 . . . . . . . . . . . . 13 ((𝑓 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
1541533expb 1120 . . . . . . . . . . . 12 ((𝑓 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
155152, 154sylan2 594 . . . . . . . . . . 11 ((𝑓 ∈ dom ∫1𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
156155ancoms 460 . . . . . . . . . 10 ((𝜑𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
157131, 156eqeltrrid 2843 . . . . . . . . 9 ((𝜑𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ)
158124fveq2d 6833 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))
159 eqid 2737 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))
160 fvex 6842 . . . . . . . . . . . . . 14 (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
161158, 159, 160fvmpt 6935 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))
162161fvoveq1d 7363 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))) = (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
163162mpteq2ia 5199 . . . . . . . . . . 11 (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
164163fveq2i 6832 . . . . . . . . . 10 (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
165148simprd 497 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
166135imcld 15005 . . . . . . . . . . . . . . 15 (𝜑 → (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)) ∈ ℝ)
167166adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)) ∈ ℝ)
168167fmpttd 7049 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
169165, 168jca 513 . . . . . . . . . . . 12 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
170 ftc1anclem4 36009 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
1711703expb 1120 . . . . . . . . . . . 12 ((𝑔 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
172169, 171sylan2 594 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
173172ancoms 460 . . . . . . . . . 10 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
174164, 173eqeltrrid 2843 . . . . . . . . 9 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ)
175157, 174anim12dan 620 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ))
1761rpred 12877 . . . . . . . . 9 (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ)
177176, 176jca 513 . . . . . . . 8 (𝑌 ∈ ℝ+ → ((𝑌 / 2) ∈ ℝ ∧ (𝑌 / 2) ∈ ℝ))
178 lt2add 11565 . . . . . . . 8 ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ) ∧ ((𝑌 / 2) ∈ ℝ ∧ (𝑌 / 2) ∈ ℝ)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))))
179175, 177, 178syl2an 597 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))))
180179an32s 650 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))))
18192recld 15004 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
182181recnd 11108 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
183 i1ff 24945 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
184183ffvelcdmda 7021 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
185184recnd 11108 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
186 subcl 11325 . . . . . . . . . . . . . . . . . 18 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (𝑓𝑡) ∈ ℂ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
187182, 185, 186syl2an 597 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
188187anassrs 469 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
189188adantlrr 719 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
19092imcld 15005 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
191190recnd 11108 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
192 i1ff 24945 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
193192ffvelcdmda 7021 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
194193recnd 11108 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
195 subcl 11325 . . . . . . . . . . . . . . . . . . 19 (((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ)
196191, 194, 195syl2an 597 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ)
197196anassrs 469 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ)
198 mulcl 11060 . . . . . . . . . . . . . . . . 17 ((i ∈ ℂ ∧ ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
19913, 197, 198sylancr 588 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
200199adantlrl 718 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
201189, 200addcld 11099 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) ∈ ℂ)
202201abscld 15247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ)
203202rexrd 11130 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ*)
204201absge0d 15255 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
205 elxrge0 13294 . . . . . . . . . . . 12 ((abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
206203, 204, 205sylanbrc 584 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ (0[,]+∞))
207206fmpttd 7049 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))):ℝ⟶(0[,]+∞))
208 icossicc 13273 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
209 ge0addcl 13297 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
210208, 209sselid 3933 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,]+∞))
211210adantl 483 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞))
212188abscld 15247 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ ℝ)
213188absge0d 15255 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
214 elrege0 13291 . . . . . . . . . . . . . 14 ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
215212, 213, 214sylanbrc 584 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ (0[,)+∞))
216215fmpttd 7049 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))):ℝ⟶(0[,)+∞))
217216adantrr 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))):ℝ⟶(0[,)+∞))
218197abscld 15247 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℝ)
219197absge0d 15255 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
220 elrege0 13291 . . . . . . . . . . . . . 14 ((abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
221218, 219, 220sylanbrc 584 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ (0[,)+∞))
222221fmpttd 7049 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))):ℝ⟶(0[,)+∞))
223222adantrl 714 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))):ℝ⟶(0[,)+∞))
224 reex 11067 . . . . . . . . . . . 12 ℝ ∈ V
225224a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ℝ ∈ V)
226 inidm 4169 . . . . . . . . . . 11 (ℝ ∩ ℝ) = ℝ
227211, 217, 223, 225, 225, 226off 7617 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))):ℝ⟶(0[,]+∞))
228189, 200abstrid 15267 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
229228ralrimiva 3140 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
230 ovexd 7376 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ V)
231 eqidd 2738 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
232 fvexd 6844 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ V)
233 fvexd 6844 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) ∈ V)
234 eqidd 2738 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
235 absmul 15105 . . . . . . . . . . . . . . . . 17 ((i ∈ ℂ ∧ ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ) → (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
23613, 197, 235sylancr 588 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
237 absi 15097 . . . . . . . . . . . . . . . . . 18 (abs‘i) = 1
238237oveq1i 7351 . . . . . . . . . . . . . . . . 17 ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (1 · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
239218recnd 11108 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
240239mulid2d 11098 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1 · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
241238, 240eqtrid 2789 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
242236, 241eqtr2d 2778 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
243242mpteq2dva 5196 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
244243adantrl 714 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
245225, 232, 233, 234, 244offval2 7619 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) = (𝑡 ∈ ℝ ↦ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
246225, 202, 230, 231, 245ofrfval2 7620 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∘r ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ↔ ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
247229, 246mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∘r ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
248 itg2le 25009 . . . . . . . . . 10 (((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))):ℝ⟶(0[,]+∞) ∧ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∘r ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
249207, 227, 247, 248syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
250 absf 15148 . . . . . . . . . . . . . 14 abs:ℂ⟶ℝ
251250a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑓 ∈ dom ∫1) → abs:ℂ⟶ℝ)
252251, 188cofmpt 7064 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
253 resubcl 11390 . . . . . . . . . . . . . . . 16 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑓𝑡) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℝ)
254181, 184, 253syl2an 597 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℝ)
255254anassrs 469 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℝ)
256255fmpttd 7049 . . . . . . . . . . . . 13 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))):ℝ⟶ℝ)
257132a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ dom ∫1) → ℝ ∈ dom vol)
258 iunin2 5022 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦}))
259 imaiun 7178 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 𝑦 ∈ ran 𝑓{𝑦}) = 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦})
260 iunid 5011 . . . . . . . . . . . . . . . . . . . . . 22 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓
261260imaeq2i 6001 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 𝑦 ∈ ran 𝑓{𝑦}) = (𝑓 “ ran 𝑓)
262259, 261eqtr3i 2767 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦}) = (𝑓 “ ran 𝑓)
263262ineq2i 4160 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓))
264258, 263eqtri 2765 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓))
265 cnvimass 6023 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
266 ovex 7374 . . . . . . . . . . . . . . . . . . . . . 22 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ V
267 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) = (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
268266, 267dmmpti 6632 . . . . . . . . . . . . . . . . . . . . 21 dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) = ℝ
269265, 268sseqtri 3971 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ ℝ
270 cnvimarndm 6024 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 “ ran 𝑓) = dom 𝑓
271183fdmd 6666 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ)
272270, 271eqtrid 2789 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (𝑓 “ ran 𝑓) = ℝ)
273269, 272sseqtrrid 3988 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ (𝑓 “ ran 𝑓))
274 df-ss 3918 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ (𝑓 “ ran 𝑓) ↔ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
275273, 274sylib 217 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
276264, 275eqtrid 2789 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
277276ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
278183frnd 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
279278ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran 𝑓 ⊆ ℝ)
280279sselda 3935 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ)
281181ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
282 resubcl 11390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ)
283181, 282sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ)
284283adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ)
285281, 2842thd 265 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ))
286 ltaddsub 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
287181, 286syl3an3 1165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
2882873comr 1125 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
2892883expa 1118 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
290285, 289anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))))
291 readdcl 11059 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
292291rexrd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
293292adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
294 elioopnf 13280 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
295293, 294syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
296 rexr 11126 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
297296ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*)
298 elioopnf 13280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))))
299297, 298syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))))
300290, 295, 2993bitr4rd 312 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))
301 oveq2 7349 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑡) = 𝑦 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))
302301eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞)))
303302bibi1d 344 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑡) = 𝑦 → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
304300, 303syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
305304pm5.32rd 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)))
306305adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)))
307280, 306syldan 592 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)))
308307rabbidv 3412 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
309183feqmptd 6897 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓 = (𝑡 ∈ ℝ ↦ (𝑓𝑡)))
310309cnveqd 5821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∈ dom ∫1𝑓 = (𝑡 ∈ ℝ ↦ (𝑓𝑡)))
311310imaeq1d 6002 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1 → (𝑓 “ {𝑦}) = ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦}))
312311ineq2d 4163 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
313267mptpreima 6180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞)}
314 vex 3446 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦 ∈ V
315 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ ℝ ↦ (𝑓𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓𝑡))
316315mptiniseg 6181 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ V → ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
317314, 316ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}
318313, 317ineq12i 4161 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
319 inrab 4257 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
320318, 319eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
321312, 320eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
322321ad3antlr 729 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
323311ineq2d 4163 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
324 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
325324mptpreima 6180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)}
326325, 317ineq12i 4161 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
327 inrab 4257 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
328326, 327eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
329323, 328eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
330329ad3antlr 729 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
331308, 322, 3303eqtr4d 2787 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})))
332331iuneq2dv 4969 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})))
333277, 332eqtr3d 2779 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})))
334 i1frn 24946 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
335334adantl 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → ran 𝑓 ∈ Fin)
33692adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡𝐷) → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
337 eldifn 4078 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡𝐷)
338337adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡𝐷)
339338iffalsed 4488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡𝐷, (𝐹𝑡), 0) = 0)
3409feqmptd 6897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
341 iftrue 4483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
342341mpteq2ia 5199 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡𝐷 ↦ if(𝑡𝐷, (𝐹𝑡), 0)) = (𝑡𝐷 ↦ (𝐹𝑡))
343340, 342eqtr4di 2795 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 = (𝑡𝐷 ↦ if(𝑡𝐷, (𝐹𝑡), 0)))
344 iblmbf 25037 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
3458, 344syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 ∈ MblFn)
346343, 345eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡𝐷 ↦ if(𝑡𝐷, (𝐹𝑡), 0)) ∈ MblFn)
3477, 133, 336, 339, 346mbfss 24915 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (𝐹𝑡), 0)) ∈ MblFn)
34892adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
349348ismbfcn2 24907 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡𝐷, (𝐹𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)))
350347, 349mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn))
351350simpld 496 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
352181adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
353352fmpttd 7049 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ)
354 mbfima 24899 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
355351, 353, 354syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
356 i1fima 24947 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (𝑓 “ {𝑦}) ∈ dom vol)
357 inmbl 24811 . . . . . . . . . . . . . . . . . . 19 ((((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (𝑓 “ {𝑦}) ∈ dom vol) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
358355, 356, 357syl2an 597 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
359358ralrimivw 3144 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
360 finiunmbl 24813 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
361335, 359, 360syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
362361adantr 482 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
363333, 362eqeltrd 2838 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∈ dom vol)
364 iunin2 5022 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦}))
365262ineq2i 4160 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓))
366364, 365eqtri 2765 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓))
367 cnvimass 6023 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
368367, 268sseqtri 3971 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ
369368, 272sseqtrrid 3988 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ (𝑓 “ ran 𝑓))
370 df-ss 3918 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ (𝑓 “ ran 𝑓) ↔ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
371369, 370sylib 217 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
372366, 371eqtrid 2789 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
373372ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
374284, 2812thd 265 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ))
375 ltsubadd 11550 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
376181, 375syl3an1 1163 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
3773763expa 1118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
378377an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
379374, 378anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦))))
380 elioomnf 13281 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥)))
381297, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥)))
382 elioomnf 13281 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦))))
383293, 382syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦))))
384379, 381, 3833bitr4d 311 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))
385301eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥)))
386385bibi1d 344 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑡) = 𝑦 → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
387384, 386syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
388387pm5.32rd 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)))
389388adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)))
390280, 389syldan 592 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)))
391390rabbidv 3412 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)})
392311ineq2d 4163 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
393267mptpreima 6180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥)}
394393, 317ineq12i 4161 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
395 inrab 4257 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)}
396394, 395eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)}
397392, 396eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)})
398397ad3antlr 729 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)})
399311ineq2d 4163 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
400324mptpreima 6180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))}
401400, 317ineq12i 4161 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
402 inrab 4257 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)}
403401, 402eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)}
404399, 403eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)})
405404ad3antlr 729 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)})
406391, 398, 4053eqtr4d 2787 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})))
407406iuneq2dv 4969 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})))
408373, 407eqtr3d 2779 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})))
409 mbfima 24899 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
410351, 353, 409syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
411 inmbl 24811 . . . . . . . . . . . . . . . . . . 19 ((((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (𝑓 “ {𝑦}) ∈ dom vol) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
412410, 356, 411syl2an 597 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
413412ralrimivw 3144 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
414 finiunmbl 24813 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
415335, 413, 414syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
416415adantr 482 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
417408, 416eqeltrd 2838 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∈ dom vol)
418256, 257, 363, 417ismbf2d 24909 . . . . . . . . . . . . 13 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ MblFn)
419 ftc1anclem1 36006 . . . . . . . . . . . . 13 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
420256, 418, 419syl2anc 585 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
421252, 420eqeltrrd 2839 . . . . . . . . . . 11 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
422421adantrr 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
423157adantrr 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ)
424174adantrl 714 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ)
425422, 217, 423, 223, 424itg2addnc 35987 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
426249, 425breqtrd 5122 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
427426adantlr 713 . . . . . . 7 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
428 itg2cl 25002 . . . . . . . . . 10 ((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ*)
429207, 428syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ*)
430429adantlr 713 . . . . . . . 8 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ*)
431 readdcl 11059 . . . . . . . . . . . 12 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ)
432157, 174, 431syl2an 597 . . . . . . . . . . 11 (((𝜑𝑓 ∈ dom ∫1) ∧ (𝜑𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ)
433432anandis 676 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ)
434433rexrd 11130 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ*)
435434adantlr 713 . . . . . . . 8 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ*)
4361, 1rpaddcld 12892 . . . . . . . . . 10 (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ+)
437436rpxrd 12878 . . . . . . . . 9 (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
438437ad2antlr 725 . . . . . . . 8 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
439 xrlelttr 12995 . . . . . . . 8 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ* ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ* ∧ ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
440430, 435, 438, 439syl3anc 1371 . . . . . . 7 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
441427, 440mpand 693 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
442180, 441syld 47 . . . . 5 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
443 mulcl 11060 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ) → (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ)
44413, 191, 443sylancr 588 . . . . . . . . . . . . . 14 (𝜑 → (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ)
445182, 444jca 513 . . . . . . . . . . . . 13 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ))
446 mulcl 11060 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
44713, 194, 446sylancr 588 . . . . . . . . . . . . . . 15 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
448185, 447anim12i 614 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ))
449448anandirs 677 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ))
450 addsub4 11369 . . . . . . . . . . . . 13 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ) ∧ ((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
451445, 449, 450syl2an 597 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
452451anassrs 469 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
45392replimd 15007 . . . . . . . . . . . . 13 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
454453ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → if(𝑡𝐷, (𝐹𝑡), 0) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
455454oveq1d 7356 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))))
456194adantll 712 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
457 subdi 11513 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡))))
45813, 191, 456, 457mp3an3an 1467 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡))))
459458anassrs 469 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡))))
460459oveq2d 7357 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
461452, 455, 4603eqtr4rd 2788 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))
462461fveq2d 6833 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) = (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
463462mpteq2dva 5196 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
464463fveq2d 6833 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
465464adantlr 713 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
466 rpcn 12845 . . . . . . . 8 (𝑌 ∈ ℝ+𝑌 ∈ ℂ)
4674662halvesd 12324 . . . . . . 7 (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
468467ad2antlr 725 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
469465, 468breq12d 5109 . . . . 5 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
470442, 469sylibd 238 . . . 4 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
471470reximdvva 3199 . . 3 ((𝜑𝑌 ∈ ℝ+) → (∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
472121, 471syl5bir 243 . 2 ((𝜑𝑌 ∈ ℝ+) → ((∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
47311, 120, 472mp2and 697 1 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wcel 2106  wne 2941  wral 3062  wrex 3071  {crab 3404  Vcvv 3442  cdif 3898  cin 3900  wss 3901  ifcif 4477  {csn 4577   ciun 4945   class class class wbr 5096  cmpt 5179  ccnv 5623  dom cdm 5624  ran crn 5625  cima 5627  ccom 5628  wf 6479  cfv 6483  (class class class)co 7341  f cof 7597  r cofr 7598  Fincfn 8808  cc 10974  cr 10975  0cc0 10976  1c1 10977  ici 10978   + caddc 10979   · cmul 10981  +∞cpnf 11111  -∞cmnf 11112  *cxr 11113   < clt 11114  cle 11115  cmin 11310  -cneg 11311   / cdiv 11737  2c2 12133  +crp 12835  (,)cioo 13184  [,)cico 13186  [,]cicc 13187  cre 14907  cim 14908  abscabs 15044  volcvol 24732  MblFncmbf 24883  1citg1 24884  2citg2 24885  𝐿1cibl 24886  citg 24887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-inf2 9502  ax-cnex 11032  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053  ax-pre-sup 11054  ax-addf 11055
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-int 4899  df-iun 4947  df-disj 5062  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-se 5580  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-isom 6492  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-of 7599  df-ofr 7600  df-om 7785  df-1st 7903  df-2nd 7904  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-2o 8372  df-er 8573  df-map 8692  df-pm 8693  df-en 8809  df-dom 8810  df-sdom 8811  df-fin 8812  df-fi 9272  df-sup 9303  df-inf 9304  df-oi 9371  df-dju 9762  df-card 9800  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-div 11738  df-nn 12079  df-2 12141  df-3 12142  df-4 12143  df-n0 12339  df-z 12425  df-uz 12688  df-q 12794  df-rp 12836  df-xneg 12953  df-xadd 12954  df-xmul 12955  df-ioo 13188  df-ico 13190  df-icc 13191  df-fz 13345  df-fzo 13488  df-fl 13617  df-mod 13695  df-seq 13827  df-exp 13888  df-hash 14150  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-clim 15296  df-sum 15497  df-rest 17230  df-topgen 17251  df-psmet 20694  df-xmet 20695  df-met 20696  df-bl 20697  df-mopn 20698  df-top 22148  df-topon 22165  df-bases 22201  df-cmp 22643  df-ovol 24733  df-vol 24734  df-mbf 24888  df-itg1 24889  df-itg2 24890  df-ibl 24891  df-0p 24939
This theorem is referenced by:  ftc1anc  36014
  Copyright terms: Public domain W3C validator