Metamath Proof Explorer

Theorem ftc1anclem6

Description: Lemma for ftc1anc - 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 F . (Contributed by Brendan Leahy, 31-May-2018)

Ref Expression
Hypotheses ftc1anc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1anc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1anc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1anc.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1anc.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
ftc1anc.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
ftc1anc.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
ftc1anc.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
Assertion ftc1anclem6 ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 )

Proof

Step Hyp Ref Expression
1 ftc1anc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1anc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1anc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1anc.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1anc.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6 ftc1anc.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7 ftc1anc.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8 ftc1anc.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
9 rphalfcl ⊢ ( 𝑌 ∈ ℝ+ → ( 𝑌 / 2 ) ∈ ℝ+ )
10 1 2 3 4 5 6 7 8 ftc1anclem5 ⊢ ( ( 𝜑 ∧ ( 𝑌 / 2 ) ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
11 9 10 sylan2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
12 eqid ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) d 𝑡 )
13 ax-icn ⊢ i ∈ ℂ
14 ine0 ⊢ i ≠ 0
15 13 14 reccli ⊢ ( 1 / i ) ∈ ℂ
16 15 a1i ⊢ ( 𝜑 → ( 1 / i ) ∈ ℂ )
17 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
18 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) )
19 18 7 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐿1 )
20 divrec2 ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
21 13 14 20 mp3an23 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑦 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
22 17 21 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
23 22 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) )
24 iblmbf ⊢ ( ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐿1 → ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn )
25 19 24 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn )
26 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
27 26 cbvmptv ⊢ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
28 27 eleq1i ⊢ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
29 17 recld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
30 29 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) ∧ 𝑦 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
32 28 biimpri ⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn → ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
33 32 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
34 31 33 mbfneg ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
35 28 34 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
36 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
37 36 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
38 37 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
39 38 negnegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
40 39 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
41 40 27 eqtr4di ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
43 negex ⊢ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ V
44 43 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ∧ 𝑥 ∈ 𝐷 ) → - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ V )
45 26 negeqd ⊢ ( 𝑦 = 𝑥 → - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
46 45 cbvmptv ⊢ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
47 46 eleq1i ⊢ ( ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
48 47 biimpi ⊢ ( ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn → ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
49 48 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑥 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
50 44 49 mbfneg ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑥 ∈ 𝐷 ↦ - - ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
51 42 50 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) → ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
52 35 51 impbida ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) )
53 divcl ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ )
54 imre ⊢ ( ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
55 53 54 syl ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
56 13 14 55 mp3an23 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
57 13 14 53 mp3an23 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ )
58 mulneg1 ⊢ ( ( i ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ ) → ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
59 13 57 58 sylancr ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
60 divcan2 ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( 𝐹 ‘ 𝑦 ) )
61 13 14 60 mp3an23 ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = ( 𝐹 ‘ 𝑦 ) )
62 61 negeqd ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → - ( i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( 𝐹 ‘ 𝑦 ) )
63 59 62 eqtrd ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( 𝐹 ‘ 𝑦 ) )
64 63 fveq2d ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℜ ‘ ( - i · ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) = ( ℜ ‘ - ( 𝐹 ‘ 𝑦 ) ) )
65 reneg ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℜ ‘ - ( 𝐹 ‘ 𝑦 ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) )
66 56 64 65 3eqtrd ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) )
67 17 66 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) = - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) )
68 67 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) = ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
69 68 eleq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ - ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) )
70 52 69 bitr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) )
71 imval ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℂ → ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
72 17 71 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) )
73 72 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) )
74 73 eleq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) )
75 70 74 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ) )
76 ancom ⊢ ( ( ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) )
77 75 76 bitrdi ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ) )
78 17 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn ) ) )
79 17 57 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) / i ) ∈ ℂ )
80 79 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ∈ MblFn ↔ ( ( 𝑦 ∈ 𝐷 ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ∧ ( 𝑦 ∈ 𝐷 ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ) ∈ MblFn ) ) )
81 77 78 80 3bitr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ MblFn ↔ ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ∈ MblFn ) )
82 25 81 mpbid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑦 ) / i ) ) ∈ MblFn )
83 23 82 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ∈ MblFn )
84 16 17 19 83 iblmulc2nc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐿1 )
85 mulcl ⊢ ( ( ( 1 / i ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) → ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
86 15 17 85 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
87 86 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) : 𝐷 ⟶ ℂ )
88 12 2 3 4 5 6 84 87 ftc1anclem5 ⊢ ( ( 𝜑 ∧ ( 𝑌 / 2 ) ∈ ℝ+ ) → ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
89 9 88 sylan2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
90 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
91 0cnd ⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℂ )
92 90 91 ifclda ⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
93 imval ⊢ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) ) )
94 92 93 syl ⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) ) )
95 fveq2 ⊢ ( 𝑦 = 𝑡 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑡 ) )
96 95 oveq2d ⊢ ( 𝑦 = 𝑡 → ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
97 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) )
98 ovex ⊢ ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) ∈ V
99 96 97 98 fvmpt ⊢ ( 𝑡 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
100 99 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
101 divrec2 ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( 𝐹 ‘ 𝑡 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
102 13 14 101 mp3an23 ⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑡 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
103 90 102 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑡 ) / i ) = ( ( 1 / i ) · ( 𝐹 ‘ 𝑡 ) ) )
104 100 103 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) / i ) )
105 104 ifeq1da ⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 ) )
106 ovif ⊢ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , ( 0 / i ) )
107 13 14 div0i ⊢ ( 0 / i ) = 0
108 ifeq2 ⊢ ( ( 0 / i ) = 0 → if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , ( 0 / i ) ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 ) )
109 107 108 ax-mp ⊢ if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , ( 0 / i ) ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 )
110 106 109 eqtri ⊢ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) = if ( 𝑡 ∈ 𝐷 , ( ( 𝐹 ‘ 𝑡 ) / i ) , 0 )
111 105 110 eqtr4di ⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) = ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) )
112 111 fveq2d ⊢ ( 𝜑 → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) / i ) ) )
113 94 112 eqtr4d ⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) )
114 113 fvoveq1d ⊢ ( 𝜑 → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
115 114 mpteq2dv ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
116 115 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
117 116 breq1d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
118 117 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ↔ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ( ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ↔ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( ( 𝑦 ∈ 𝐷 ↦ ( ( 1 / i ) · ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) )
120 89 119 mpbird ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) )
121 reeanv ⊢ ( ∃ 𝑓 ∈ 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 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷 ) )
123 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
124 122 123 ifbieq1d ⊢ ( 𝑥 = 𝑡 → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) )
125 124 fveq2d ⊢ ( 𝑥 = 𝑡 → ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
126 eqid ⊢ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
127 fvex ⊢ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ V
128 125 126 127 fvmpt ⊢ ( 𝑡 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) = ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
129 128 fvoveq1d ⊢ ( 𝑡 ∈ ℝ → ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) )
130 129 mpteq2ia ⊢ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) )
131 130 fveq2i ⊢ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
132 rembl ⊢ ℝ ∈ dom vol
133 132 a1i ⊢ ( 𝜑 → ℝ ∈ dom vol )
134 0cnd ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐷 ) → 0 ∈ ℂ )
135 36 134 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℂ )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℂ )
137 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐷 ) → ¬ 𝑥 ∈ 𝐷 )
138 137 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐷 ) ) → ¬ 𝑥 ∈ 𝐷 )
139 138 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐷 ) ) → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
140 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
141 iftrue ⊢ ( 𝑥 ∈ 𝐷 → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
142 141 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) )
143 140 142 eqtr4di ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
144 143 7 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
145 6 133 136 139 144 iblss2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
146 135 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℂ )
147 146 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ) ) )
148 145 147 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ) )
149 148 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 )
150 146 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ ℝ )
151 150 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ )
152 149 151 jca ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) )
153 ftc1anclem4 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
154 153 3expb ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
155 152 154 sylan2 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝜑 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
156 155 ancoms ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
157 131 156 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
158 124 fveq2d ⊢ ( 𝑥 = 𝑡 → ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
159 eqid ⊢ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
160 fvex ⊢ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ V
161 158 159 160 fvmpt ⊢ ( 𝑡 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) = ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
162 161 fvoveq1d ⊢ ( 𝑡 ∈ ℝ → ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
163 162 mpteq2ia ⊢ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
164 163 fveq2i ⊢ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
165 148 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 )
166 135 imcld ⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ ℝ )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ ℝ )
168 167 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ )
169 165 168 jca ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) )
170 ftc1anclem4 ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
171 170 3expb ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) : ℝ ⟶ ℝ ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
172 169 171 sylan2 ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝜑 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
173 172 ancoms ⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( 𝑥 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑥 ∈ 𝐷 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑡 ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
174 164 173 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
175 157 174 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) )
176 9 rpred ⊢ ( 𝑌 ∈ ℝ+ → ( 𝑌 / 2 ) ∈ ℝ )
177 176 176 jca ⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) ∈ ℝ ∧ ( 𝑌 / 2 ) ∈ ℝ ) )
178 lt2add ⊢ ( ( ( ( ∫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 ) ) ) )
179 175 177 178 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑌 ∈ ℝ+ ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
180 179 an32s ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
181 92 recld ⊢ ( 𝜑 → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
182 181 recnd ⊢ ( 𝜑 → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ )
183 i1ff ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
184 183 ffvelcdmda ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
185 184 recnd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℂ )
186 subcl ⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( 𝑓 ‘ 𝑡 ) ∈ ℂ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
187 182 185 186 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
188 187 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
189 188 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℂ )
190 92 imcld ⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
191 190 recnd ⊢ ( 𝜑 → ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ )
192 i1ff ⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 : ℝ ⟶ ℝ )
193 192 ffvelcdmda ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
194 193 recnd ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ )
195 subcl ⊢ ( ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
196 191 194 195 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
197 196 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
198 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
199 13 197 198 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
200 199 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
201 189 200 addcld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
202 201 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
203 202 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
204 201 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
205 elxrge0 ⊢ ( ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
206 203 204 205 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
207 206 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
208 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
209 ge0addcl ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
210 208 209 sselid ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,] +∞ ) )
211 210 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,] +∞ ) )
212 188 abscld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ℝ )
213 188 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) )
214 elrege0 ⊢ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
215 212 213 214 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
216 215 fmpttd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
217 216 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
218 197 abscld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
219 197 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
220 elrege0 ⊢ ( ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
221 218 219 220 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
222 221 fmpttd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
223 222 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
224 reex ⊢ ℝ ∈ V
225 224 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ℝ ∈ V )
226 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
227 211 217 223 225 225 226 off ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
228 189 200 abstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
229 228 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ∀ 𝑡 ∈ ℝ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
230 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ V )
231 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
232 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ V )
233 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ V )
234 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
235 absmul ⊢ ( ( i ∈ ℂ ∧ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
236 13 197 235 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
237 absi ⊢ ( abs ‘ i ) = 1
238 237 oveq1i ⊢ ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 1 · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
239 218 recnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
240 239 mullidd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 1 · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
241 238 240 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ i ) · ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) )
242 236 241 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) )
243 242 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
244 243 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
245 225 232 233 234 244 offval2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
246 225 202 230 231 245 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 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 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
247 229 246 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∘r ≤ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
248 itg2le ⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( 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 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
249 207 227 247 248 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
250 absf ⊢ abs : ℂ ⟶ ℝ
251 250 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → abs : ℂ ⟶ ℝ )
252 251 188 cofmpt ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) )
253 resubcl ⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑓 ‘ 𝑡 ) ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
254 181 184 253 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
255 254 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
256 255 fmpttd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) : ℝ ⟶ ℝ )
257 132 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ℝ ∈ dom vol )
258 iunin2 ⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) )
259 imaiun ⊢ ( ◡ 𝑓 “ ∪ 𝑦 ∈ ran 𝑓 { 𝑦 } ) = ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } )
260 iunid ⊢ ∪ 𝑦 ∈ ran 𝑓 { 𝑦 } = ran 𝑓
261 260 imaeq2i ⊢ ( ◡ 𝑓 “ ∪ 𝑦 ∈ ran 𝑓 { 𝑦 } ) = ( ◡ 𝑓 “ ran 𝑓 )
262 259 261 eqtr3i ⊢ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) = ( ◡ 𝑓 “ ran 𝑓 )
263 262 ineq2i ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
264 258 263 eqtri ⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
265 cnvimass ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ dom ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) )
266 ovex ⊢ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ V
267 eqid ⊢ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) )
268 266 267 dmmpti ⊢ dom ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) = ℝ
269 265 268 sseqtri ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ ℝ
270 cnvimarndm ⊢ ( ◡ 𝑓 “ ran 𝑓 ) = dom 𝑓
271 183 fdmd ⊢ ( 𝑓 ∈ dom ∫1 → dom 𝑓 = ℝ )
272 270 271 eqtrid ⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ 𝑓 “ ran 𝑓 ) = ℝ )
273 269 272 sseqtrrid ⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) )
274 dfss2 ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) ↔ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
275 273 274 sylib ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
276 264 275 eqtrid ⊢ ( 𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
277 276 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) )
278 183 frnd ⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ )
279 278 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ran 𝑓 ⊆ ℝ )
280 279 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → 𝑦 ∈ ℝ )
281 181 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
282 resubcl ⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ )
283 181 282 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ )
284 283 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ )
285 281 284 2thd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ) )
286 ltaddsub ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
287 181 286 syl3an3 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑 ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
288 287 3comr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
289 288 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ↔ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) )
290 285 289 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) ) )
291 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
292 291 rexrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
293 292 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
294 elioopnf ⊢ ( ( 𝑥 + 𝑦 ) ∈ ℝ* → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
295 293 294 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( 𝑥 + 𝑦 ) < ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
296 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
297 296 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ* )
298 elioopnf ⊢ ( 𝑥 ∈ ℝ* → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) ) )
299 297 298 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ 𝑥 < ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ) ) )
300 290 295 299 3bitr4rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) )
301 oveq2 ⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) = ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) )
302 301 eleq1d ⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ) )
303 302 bibi1d ⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ) )
304 300 303 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ) )
305 304 pm5.32rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
306 305 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
307 280 306 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
308 307 rabbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
309 183 feqmptd ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
310 309 cnveqd ⊢ ( 𝑓 ∈ dom ∫1 → ◡ 𝑓 = ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
311 310 imaeq1d ⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ 𝑓 “ { 𝑦 } ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) )
312 311 ineq2d ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
313 267 mptpreima ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) }
314 vex ⊢ 𝑦 ∈ V
315 eqid ⊢ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) )
316 315 mptiniseg ⊢ ( 𝑦 ∈ V → ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
317 314 316 ax-mp ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 }
318 313 317 ineq12i ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
319 inrab ⊢ ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
320 318 319 eqtri ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
321 312 320 eqtrdi ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
322 321 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( 𝑥 (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
323 311 ineq2d ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
324 eqid ⊢ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
325 324 mptpreima ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) = { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) }
326 325 317 ineq12i ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
327 inrab ⊢ ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
328 326 327 eqtri ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
329 323 328 eqtrdi ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
330 329 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
331 308 322 330 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
332 331 iuneq2dv ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
333 277 332 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
334 i1frn ⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin )
335 334 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ran 𝑓 ∈ Fin )
336 92 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
337 eldifn ⊢ ( 𝑡 ∈ ( ℝ ∖ 𝐷 ) → ¬ 𝑡 ∈ 𝐷 )
338 337 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → ¬ 𝑡 ∈ 𝐷 )
339 338 iffalsed ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = 0 )
340 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
341 iftrue ⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( 𝐹 ‘ 𝑡 ) )
342 341 mpteq2ia ⊢ ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) )
343 340 342 eqtr4di ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) )
344 iblmbf ⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )
345 7 344 syl ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
346 343 345 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ MblFn )
347 6 133 336 339 346 mbfss ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ MblFn )
348 92 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
349 348 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ MblFn ↔ ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ) ) )
350 347 349 mpbid ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ) )
351 350 simpld ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn )
352 181 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ )
353 352 fmpttd ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) : ℝ ⟶ ℝ )
354 mbfima ⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∈ dom vol )
355 351 353 354 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∈ dom vol )
356 i1fima ⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ 𝑓 “ { 𝑦 } ) ∈ dom vol )
357 inmbl ⊢ ( ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∈ dom vol ∧ ( ◡ 𝑓 “ { 𝑦 } ) ∈ dom vol ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
358 355 356 357 syl2an ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
359 358 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
360 finiunmbl ⊢ ( ( ran 𝑓 ∈ Fin ∧ ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
361 335 359 360 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
362 361 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( ( 𝑥 + 𝑦 ) (,) +∞ ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
363 333 362 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
364 iunin2 ⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) )
365 262 ineq2i ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ∪ 𝑦 ∈ ran 𝑓 ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
366 364 365 eqtri ⊢ ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) )
367 cnvimass ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ dom ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) )
368 367 268 sseqtri ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ ℝ
369 368 272 sseqtrrid ⊢ ( 𝑓 ∈ dom ∫1 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) )
370 dfss2 ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ⊆ ( ◡ 𝑓 “ ran 𝑓 ) ↔ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
371 369 370 sylib ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ ran 𝑓 ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
372 366 371 eqtrid ⊢ ( 𝑓 ∈ dom ∫1 → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
373 372 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) )
374 284 281 2thd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ) )
375 ltsubadd ⊢ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
376 181 375 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
377 376 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
378 377 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) )
379 374 378 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) ) )
380 elioomnf ⊢ ( 𝑥 ∈ ℝ* → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ) ) )
381 297 380 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ℝ ∧ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) < 𝑥 ) ) )
382 elioomnf ⊢ ( ( 𝑥 + 𝑦 ) ∈ ℝ* → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) ) )
383 293 382 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℝ ∧ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) < ( 𝑥 + 𝑦 ) ) ) )
384 379 381 383 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) )
385 301 eleq1d ⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ) )
386 385 bibi1d ⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ↔ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − 𝑦 ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ) )
387 384 386 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) = 𝑦 → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ↔ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ) )
388 387 pm5.32rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
389 388 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
390 280 389 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ↔ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) ) )
391 390 rabbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
392 311 ineq2d ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
393 267 mptpreima ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) }
394 393 317 ineq12i ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
395 inrab ⊢ ( { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
396 394 395 eqtri ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
397 392 396 eqtrdi ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
398 397 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ∈ ( -∞ (,) 𝑥 ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
399 311 ineq2d ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) )
400 324 mptpreima ⊢ ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) = { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) }
401 400 317 ineq12i ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } )
402 inrab ⊢ ( { 𝑡 ∈ ℝ ∣ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) } ∩ { 𝑡 ∈ ℝ ∣ ( 𝑓 ‘ 𝑡 ) = 𝑦 } ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
403 401 402 eqtri ⊢ ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) }
404 399 403 eqtrdi ⊢ ( 𝑓 ∈ dom ∫1 → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
405 404 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = { 𝑡 ∈ ℝ ∣ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ∧ ( 𝑓 ‘ 𝑡 ) = 𝑦 ) } )
406 391 398 405 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
407 406 iuneq2dv ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
408 373 407 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) = ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) )
409 mbfima ⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) : ℝ ⟶ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∈ dom vol )
410 351 353 409 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∈ dom vol )
411 inmbl ⊢ ( ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∈ dom vol ∧ ( ◡ 𝑓 “ { 𝑦 } ) ∈ dom vol ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
412 410 356 411 syl2an ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
413 412 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
414 finiunmbl ⊢ ( ( ran 𝑓 ∈ Fin ∧ ∀ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
415 335 413 414 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
416 415 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ∪ 𝑦 ∈ ran 𝑓 ( ( ◡ ( 𝑡 ∈ ℝ ↦ ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) “ ( -∞ (,) ( 𝑥 + 𝑦 ) ) ) ∩ ( ◡ 𝑓 “ { 𝑦 } ) ) ∈ dom vol )
417 408 416 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
418 256 257 363 417 ismbf2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ MblFn )
419 ftc1anclem1 ⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) : ℝ ⟶ ℝ ∧ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ∈ MblFn ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
420 256 418 419 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
421 252 420 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
422 421 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∈ MblFn )
423 157 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
424 174 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
425 422 217 423 223 424 itg2addnc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
426 249 425 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
427 426 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
428 itg2cl ⊢ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
429 207 428 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
430 429 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
431 readdcl ⊢ ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ )
432 157 174 431 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) ∧ ( 𝜑 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ )
433 432 anandis ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ )
434 433 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ* )
435 434 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ∈ ℝ* )
436 9 9 rpaddcld ⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ+ )
437 436 rpxrd ⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ* )
438 437 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ∈ ℝ* )
439 xrlelttr ⊢ ( ( ( ∫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 ) ) ) )
440 430 435 438 439 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 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 ) ) ) )
441 427 440 mpand ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ) )
442 180 441 syld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 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 ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ) → ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ )
444 13 191 443 sylancr ⊢ ( 𝜑 → ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ )
445 182 444 jca ⊢ ( 𝜑 → ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ ) )
446 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
447 13 194 446 sylancr ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
448 185 447 anim12i ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) )
449 448 anandirs ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) )
450 addsub4 ⊢ ( ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ∈ ℂ ) ∧ ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
451 445 449 450 syl2an ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
452 451 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
453 92 replimd ⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
454 453 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) )
455 454 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) + ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
456 194 adantll ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ )
457 subdi ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
458 13 191 456 457 mp3an3an ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
459 458 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) = ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
460 459 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( ( i · ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) − ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
461 452 455 460 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) = ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
462 461 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
463 462 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
464 463 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
465 464 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
466 rpcn ⊢ ( 𝑌 ∈ ℝ+ → 𝑌 ∈ ℂ )
467 466 2halvesd ⊢ ( 𝑌 ∈ ℝ+ → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) = 𝑌 )
468 467 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) = 𝑌 )
469 465 468 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) + ( i · ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( ( 𝑌 / 2 ) + ( 𝑌 / 2 ) ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
470 442 469 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
471 470 reximdvva ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ( ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
472 121 471 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ( ( ∃ 𝑓 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℜ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑓 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ∧ ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( ℑ ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) − ( 𝑔 ‘ 𝑡 ) ) ) ) ) < ( 𝑌 / 2 ) ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 ) )
473 11 120 472 mp2and ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < 𝑌 )