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

Theorem ftc1anclem6 33620
 Description: Lemma for ftc1anc 33623- 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 11896 . . 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 33619 . . 3 ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2))
111, 10sylan2 490 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2))
12 eqid 2651 . . . . 5 (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) d𝑡)
13 ax-icn 10033 . . . . . . . 8 i ∈ ℂ
14 ine0 10503 . . . . . . . 8 i ≠ 0
1513, 14reccli 10793 . . . . . . 7 (1 / i) ∈ ℂ
1615a1i 11 . . . . . 6 (𝜑 → (1 / i) ∈ ℂ)
179ffvelrnda 6399 . . . . . 6 ((𝜑𝑦𝐷) → (𝐹𝑦) ∈ ℂ)
189feqmptd 6288 . . . . . . 7 (𝜑𝐹 = (𝑦𝐷 ↦ (𝐹𝑦)))
1918, 8eqeltrrd 2731 . . . . . 6 (𝜑 → (𝑦𝐷 ↦ (𝐹𝑦)) ∈ 𝐿1)
20 divrec2 10740 . . . . . . . . . 10 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹𝑦) / i) = ((1 / i) · (𝐹𝑦)))
2113, 14, 20mp3an23 1456 . . . . . . . . 9 ((𝐹𝑦) ∈ ℂ → ((𝐹𝑦) / i) = ((1 / i) · (𝐹𝑦)))
2217, 21syl 17 . . . . . . . 8 ((𝜑𝑦𝐷) → ((𝐹𝑦) / i) = ((1 / i) · (𝐹𝑦)))
2322mpteq2dva 4777 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ ((𝐹𝑦) / i)) = (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))))
24 iblmbf 23579 . . . . . . . . 9 ((𝑦𝐷 ↦ (𝐹𝑦)) ∈ 𝐿1 → (𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn)
2519, 24syl 17 . . . . . . . 8 (𝜑 → (𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn)
26 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
2726fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (ℜ‘(𝐹𝑦)) = (ℜ‘(𝐹𝑥)))
2827cbvmptv 4783 . . . . . . . . . . . . . . 15 (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) = (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥)))
2928eleq1i 2721 . . . . . . . . . . . . . 14 ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn)
3017recld 13978 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝐷) → (ℜ‘(𝐹𝑦)) ∈ ℝ)
3130recnd 10106 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐷) → (ℜ‘(𝐹𝑦)) ∈ ℂ)
3231adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn) ∧ 𝑦𝐷) → (ℜ‘(𝐹𝑦)) ∈ ℂ)
3329biimpri 218 . . . . . . . . . . . . . . . 16 ((𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn → (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn)
3433adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn) → (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn)
3532, 34mbfneg 23462 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))) ∈ MblFn) → (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn)
3629, 35sylan2b 491 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn)
379ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐷) → (𝐹𝑥) ∈ ℂ)
3837recld 13978 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐷) → (ℜ‘(𝐹𝑥)) ∈ ℝ)
3938recnd 10106 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷) → (ℜ‘(𝐹𝑥)) ∈ ℂ)
4039negnegd 10421 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → --(ℜ‘(𝐹𝑥)) = (ℜ‘(𝐹𝑥)))
4140mpteq2dva 4777 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) = (𝑥𝐷 ↦ (ℜ‘(𝐹𝑥))))
4241, 28syl6eqr 2703 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) = (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))))
4342adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) = (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))))
44 negex 10317 . . . . . . . . . . . . . . . 16 -(ℜ‘(𝐹𝑥)) ∈ V
4544a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) ∧ 𝑥𝐷) → -(ℜ‘(𝐹𝑥)) ∈ V)
4627negeqd 10313 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → -(ℜ‘(𝐹𝑦)) = -(ℜ‘(𝐹𝑥)))
4746cbvmptv 4783 . . . . . . . . . . . . . . . . . 18 (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) = (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥)))
4847eleq1i 2721 . . . . . . . . . . . . . . . . 17 ((𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥))) ∈ MblFn)
4948biimpi 206 . . . . . . . . . . . . . . . 16 ((𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn → (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥))) ∈ MblFn)
5049adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑥𝐷 ↦ -(ℜ‘(𝐹𝑥))) ∈ MblFn)
5145, 50mbfneg 23462 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑥𝐷 ↦ --(ℜ‘(𝐹𝑥))) ∈ MblFn)
5243, 51eqeltrrd 2731 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn) → (𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn)
5336, 52impbida 895 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn))
54 divcl 10729 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹𝑦) / i) ∈ ℂ)
55 imre 13892 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑦) / i) ∈ ℂ → (ℑ‘((𝐹𝑦) / i)) = (ℜ‘(-i · ((𝐹𝑦) / i))))
5654, 55syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (ℑ‘((𝐹𝑦) / i)) = (ℜ‘(-i · ((𝐹𝑦) / i))))
5713, 14, 56mp3an23 1456 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ ℂ → (ℑ‘((𝐹𝑦) / i)) = (ℜ‘(-i · ((𝐹𝑦) / i))))
5813, 14, 54mp3an23 1456 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ ℂ → ((𝐹𝑦) / i) ∈ ℂ)
59 mulneg1 10504 . . . . . . . . . . . . . . . . . . 19 ((i ∈ ℂ ∧ ((𝐹𝑦) / i) ∈ ℂ) → (-i · ((𝐹𝑦) / i)) = -(i · ((𝐹𝑦) / i)))
6013, 58, 59sylancr 696 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ ℂ → (-i · ((𝐹𝑦) / i)) = -(i · ((𝐹𝑦) / i)))
61 divcan2 10731 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑦) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → (i · ((𝐹𝑦) / i)) = (𝐹𝑦))
6213, 14, 61mp3an23 1456 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) ∈ ℂ → (i · ((𝐹𝑦) / i)) = (𝐹𝑦))
6362negeqd 10313 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ ℂ → -(i · ((𝐹𝑦) / i)) = -(𝐹𝑦))
6460, 63eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝐹𝑦) ∈ ℂ → (-i · ((𝐹𝑦) / i)) = -(𝐹𝑦))
6564fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ ℂ → (ℜ‘(-i · ((𝐹𝑦) / i))) = (ℜ‘-(𝐹𝑦)))
66 reneg 13909 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ ℂ → (ℜ‘-(𝐹𝑦)) = -(ℜ‘(𝐹𝑦)))
6757, 65, 663eqtrd 2689 . . . . . . . . . . . . . . 15 ((𝐹𝑦) ∈ ℂ → (ℑ‘((𝐹𝑦) / i)) = -(ℜ‘(𝐹𝑦)))
6817, 67syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐷) → (ℑ‘((𝐹𝑦) / i)) = -(ℜ‘(𝐹𝑦)))
6968mpteq2dva 4777 . . . . . . . . . . . . 13 (𝜑 → (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) = (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))))
7069eleq1d 2715 . . . . . . . . . . . 12 (𝜑 → ((𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn ↔ (𝑦𝐷 ↦ -(ℜ‘(𝐹𝑦))) ∈ MblFn))
7153, 70bitr4d 271 . . . . . . . . . . 11 (𝜑 → ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn))
72 imval 13891 . . . . . . . . . . . . . 14 ((𝐹𝑦) ∈ ℂ → (ℑ‘(𝐹𝑦)) = (ℜ‘((𝐹𝑦) / i)))
7317, 72syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝐷) → (ℑ‘(𝐹𝑦)) = (ℜ‘((𝐹𝑦) / i)))
7473mpteq2dva 4777 . . . . . . . . . . . 12 (𝜑 → (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) = (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))))
7574eleq1d 2715 . . . . . . . . . . 11 (𝜑 → ((𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn ↔ (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn))
7671, 75anbi12d 747 . . . . . . . . . 10 (𝜑 → (((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn) ↔ ((𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn)))
77 ancom 465 . . . . . . . . . 10 (((𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn) ↔ ((𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn))
7876, 77syl6bb 276 . . . . . . . . 9 (𝜑 → (((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn) ↔ ((𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn)))
7917ismbfcn2 23451 . . . . . . . . 9 (𝜑 → ((𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn ↔ ((𝑦𝐷 ↦ (ℜ‘(𝐹𝑦))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘(𝐹𝑦))) ∈ MblFn)))
8017, 58syl 17 . . . . . . . . . 10 ((𝜑𝑦𝐷) → ((𝐹𝑦) / i) ∈ ℂ)
8180ismbfcn2 23451 . . . . . . . . 9 (𝜑 → ((𝑦𝐷 ↦ ((𝐹𝑦) / i)) ∈ MblFn ↔ ((𝑦𝐷 ↦ (ℜ‘((𝐹𝑦) / i))) ∈ MblFn ∧ (𝑦𝐷 ↦ (ℑ‘((𝐹𝑦) / i))) ∈ MblFn)))
8278, 79, 813bitr4d 300 . . . . . . . 8 (𝜑 → ((𝑦𝐷 ↦ (𝐹𝑦)) ∈ MblFn ↔ (𝑦𝐷 ↦ ((𝐹𝑦) / i)) ∈ MblFn))
8325, 82mpbid 222 . . . . . . 7 (𝜑 → (𝑦𝐷 ↦ ((𝐹𝑦) / i)) ∈ MblFn)
8423, 83eqeltrrd 2731 . . . . . 6 (𝜑 → (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))) ∈ MblFn)
8516, 17, 19, 84iblmulc2nc 33605 . . . . 5 (𝜑 → (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))) ∈ 𝐿1)
86 mulcl 10058 . . . . . . 7 (((1 / i) ∈ ℂ ∧ (𝐹𝑦) ∈ ℂ) → ((1 / i) · (𝐹𝑦)) ∈ ℂ)
8715, 17, 86sylancr 696 . . . . . 6 ((𝜑𝑦𝐷) → ((1 / i) · (𝐹𝑦)) ∈ ℂ)
88 eqid 2651 . . . . . 6 (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))) = (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))
8987, 88fmptd 6425 . . . . 5 (𝜑 → (𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦))):𝐷⟶ℂ)
9012, 3, 4, 5, 6, 7, 85, 89ftc1anclem5 33619 . . . 4 ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2))
911, 90sylan2 490 . . 3 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2))
929ffvelrnda 6399 . . . . . . . . . . . . 13 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
93 0cnd 10071 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
9492, 93ifclda 4153 . . . . . . . . . . . 12 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
95 imval 13891 . . . . . . . . . . . 12 (if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(if(𝑡𝐷, (𝐹𝑡), 0) / i)))
9694, 95syl 17 . . . . . . . . . . 11 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(if(𝑡𝐷, (𝐹𝑡), 0) / i)))
97 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑡 → (𝐹𝑦) = (𝐹𝑡))
9897oveq2d 6706 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑡 → ((1 / i) · (𝐹𝑦)) = ((1 / i) · (𝐹𝑡)))
99 ovex 6718 . . . . . . . . . . . . . . . . 17 ((1 / i) · (𝐹𝑡)) ∈ V
10098, 88, 99fvmpt 6321 . . . . . . . . . . . . . . . 16 (𝑡𝐷 → ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) = ((1 / i) · (𝐹𝑡)))
101100adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐷) → ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) = ((1 / i) · (𝐹𝑡)))
102 divrec2 10740 . . . . . . . . . . . . . . . . 17 (((𝐹𝑡) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((𝐹𝑡) / i) = ((1 / i) · (𝐹𝑡)))
10313, 14, 102mp3an23 1456 . . . . . . . . . . . . . . . 16 ((𝐹𝑡) ∈ ℂ → ((𝐹𝑡) / i) = ((1 / i) · (𝐹𝑡)))
10492, 103syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐷) → ((𝐹𝑡) / i) = ((1 / i) · (𝐹𝑡)))
105101, 104eqtr4d 2688 . . . . . . . . . . . . . 14 ((𝜑𝑡𝐷) → ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡) = ((𝐹𝑡) / i))
106105ifeq1da 4149 . . . . . . . . . . . . 13 (𝜑 → if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0) = if(𝑡𝐷, ((𝐹𝑡) / i), 0))
107 ovif 6779 . . . . . . . . . . . . . 14 (if(𝑡𝐷, (𝐹𝑡), 0) / i) = if(𝑡𝐷, ((𝐹𝑡) / i), (0 / i))
10813, 14div0i 10797 . . . . . . . . . . . . . . 15 (0 / i) = 0
109 ifeq2 4124 . . . . . . . . . . . . . . 15 ((0 / i) = 0 → if(𝑡𝐷, ((𝐹𝑡) / i), (0 / i)) = if(𝑡𝐷, ((𝐹𝑡) / i), 0))
110108, 109ax-mp 5 . . . . . . . . . . . . . 14 if(𝑡𝐷, ((𝐹𝑡) / i), (0 / i)) = if(𝑡𝐷, ((𝐹𝑡) / i), 0)
111107, 110eqtri 2673 . . . . . . . . . . . . 13 (if(𝑡𝐷, (𝐹𝑡), 0) / i) = if(𝑡𝐷, ((𝐹𝑡) / i), 0)
112106, 111syl6eqr 2703 . . . . . . . . . . . 12 (𝜑 → if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0) = (if(𝑡𝐷, (𝐹𝑡), 0) / i))
113112fveq2d 6233 . . . . . . . . . . 11 (𝜑 → (ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡𝐷, (𝐹𝑡), 0) / i)))
11496, 113eqtr4d 2688 . . . . . . . . . 10 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)))
115114oveq1d 6705 . . . . . . . . 9 (𝜑 → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) = ((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡)))
116115fveq2d 6233 . . . . . . . 8 (𝜑 → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))
117116mpteq2dv 4778 . . . . . . 7 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡)))))
118117fveq2d 6233 . . . . . 6 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))))
119118breq1d 4695 . . . . 5 (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
120119rexbidv 3081 . . . 4 (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
121120adantr 480 . . 3 ((𝜑𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, ((𝑦𝐷 ↦ ((1 / i) · (𝐹𝑦)))‘𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)))
12291, 121mpbird 247 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2))
123 reeanv 3136 . . 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)))
124 eleq1w 2713 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑡 → (𝑥𝐷𝑡𝐷))
125 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
126124, 125ifbieq1d 4142 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → if(𝑥𝐷, (𝐹𝑥), 0) = if(𝑡𝐷, (𝐹𝑡), 0))
127126fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
128 eqid 2651 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))
129 fvex 6239 . . . . . . . . . . . . . . 15 (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
130127, 128, 129fvmpt 6321 . . . . . . . . . . . . . 14 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
131130oveq1d 6705 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
132131fveq2d 6233 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
133132mpteq2ia 4773 . . . . . . . . . . 11 (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
134133fveq2i 6232 . . . . . . . . . 10 (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
135 rembl 23354 . . . . . . . . . . . . . . . . 17 ℝ ∈ dom vol
136135a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℝ ∈ dom vol)
137 0cnd 10071 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝑥𝐷) → 0 ∈ ℂ)
13837, 137ifclda 4153 . . . . . . . . . . . . . . . . 17 (𝜑 → if(𝑥𝐷, (𝐹𝑥), 0) ∈ ℂ)
139138adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐷) → if(𝑥𝐷, (𝐹𝑥), 0) ∈ ℂ)
140 eldifn 3766 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥𝐷)
141140adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥𝐷)
142141iffalsed 4130 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥𝐷, (𝐹𝑥), 0) = 0)
1439feqmptd 6288 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥𝐷 ↦ (𝐹𝑥)))
144 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐷 → if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥))
145144mpteq2ia 4773 . . . . . . . . . . . . . . . . . 18 (𝑥𝐷 ↦ if(𝑥𝐷, (𝐹𝑥), 0)) = (𝑥𝐷 ↦ (𝐹𝑥))
146143, 145syl6eqr 2703 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 = (𝑥𝐷 ↦ if(𝑥𝐷, (𝐹𝑥), 0)))
147146, 8eqeltrrd 2731 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝐷 ↦ if(𝑥𝐷, (𝐹𝑥), 0)) ∈ 𝐿1)
1487, 136, 139, 142, 147iblss2 23617 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐷, (𝐹𝑥), 0)) ∈ 𝐿1)
149138adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐷, (𝐹𝑥), 0) ∈ ℂ)
150149iblcn 23610 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥𝐷, (𝐹𝑥), 0)) ∈ 𝐿1 ↔ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)))
151148, 150mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1))
152151simpld 474 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
153149recld 13978 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ∈ ℝ)
154153, 128fmptd 6425 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
155152, 154jca 553 . . . . . . . . . . . 12 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
156 ftc1anclem4 33618 . . . . . . . . . . . . 13 ((𝑓 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
1571563expb 1285 . . . . . . . . . . . 12 ((𝑓 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
158155, 157sylan2 490 . . . . . . . . . . 11 ((𝑓 ∈ dom ∫1𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
159158ancoms 468 . . . . . . . . . 10 ((𝜑𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑓𝑡))))) ∈ ℝ)
160134, 159syl5eqelr 2735 . . . . . . . . 9 ((𝜑𝑓 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ)
161126fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))
162 eqid 2651 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))
163 fvex 6239 . . . . . . . . . . . . . . 15 (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
164161, 162, 163fvmpt 6321 . . . . . . . . . . . . . 14 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))
165164oveq1d 6705 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡)) = ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))
166165fveq2d 6233 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))) = (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
167166mpteq2ia 4773 . . . . . . . . . . 11 (𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
168167fveq2i 6232 . . . . . . . . . 10 (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
169151simprd 478 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
170138imcld 13979 . . . . . . . . . . . . . . 15 (𝜑 → (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)) ∈ ℝ)
171170adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)) ∈ ℝ)
172171, 162fmptd 6425 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
173169, 172jca 553 . . . . . . . . . . . 12 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
174 ftc1anclem4 33618 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
1751743expb 1285 . . . . . . . . . . . 12 ((𝑔 ∈ dom ∫1 ∧ ((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
176173, 175sylan2 490 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1𝜑) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
177176ancoms 468 . . . . . . . . . 10 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℑ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − (𝑔𝑡))))) ∈ ℝ)
178168, 177syl5eqelr 2735 . . . . . . . . 9 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ)
179160, 178anim12dan 900 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ))
1801rpred 11910 . . . . . . . . 9 (𝑌 ∈ ℝ+ → (𝑌 / 2) ∈ ℝ)
181180, 180jca 553 . . . . . . . 8 (𝑌 ∈ ℝ+ → ((𝑌 / 2) ∈ ℝ ∧ (𝑌 / 2) ∈ ℝ))
182 lt2add 10551 . . . . . . . 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))))
183179, 181, 182syl2an 493 . . . . . . 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))))
184183an32s 863 . . . . . 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))))
18594recld 13978 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
186185recnd 10106 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
187 i1ff 23488 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
188187ffvelrnda 6399 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
189188recnd 10106 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
190 subcl 10318 . . . . . . . . . . . . . . . . . 18 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (𝑓𝑡) ∈ ℂ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
191186, 189, 190syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
192191anassrs 681 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
193192adantlrr 757 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℂ)
19494imcld 13979 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
195194recnd 10106 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
196 i1ff 23488 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
197196ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
198197recnd 10106 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
199 subcl 10318 . . . . . . . . . . . . . . . . . . 19 (((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ)
200195, 198, 199syl2an 493 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ)
201200anassrs 681 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ)
202 mulcl 10058 . . . . . . . . . . . . . . . . 17 ((i ∈ ℂ ∧ ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
20313, 201, 202sylancr 696 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
204203adantlrl 756 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
205193, 204addcld 10097 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) ∈ ℂ)
206205abscld 14219 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ)
207206rexrd 10127 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ*)
208205absge0d 14227 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
209 elxrge0 12319 . . . . . . . . . . . 12 ((abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
210207, 208, 209sylanbrc 699 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ (0[,]+∞))
211 eqid 2651 . . . . . . . . . . 11 (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
212210, 211fmptd 6425 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))):ℝ⟶(0[,]+∞))
213 icossicc 12298 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
214 ge0addcl 12322 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
215213, 214sseldi 3634 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,]+∞))
216215adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞))
217192abscld 14219 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ ℝ)
218192absge0d 14227 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
219 elrege0 12316 . . . . . . . . . . . . . 14 ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
220217, 218, 219sylanbrc 699 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ (0[,)+∞))
221 eqid 2651 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))
222220, 221fmptd 6425 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))):ℝ⟶(0[,)+∞))
223222adantrr 753 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))):ℝ⟶(0[,)+∞))
224201abscld 14219 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℝ)
225201absge0d 14227 . . . . . . . . . . . . . 14 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
226 elrege0 12316 . . . . . . . . . . . . . 14 ((abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ (0[,)+∞) ↔ ((abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
227224, 225, 226sylanbrc 699 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ (0[,)+∞))
228 eqid 2651 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
229227, 228fmptd 6425 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))):ℝ⟶(0[,)+∞))
230229adantrl 752 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))):ℝ⟶(0[,)+∞))
231 reex 10065 . . . . . . . . . . . 12 ℝ ∈ V
232231a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ℝ ∈ V)
233 inidm 3855 . . . . . . . . . . 11 (ℝ ∩ ℝ) = ℝ
234216, 223, 230, 232, 232, 233off 6954 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))):ℝ⟶(0[,]+∞))
235193, 204abstrid 14239 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
236235ralrimiva 2995 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
237 ovexd 6720 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ V)
238 eqidd 2652 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
239 fvexd 6241 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ V)
240 fvexd 6241 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) ∈ V)
241 eqidd 2652 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
242 absmul 14078 . . . . . . . . . . . . . . . . 17 ((i ∈ ℂ ∧ ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)) ∈ ℂ) → (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
24313, 201, 242sylancr 696 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
244 absi 14070 . . . . . . . . . . . . . . . . . 18 (abs‘i) = 1
245244oveq1i 6700 . . . . . . . . . . . . . . . . 17 ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (1 · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
246224recnd 10106 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) ∈ ℂ)
247246mulid2d 10096 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1 · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
248245, 247syl5eq 2697 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘i) · (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))
249243, 248eqtr2d 2686 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))
250249mpteq2dva 4777 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
251250adantrl 752 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
252232, 239, 240, 241, 251offval2 6956 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) = (𝑡 ∈ ℝ ↦ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
253232, 206, 237, 238, 252ofrfval2 6957 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ↔ ∀𝑡 ∈ ℝ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ≤ ((abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) + (abs‘(i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
254236, 253mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))
255 itg2le 23551 . . . . . . . . . 10 (((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))):ℝ⟶(0[,]+∞) ∧ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
256212, 234, 254, 255syl3anc 1366 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
257 absf 14121 . . . . . . . . . . . . . 14 abs:ℂ⟶ℝ
258257a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑓 ∈ dom ∫1) → abs:ℂ⟶ℝ)
259258, 192cofmpt 6439 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))))
260 resubcl 10383 . . . . . . . . . . . . . . . 16 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑓𝑡) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℝ)
261185, 188, 260syl2an 493 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℝ)
262261anassrs 681 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ ℝ)
263 eqid 2651 . . . . . . . . . . . . . 14 (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) = (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
264262, 263fmptd 6425 . . . . . . . . . . . . 13 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))):ℝ⟶ℝ)
265135a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑓 ∈ dom ∫1) → ℝ ∈ dom vol)
266 iunin2 4616 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦}))
267 imaiun 6543 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 𝑦 ∈ ran 𝑓{𝑦}) = 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦})
268 iunid 4607 . . . . . . . . . . . . . . . . . . . . . 22 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓
269268imaeq2i 5499 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 𝑦 ∈ ran 𝑓{𝑦}) = (𝑓 “ ran 𝑓)
270267, 269eqtr3i 2675 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦}) = (𝑓 “ ran 𝑓)
271270ineq2i 3844 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓))
272266, 271eqtri 2673 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓))
273 cnvimass 5520 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
274 ovex 6718 . . . . . . . . . . . . . . . . . . . . . 22 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ V
275274, 263dmmpti 6061 . . . . . . . . . . . . . . . . . . . . 21 dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) = ℝ
276273, 275sseqtri 3670 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ ℝ
277 cnvimarndm 5521 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 “ ran 𝑓) = dom 𝑓
278 fdm 6089 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:ℝ⟶ℝ → dom 𝑓 = ℝ)
279187, 278syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ)
280277, 279syl5eq 2697 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (𝑓 “ ran 𝑓) = ℝ)
281276, 280syl5sseqr 3687 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ (𝑓 “ ran 𝑓))
282 df-ss 3621 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ⊆ (𝑓 “ ran 𝑓) ↔ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
283281, 282sylib 208 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
284272, 283syl5eq 2697 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
285284ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)))
286 frn 6091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℝ)
287187, 286syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
288287ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran 𝑓 ⊆ ℝ)
289288sselda 3636 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ)
290185ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
291 resubcl 10383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ)
292185, 291sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ)
293292adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ)
294290, 2932thd 255 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ))
295 ltaddsub 10540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
296185, 295syl3an3 1401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
2972963comr 1290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
2982973expa 1284 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦)))
299294, 298anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))))
300 readdcl 10057 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
301300rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
302301adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ*)
303 elioopnf 12305 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
305 rexr 10123 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
306305ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*)
307 elioopnf 12305 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))))
308306, 307syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))))
309299, 304, 3083bitr4rd 301 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))
310 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑡) = 𝑦 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦))
311310eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞)))
312311bibi1d 332 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑡) = 𝑦 → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
313309, 312syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))))
314313pm5.32rd 673 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)))
315314adantllr 755 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)))
316289, 315syldan 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)))
317316rabbidv 3220 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
318187feqmptd 6288 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ dom ∫1𝑓 = (𝑡 ∈ ℝ ↦ (𝑓𝑡)))
319318cnveqd 5330 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∈ dom ∫1𝑓 = (𝑡 ∈ ℝ ↦ (𝑓𝑡)))
320319imaeq1d 5500 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1 → (𝑓 “ {𝑦}) = ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦}))
321320ineq2d 3847 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
322263mptpreima 5666 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞)}
323 vex 3234 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦 ∈ V
324 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ ℝ ↦ (𝑓𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓𝑡))
325324mptiniseg 5667 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ V → ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
326323, 325ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}
327322, 326ineq12i 3845 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
328 inrab 3932 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
329327, 328eqtri 2673 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
330321, 329syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
331330ad3antlr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
332320ineq2d 3847 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
333 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
334333mptpreima 5666 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)}
335334, 326ineq12i 3845 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
336 inrab 3932 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
337335, 336eqtri 2673 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)}
338332, 337syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
339338ad3antlr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓𝑡) = 𝑦)})
340317, 331, 3393eqtr4d 2695 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})))
341340iuneq2dv 4574 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∩ (𝑓 “ {𝑦})) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})))
342285, 341eqtr3d 2687 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})))
343 i1frn 23489 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
344343adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → ran 𝑓 ∈ Fin)
34594adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡𝐷) → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
346 eldifn 3766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡𝐷)
347346adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡𝐷)
348347iffalsed 4130 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡𝐷, (𝐹𝑡), 0) = 0)
3499feqmptd 6288 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
350 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
351350mpteq2ia 4773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡𝐷 ↦ if(𝑡𝐷, (𝐹𝑡), 0)) = (𝑡𝐷 ↦ (𝐹𝑡))
352349, 351syl6eqr 2703 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 = (𝑡𝐷 ↦ if(𝑡𝐷, (𝐹𝑡), 0)))
353 iblmbf 23579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
3548, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 ∈ MblFn)
355352, 354eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡𝐷 ↦ if(𝑡𝐷, (𝐹𝑡), 0)) ∈ MblFn)
3567, 136, 345, 348, 355mbfss 23458 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (𝐹𝑡), 0)) ∈ MblFn)
35794adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
358357ismbfcn2 23451 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡𝐷, (𝐹𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)))
359356, 358mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn))
360359simpld 474 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
361185adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
362361, 333fmptd 6425 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ)
363 mbfima 23444 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
364360, 362, 363syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol)
365 i1fima 23490 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (𝑓 “ {𝑦}) ∈ dom vol)
366 inmbl 23356 . . . . . . . . . . . . . . . . . . 19 ((((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (𝑓 “ {𝑦}) ∈ dom vol) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
367364, 365, 366syl2an 493 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
368367ralrimivw 2996 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
369 finiunmbl 23358 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
370344, 368, 369syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
371370adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
372342, 371eqeltrd 2730 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (𝑥(,)+∞)) ∈ dom vol)
373 iunin2 4616 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦}))
374270ineq2i 3844 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ 𝑦 ∈ ran 𝑓(𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓))
375373, 374eqtri 2673 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓))
376 cnvimass 5520 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))
377376, 275sseqtri 3670 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ
378377, 280syl5sseqr 3687 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ (𝑓 “ ran 𝑓))
379 df-ss 3621 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ⊆ (𝑓 “ ran 𝑓) ↔ (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
380378, 379sylib 208 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ ran 𝑓)) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
381375, 380syl5eq 2697 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
382381ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)))
383293, 2902thd 255 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ))
384 ltsubadd 10536 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
385185, 384syl3an1 1399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
3863853expa 1284 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
387386an32s 863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦)))
388383, 387anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦))))
389 elioomnf 12306 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ* → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥)))
390306, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ ℝ ∧ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) < 𝑥)))
391 elioomnf 12306 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 + 𝑦) ∈ ℝ* → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦))))
392302, 391syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < (𝑥 + 𝑦))))
393388, 390, 3923bitr4d 300 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))
394310eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥)))
395394bibi1d 332 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑡) = 𝑦 → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
396393, 395syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓𝑡) = 𝑦 → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))))
397396pm5.32rd 673 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)))
398397adantllr 755 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)))
399289, 398syldan 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)))
400399rabbidv 3220 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)})
401320ineq2d 3847 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
402263mptpreima 5666 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥)}
403402, 326ineq12i 3845 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
404 inrab 3932 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)}
405403, 404eqtri 2673 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)}
406401, 405syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)})
407406ad3antlr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓𝑡) = 𝑦)})
408320ineq2d 3847 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})))
409333mptpreima 5666 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))}
410409, 326ineq12i 3845 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦})
411 inrab 3932 . . . . . . . . . . . . . . . . . . . . 21 ({𝑡 ∈ ℝ ∣ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)}
412410, 411eqtri 2673 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ ((𝑡 ∈ ℝ ↦ (𝑓𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)}
413408, 412syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)})
414413ad3antlr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓𝑡) = 𝑦)})
415400, 407, 4143eqtr4d 2695 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})))
416415iuneq2dv 4574 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∩ (𝑓 “ {𝑦})) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})))
417382, 416eqtr3d 2687 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) = 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})))
418 mbfima 23444 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
419360, 362, 418syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol)
420 inmbl 23356 . . . . . . . . . . . . . . . . . . 19 ((((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (𝑓 “ {𝑦}) ∈ dom vol) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
421419, 365, 420syl2an 493 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓 ∈ dom ∫1) → (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
422421ralrimivw 2996 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓 ∈ dom ∫1) → ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
423 finiunmbl 23358 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ∀𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
424344, 422, 423syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ dom ∫1) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
425424adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → 𝑦 ∈ ran 𝑓(((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (𝑓 “ {𝑦})) ∈ dom vol)
426417, 425eqeltrd 2730 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) “ (-∞(,)𝑥)) ∈ dom vol)
427264, 265, 372, 426ismbf2d 23453 . . . . . . . . . . . . 13 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ MblFn)
428 ftc1anclem1 33615 . . . . . . . . . . . . 13 (((𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
429264, 427, 428syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ dom ∫1) → (abs ∘ (𝑡 ∈ ℝ ↦ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
430259, 429eqeltrrd 2731 . . . . . . . . . . 11 ((𝜑𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
431430adantrr 753 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∈ MblFn)
432160adantrr 753 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ)
433178adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ)
434431, 223, 432, 230, 433itg2addnc 33594 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
435256, 434breqtrd 4711 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
436435adantlr 751 . . . . . . 7 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))))
437 itg2cl 23544 . . . . . . . . . 10 ((𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ*)
438212, 437syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ*)
439438adantlr 751 . . . . . . . 8 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) ∈ ℝ*)
440 readdcl 10057 . . . . . . . . . . . 12 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ)
441160, 178, 440syl2an 493 . . . . . . . . . . 11 (((𝜑𝑓 ∈ dom ∫1) ∧ (𝜑𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ)
442441anandis 890 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ)
443442rexrd 10127 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ*)
444443adantlr 751 . . . . . . . 8 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) ∈ ℝ*)
4451, 1rpaddcld 11925 . . . . . . . . . 10 (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ+)
446445rpxrd 11911 . . . . . . . . 9 (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
447446ad2antlr 763 . . . . . . . 8 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈ ℝ*)
448 xrlelttr 12025 . . . . . . . 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))))
449439, 444, 447, 448syl3anc 1366 . . . . . . 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))))
450436, 449mpand 711 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2))))
451184, 450syld 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))))
452 mulcl 10058 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ) → (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ)
45313, 195, 452sylancr 696 . . . . . . . . . . . . . 14 (𝜑 → (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ)
454186, 453jca 553 . . . . . . . . . . . . 13 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ))
455 mulcl 10058 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
45613, 198, 455sylancr 696 . . . . . . . . . . . . . . 15 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
457189, 456anim12i 589 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ))
458457anandirs 891 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ))
459 addsub4 10362 . . . . . . . . . . . . 13 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ) ∧ ((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
460454, 458, 459syl2an 493 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
461460anassrs 681 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
46294replimd 13981 . . . . . . . . . . . . 13 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
463462ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → if(𝑡𝐷, (𝐹𝑡), 0) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
464463oveq1d 6705 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + (i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)))) − ((𝑓𝑡) + (i · (𝑔𝑡)))))
465198adantll 750 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
466 subdi 10501 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡))))
46713, 195, 465, 466mp3an3an 1470 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡))))
468467anassrs 681 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))) = ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡))))
469468oveq2d 6706 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + ((i · (ℑ‘if(𝑡𝐷, (𝐹𝑡), 0))) − (i · (𝑔𝑡)))))
470461, 464, 4693eqtr4rd 2696 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))) = (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))
471470fveq2d 6233 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) = (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
472471mpteq2dva 4777 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
473472fveq2d 6233 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
474473adantlr 751 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
475 rpcn 11879 . . . . . . . 8 (𝑌 ∈ ℝ+𝑌 ∈ ℂ)
4764752halvesd 11316 . . . . . . 7 (𝑌 ∈ ℝ+ → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
477476ad2antlr 763 . . . . . 6 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌)
478474, 477breq12d 4698 . . . . 5 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡)) + (i · ((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
479451, 478sylibd 229 . . . 4 (((𝜑𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
480479reximdvva 3048 . . 3 ((𝜑𝑌 ∈ ℝ+) → (∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
481123, 480syl5bir 233 . 2 ((𝜑𝑌 ∈ ℝ+) → ((∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < (𝑌 / 2) ∧ ∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℑ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑔𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌))
48211, 122, 481mp2and 715 1 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < 𝑌)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∩ cin 3606   ⊆ wss 3607  ifcif 4119  {csn 4210  ∪ ciun 4552   class class class wbr 4685   ↦ cmpt 4762  ◡ccnv 5142  dom cdm 5143  ran crn 5144   “ cima 5146   ∘ ccom 5147  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ∘𝑓 cof 6937   ∘𝑟 cofr 6938  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975  ici 9976   + caddc 9977   · cmul 9979  +∞cpnf 10109  -∞cmnf 10110  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  2c2 11108  ℝ+crp 11870  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  ℜcre 13881  ℑcim 13882  abscabs 14018  volcvol 23278  MblFncmbf 23428  ∫1citg1 23429  ∫2citg2 23430  𝐿1cibl 23431  ∫citg 23432 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435  df-ibl 23436  df-0p 23482 This theorem is referenced by:  ftc1anc  33623
 Copyright terms: Public domain W3C validator