Metamath Proof Explorer

Theorem ftc1anclem4

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 17-Jun-2018)

Ref Expression
Assertion ftc1anclem4 ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ffvelrn ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
2 1 recnd ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝐺 ‘ 𝑡 ) ∈ ℂ )
3 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
4 3 ffvelrnda ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
5 4 recnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
6 subcl ⊢ ( ( ( 𝐺 ‘ 𝑡 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
7 2 5 6 syl2anr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) ) → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
8 7 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
9 8 abscld ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
10 9 rexrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ* )
11 8 absge0d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) )
12 elxrge0 ⊢ ( ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) )
13 10 11 12 sylanbrc ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,] +∞ ) )
14 13 fmpttd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
15 14 3adant2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
16 reex ⊢ ℝ ∈ V
17 16 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ℝ ∈ V )
18 fvexd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ V )
19 fvexd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ V )
20 eqidd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
21 eqidd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
22 17 18 19 20 21 offval2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
23 22 fveq2d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
24 id ⊢ ( 𝐺 : ℝ ⟶ ℝ → 𝐺 : ℝ ⟶ ℝ )
25 24 feqmptd ⊢ ( 𝐺 : ℝ ⟶ ℝ → 𝐺 = ( 𝑡 ∈ ℝ ↦ ( 𝐺 ‘ 𝑡 ) ) )
26 absf ⊢ abs : ℂ ⟶ ℝ
27 26 a1i ⊢ ( 𝐺 : ℝ ⟶ ℝ → abs : ℂ ⟶ ℝ )
28 27 feqmptd ⊢ ( 𝐺 : ℝ ⟶ ℝ → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
29 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑡 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) )
30 2 25 28 29 fmptco ⊢ ( 𝐺 : ℝ ⟶ ℝ → ( abs ∘ 𝐺 ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
31 30 adantl ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( abs ∘ 𝐺 ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
32 iblmbf ⊢ ( 𝐺 ∈ 𝐿1 → 𝐺 ∈ MblFn )
33 ftc1anclem1 ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝐺 ∈ MblFn ) → ( abs ∘ 𝐺 ) ∈ MblFn )
34 32 33 sylan2 ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝐺 ∈ 𝐿1 ) → ( abs ∘ 𝐺 ) ∈ MblFn )
35 34 ancoms ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( abs ∘ 𝐺 ) ∈ MblFn )
36 31 35 eqeltrrd ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ MblFn )
37 36 3adant1 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ MblFn )
38 2 abscld ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ )
39 2 absge0d ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) )
40 elrege0 ⊢ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
41 38 39 40 sylanbrc ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) )
42 41 fmpttd ⊢ ( 𝐺 : ℝ ⟶ ℝ → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
43 42 3ad2ant3 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
44 iftrue ⊢ ( 𝑡 ∈ ℝ → if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) , 0 ) = ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) )
45 44 mpteq2ia ⊢ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) )
46 45 fveq2i ⊢ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
47 1 adantll ⊢ ( ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
48 simpr ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → 𝐺 : ℝ ⟶ ℝ )
49 48 feqmptd ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → 𝐺 = ( 𝑡 ∈ ℝ ↦ ( 𝐺 ‘ 𝑡 ) ) )
50 simpl ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → 𝐺 ∈ 𝐿1 )
51 49 50 eqeltrrd ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( 𝐺 ‘ 𝑡 ) ) ∈ 𝐿1 )
52 47 51 36 iblabsnc ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐿1 )
53 38 adantll ⊢ ( ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ )
54 39 adantll ⊢ ( ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) )
55 53 54 iblpos ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐿1 ↔ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ ) ) )
56 52 55 mpbid ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ ) )
57 56 simprd ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ )
58 46 57 eqeltrrid ⊢ ( ( 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ∈ ℝ )
59 58 3adant1 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ∈ ℝ )
60 5 abscld ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
61 5 absge0d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
62 elrege0 ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
63 60 61 62 sylanbrc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) )
64 63 fmpttd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
65 64 3ad2ant1 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
66 iftrue ⊢ ( 𝑡 ∈ ℝ → if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
67 66 mpteq2ia ⊢ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
68 67 fveq2i ⊢ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
69 3 feqmptd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 = ( 𝑡 ∈ ℝ ↦ ( 𝐹 ‘ 𝑡 ) ) )
70 i1fibl ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1 )
71 69 70 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑡 ∈ ℝ ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
72 26 a1i ⊢ ( 𝐹 ∈ dom ∫1 → abs : ℂ ⟶ ℝ )
73 72 feqmptd ⊢ ( 𝐹 ∈ dom ∫1 → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
74 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑡 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
75 5 69 73 74 fmptco ⊢ ( 𝐹 ∈ dom ∫1 → ( abs ∘ 𝐹 ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
76 i1fmbf ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn )
77 ftc1anclem1 ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝐹 ∈ MblFn ) → ( abs ∘ 𝐹 ) ∈ MblFn )
78 3 76 77 syl2anc ⊢ ( 𝐹 ∈ dom ∫1 → ( abs ∘ 𝐹 ) ∈ MblFn )
79 75 78 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn )
80 4 71 79 iblabsnc ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐿1 )
81 60 61 iblpos ⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐿1 ↔ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ ) ) )
82 80 81 mpbid ⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ ) )
83 82 simprd ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ℝ , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ )
84 68 83 eqeltrrid ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ∈ ℝ )
85 84 3ad2ant1 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ∈ ℝ )
86 37 43 59 65 85 itg2addnc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∘f + ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) = ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
87 23 86 eqtr3d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) = ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
88 59 85 readdcld ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
89 87 88 eqeltrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
90 readdcl ⊢ ( ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ) → ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
91 38 60 90 syl2anr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
92 91 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
93 92 rexrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ* )
94 38 adantll ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ )
95 60 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
96 39 adantll ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) )
97 61 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
98 94 95 96 97 addge0d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
99 elxrge0 ⊢ ( ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ* ∧ 0 ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
100 93 98 99 sylanbrc ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,] +∞ ) )
101 100 fmpttd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
102 101 3adant2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
103 abs2dif2 ⊢ ( ( ( 𝐺 ‘ 𝑡 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
104 2 5 103 syl2anr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
105 104 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
106 105 ralrimiva ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ∀ 𝑡 ∈ ℝ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
107 16 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ℝ ∈ V )
108 eqidd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) )
109 eqidd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
110 107 9 92 108 109 ofrfval2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ↔ ∀ 𝑡 ∈ ℝ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
111 106 110 mpbird ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
112 111 3adant2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
113 itg2le ⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
114 15 102 112 113 syl3anc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
115 itg2lecl ⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝐺 ‘ 𝑡 ) ) + ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
116 15 89 114 115 syl3anc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺 : ℝ ⟶ ℝ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )