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