Metamath Proof Explorer

Theorem ftc1anclem7

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 13-May-2018)

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

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 i1ff ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
10 9 ffvelrnda ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
11 10 recnd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
12 ax-icn ⊢ i ∈ ℂ
13 i1ff ⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 : ℝ ⟶ ℝ )
14 13 ffvelrnda ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℂ )
16 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑥 ) ∈ ℂ ) → ( i · ( 𝑔 ‘ 𝑥 ) ) ∈ ℂ )
17 12 15 16 sylancr ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑥 ) ) ∈ ℂ )
18 addcl ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑥 ) ) ∈ ℂ ) → ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℂ )
19 11 17 18 syl2an ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℂ )
20 19 anandirs ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℂ )
21 reex ⊢ ℝ ∈ V
22 21 a1i ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ℝ ∈ V )
23 10 adantlr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
24 ovexd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑥 ) ) ∈ V )
25 9 feqmptd ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓 ‘ 𝑥 ) ) )
26 25 adantr ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓 ‘ 𝑥 ) ) )
27 21 a1i ⊢ ( 𝑔 ∈ dom ∫1 → ℝ ∈ V )
28 12 a1i ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → i ∈ ℂ )
29 fconstmpt ⊢ ( ℝ × { i } ) = ( 𝑥 ∈ ℝ ↦ i )
30 29 a1i ⊢ ( 𝑔 ∈ dom ∫1 → ( ℝ × { i } ) = ( 𝑥 ∈ ℝ ↦ i ) )
31 13 feqmptd ⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 = ( 𝑥 ∈ ℝ ↦ ( 𝑔 ‘ 𝑥 ) ) )
32 27 28 14 30 31 offval2 ⊢ ( 𝑔 ∈ dom ∫1 → ( ( ℝ × { i } ) ∘f · 𝑔 ) = ( 𝑥 ∈ ℝ ↦ ( i · ( 𝑔 ‘ 𝑥 ) ) ) )
33 32 adantl ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( ℝ × { i } ) ∘f · 𝑔 ) = ( 𝑥 ∈ ℝ ↦ ( i · ( 𝑔 ‘ 𝑥 ) ) ) )
34 22 23 24 26 33 offval2 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) )
35 absf ⊢ abs : ℂ ⟶ ℝ
36 35 a1i ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → abs : ℂ ⟶ ℝ )
37 36 feqmptd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → abs = ( 𝑡 ∈ ℂ ↦ ( abs ‘ 𝑡 ) ) )
38 fveq2 ⊢ ( 𝑡 = ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) → ( abs ‘ 𝑡 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) )
39 20 34 37 38 fmptco ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
40 ftc1anclem3 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ∈ dom ∫1 )
41 39 40 eqeltrrd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) ∈ dom ∫1 )
42 ioombl ⊢ ( 𝑢 (,) 𝑤 ) ∈ dom vol
43 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑡 ) )
44 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑡 ) )
45 44 oveq2d ⊢ ( 𝑥 = 𝑡 → ( i · ( 𝑔 ‘ 𝑥 ) ) = ( i · ( 𝑔 ‘ 𝑡 ) ) )
46 43 45 oveq12d ⊢ ( 𝑥 = 𝑡 → ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) = ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
47 46 fveq2d ⊢ ( 𝑥 = 𝑡 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
48 eqid ⊢ ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) )
49 fvex ⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ V
50 47 48 49 fvmpt ⊢ ( 𝑡 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) ‘ 𝑡 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
51 50 eqcomd ⊢ ( 𝑡 ∈ ℝ → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) ‘ 𝑡 ) )
52 51 ifeq1d ⊢ ( 𝑡 ∈ ℝ → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) ‘ 𝑡 ) , 0 ) )
53 52 mpteq2ia ⊢ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) ‘ 𝑡 ) , 0 ) )
54 53 i1fres ⊢ ( ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ) ) ∈ dom ∫1 ∧ ( 𝑢 (,) 𝑤 ) ∈ dom vol ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ dom ∫1 )
55 41 42 54 sylancl ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ dom ∫1 )
56 breq2 ⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ↔ 0 ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
57 breq2 ⊢ ( 0 = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
58 elioore ⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 𝑡 ∈ ℝ )
59 eleq1w ⊢ ( 𝑥 = 𝑡 → ( 𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ ) )
60 59 anbi2d ⊢ ( 𝑥 = 𝑡 → ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) ↔ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ) )
61 46 eleq1d ⊢ ( 𝑥 = 𝑡 → ( ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℂ ↔ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) )
62 60 61 imbi12d ⊢ ( 𝑥 = 𝑡 → ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑥 ) + ( i · ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℂ ) ↔ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) ) )
63 62 20 chvarvv ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
64 63 absge0d ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
65 58 64 sylan2 ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
66 0le0 ⊢ 0 ≤ 0
67 66 a1i ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ 0 )
68 56 57 65 67 ifbothda ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0 ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
69 68 ralrimivw ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ∀ 𝑡 ∈ ℝ 0 ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
70 ax-resscn ⊢ ℝ ⊆ ℂ
71 70 a1i ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ℝ ⊆ ℂ )
72 c0ex ⊢ 0 ∈ V
73 49 72 ifex ⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V
74 eqid ⊢ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
75 73 74 fnmpti ⊢ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) Fn ℝ
76 75 a1i ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) Fn ℝ )
77 71 76 0pledm ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) )
78 72 a1i ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ∈ V )
79 73 a1i ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V )
80 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑡 ∈ ℝ ↦ 0 )
81 80 a1i ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ℝ × { 0 } ) = ( 𝑡 ∈ ℝ ↦ 0 ) )
82 eqidd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
83 22 78 79 81 82 ofrfval2 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ 0 ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
84 77 83 bitrd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ 0 ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
85 69 84 mpbird ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
86 itg2itg1 ⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) )
87 itg1cl ⊢ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
88 87 adantr ⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) → ( ∫1 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
89 86 88 eqeltrd ⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
90 55 85 89 syl2anc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
91 90 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
92 simplll ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) )
93 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
94 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
95 93 94 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
96 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑡 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦 ) } )
97 96 elixx3g ⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) )
98 97 simprbi ⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) )
99 98 simpld ⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → 𝐴 ≤ 𝑢 )
100 96 elixx3g ⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵 ) ) )
101 100 simprbi ⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵 ) )
102 101 simprd ⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → 𝑤 ≤ 𝐵 )
103 99 102 anim12i ⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵 ) )
104 ioossioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵 ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
105 95 103 104 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
106 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
107 105 106 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ 𝐷 )
108 107 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑢 (,) 𝑤 ) ⊆ 𝐷 )
109 108 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 )
110 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
111 110 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
112 109 111 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
113 112 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
114 63 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
115 58 114 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
116 115 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
117 113 116 subcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
118 117 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
119 118 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
120 117 absge0d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
121 elxrge0 ⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
122 119 120 121 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
123 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
124 123 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) )
125 122 124 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
126 125 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
127 126 fmpttd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
128 92 127 sylan ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
129 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
130 129 rehalfcld ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
131 130 ad2antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑦 / 2 ) ∈ ℝ )
132 simpll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) )
133 107 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 )
134 133 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 )
135 110 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
136 6 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 𝑡 ∈ ℝ )
137 136 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → 𝑡 ∈ ℝ )
138 137 114 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
139 135 138 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
140 139 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
141 140 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
142 141 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
143 134 142 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
144 139 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
145 144 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
146 134 145 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
147 143 146 121 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
148 123 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) )
149 147 148 ifclda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
150 149 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
151 150 fmpttd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
152 itg2cl ⊢ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
153 151 152 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
154 132 153 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
155 rphalfcl ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
156 155 rpxrd ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ* )
157 156 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑦 / 2 ) ∈ ℝ* )
158 0cnd ⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℂ )
159 110 158 ifclda ⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ )
160 subcl ⊢ ( ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ ∧ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
161 159 63 160 syl2an ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
162 161 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
163 162 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
164 163 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
165 162 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
166 elxrge0 ⊢ ( ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
167 164 165 166 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
168 167 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
169 itg2cl ⊢ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
170 168 169 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
171 170 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) ∈ ℝ* )
172 168 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
173 breq1 ⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
174 breq1 ⊢ ( 0 = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
175 140 leidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
176 iftrue ⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) = ( 𝐹 ‘ 𝑡 ) )
177 176 fvoveq1d ⊢ ( 𝑡 ∈ 𝐷 → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
178 177 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
179 175 178 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
180 179 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
181 134 180 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
182 181 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
183 165 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
184 183 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
185 173 174 182 184 ifbothda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
186 185 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
187 21 a1i ⊢ ( 𝜑 → ℝ ∈ V )
188 fvex ⊢ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ V
189 188 72 ifex ⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ V
190 189 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ V )
191 fvexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ V )
192 eqidd ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
193 eqidd ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
194 187 190 191 192 193 ofrfval2 ⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
195 194 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
196 186 195 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
197 itg2le ⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
198 151 172 196 197 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
199 132 198 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) )
200 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) )
201 154 171 157 199 200 xrlelttrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
202 154 157 201 xrltled ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( 𝑦 / 2 ) )
203 202 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( 𝑦 / 2 ) )
204 203 3adantr3 ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( 𝑦 / 2 ) )
205 itg2lecl ⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑦 / 2 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( 𝑦 / 2 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ )
206 128 131 204 205 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ )
207 206 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ )
208 130 ad3antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( 𝑦 / 2 ) ∈ ℝ )
209 90 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
210 2rp ⊢ 2 ∈ ℝ+
211 imassrn ⊢ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ran abs
212 frn ⊢ ( abs : ℂ ⟶ ℝ → ran abs ⊆ ℝ )
213 35 212 ax-mp ⊢ ran abs ⊆ ℝ
214 211 213 sstri ⊢ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ
215 214 a1i ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ )
216 9 frnd ⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ )
217 216 adantr ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ran 𝑓 ⊆ ℝ )
218 13 frnd ⊢ ( 𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ )
219 218 adantl ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ran 𝑔 ⊆ ℝ )
220 217 219 unssd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℝ )
221 220 70 sstrdi ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ )
222 i1f0rn ⊢ ( 𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓 )
223 elun1 ⊢ ( 0 ∈ ran 𝑓 → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
224 222 223 syl ⊢ ( 𝑓 ∈ dom ∫1 → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
225 224 adantr ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
226 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
227 35 226 ax-mp ⊢ abs Fn ℂ
228 fnfvima ⊢ ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
229 227 228 mp3an1 ⊢ ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
230 221 225 229 syl2anc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
231 230 ne0d ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ )
232 ffun ⊢ ( abs : ℂ ⟶ ℝ → Fun abs )
233 35 232 ax-mp ⊢ Fun abs
234 i1frn ⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin )
235 i1frn ⊢ ( 𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin )
236 unfi ⊢ ( ( ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin ) → ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin )
237 234 235 236 syl2an ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin )
238 imafi ⊢ ( ( Fun abs ∧ ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin )
239 233 237 238 sylancr ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin )
240 fimaxre2 ⊢ ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 )
241 214 239 240 sylancr ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 )
242 suprcl ⊢ ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
243 215 231 241 242 syl3anc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
244 243 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
245 0red ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 ∈ ℝ )
246 221 sselda ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → 𝑟 ∈ ℂ )
247 246 abscld ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ℝ )
248 247 adantrr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → ( abs ‘ 𝑟 ) ∈ ℝ )
249 absgt0 ⊢ ( 𝑟 ∈ ℂ → ( 𝑟 ≠ 0 ↔ 0 < ( abs ‘ 𝑟 ) ) )
250 246 249 syl ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( 𝑟 ≠ 0 ↔ 0 < ( abs ‘ 𝑟 ) ) )
251 250 biimpa ⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) ∧ 𝑟 ≠ 0 ) → 0 < ( abs ‘ 𝑟 ) )
252 251 anasss ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 < ( abs ‘ 𝑟 ) )
253 215 231 241 3jca ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) )
254 253 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) )
255 fnfvima ⊢ ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
256 227 255 mp3an1 ⊢ ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
257 221 256 sylan ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
258 suprub ⊢ ( ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ∧ ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
259 254 257 258 syl2anc ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
260 259 adantrr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
261 245 248 244 252 260 ltletrd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
262 244 261 elrpd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ )
263 262 rexlimdvaa ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ ) )
264 263 imp ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ )
265 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
266 210 264 265 sylancr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
267 209 266 rerpdivcld ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
268 267 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
269 268 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
270 269 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
271 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → 𝜑 )
272 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
273 2 3 272 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
274 273 70 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
275 274 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℂ )
276 274 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℂ )
277 subcl ⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( 𝑤 − 𝑢 ) ∈ ℂ )
278 275 276 277 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑤 − 𝑢 ) ∈ ℂ )
279 278 anandis ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑤 − 𝑢 ) ∈ ℂ )
280 279 abscld ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) ∈ ℝ )
281 280 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) ∈ ℝ )
282 271 281 sylan ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) ∈ ℝ )
283 282 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) ∈ ℝ )
284 rpdivcl ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ )
285 155 266 284 syl2anr ⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ )
286 285 rpred ⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
287 286 adantlll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
288 287 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
289 288 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ )
290 273 sseld ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → 𝑢 ∈ ℝ ) )
291 273 sseld ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → 𝑤 ∈ ℝ ) )
292 idd ⊢ ( 𝜑 → ( 𝑢 ≤ 𝑤 → 𝑢 ≤ 𝑤 ) )
293 290 291 292 3anim123d ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) → ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) )
294 293 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) → ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) )
295 294 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) )
296 63 abscld ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ )
297 296 rexrd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ* )
298 elxrge0 ⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
299 297 64 298 sylanbrc ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) )
300 ifcl ⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
301 299 123 300 sylancl ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
302 301 fmpttd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
303 243 recnd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℂ )
304 303 2timesd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) = ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
305 243 243 readdcld ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ )
306 305 rexrd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ* )
307 abs0 ⊢ ( abs ‘ 0 ) = 0
308 307 230 eqeltrrid ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
309 suprub ⊢ ( ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ∧ 0 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) → 0 ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
310 253 308 309 syl2anc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0 ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
311 243 243 310 310 addge0d ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0 ≤ ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
312 elxrge0 ⊢ ( ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ* ∧ 0 ≤ ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) )
313 306 311 312 sylanbrc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,] +∞ ) )
314 304 313 eqeltrd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,] +∞ ) )
315 ifcl ⊢ ( ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
316 314 123 315 sylancl ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
317 316 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
318 317 fmpttd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
319 9 ffvelrnda ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
320 319 recnd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℂ )
321 320 abscld ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
322 13 ffvelrnda ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
323 322 recnd ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ )
324 323 abscld ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ )
325 readdcl ⊢ ( ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
326 321 324 325 syl2an ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
327 326 anandirs ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
328 305 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ )
329 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
330 12 323 329 sylancr ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
331 abstri ⊢ ( ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
332 320 330 331 syl2an ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
333 332 anandirs ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
334 absmul ⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
335 12 323 334 sylancr ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
336 absi ⊢ ( abs ‘ i ) = 1
337 336 oveq1i ⊢ ( ( abs ‘ i ) · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) = ( 1 · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
338 335 337 eqtrdi ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( 1 · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
339 324 recnd ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
340 339 mulid2d ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 1 · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
341 338 340 eqtrd ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
342 341 adantll ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
343 342 oveq2d ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
344 333 343 breqtrd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
345 321 adantlr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
346 324 adantll ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ )
347 243 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
348 253 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) )
349 221 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ )
350 9 ffnd ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 Fn ℝ )
351 fnfvelrn ⊢ ( ( 𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ran 𝑓 )
352 350 351 sylan ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ran 𝑓 )
353 elun1 ⊢ ( ( 𝑓 ‘ 𝑡 ) ∈ ran 𝑓 → ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
354 352 353 syl ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
355 354 adantlr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
356 fnfvima ⊢ ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
357 227 356 mp3an1 ⊢ ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
358 349 355 357 syl2anc ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
359 suprub ⊢ ( ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ∧ ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
360 348 358 359 syl2anc ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
361 13 ffnd ⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ )
362 fnfvelrn ⊢ ( ( 𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ran 𝑔 )
363 361 362 sylan ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ran 𝑔 )
364 elun2 ⊢ ( ( 𝑔 ‘ 𝑡 ) ∈ ran 𝑔 → ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
365 363 364 syl ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
366 365 adantll ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
367 fnfvima ⊢ ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
368 227 367 mp3an1 ⊢ ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
369 349 366 368 syl2anc ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
370 suprub ⊢ ( ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ∧ ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
371 348 369 370 syl2anc ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
372 345 346 347 347 360 371 le2addd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ≤ ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
373 296 327 328 344 372 letrd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
374 304 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) = ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
375 373 374 breqtrrd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
376 58 375 sylan2 ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
377 iftrue ⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
378 377 adantl ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
379 iftrue ⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) = ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
380 379 adantl ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) = ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
381 376 378 380 3brtr4d ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) )
382 381 ex ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) )
383 66 a1i ⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 0 ≤ 0 )
384 iffalse ⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = 0 )
385 iffalse ⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) = 0 )
386 383 384 385 3brtr4d ⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) )
387 382 386 pm2.61d1 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) )
388 387 ralrimivw ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) )
389 ovex ⊢ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ V
390 389 72 ifex ⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ∈ V
391 390 a1i ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ∈ V )
392 eqidd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) )
393 22 79 391 82 392 ofrfval2 ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) )
394 388 393 mpbird ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) )
395 itg2le ⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) )
396 302 318 394 395 syl3anc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) )
397 396 adantr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) )
398 mblvol ⊢ ( ( 𝑢 (,) 𝑤 ) ∈ dom vol → ( vol ‘ ( 𝑢 (,) 𝑤 ) ) = ( vol* ‘ ( 𝑢 (,) 𝑤 ) ) )
399 42 398 ax-mp ⊢ ( vol ‘ ( 𝑢 (,) 𝑤 ) ) = ( vol* ‘ ( 𝑢 (,) 𝑤 ) )
400 ovolioo ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( vol* ‘ ( 𝑢 (,) 𝑤 ) ) = ( 𝑤 − 𝑢 ) )
401 399 400 syl5eq ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( vol ‘ ( 𝑢 (,) 𝑤 ) ) = ( 𝑤 − 𝑢 ) )
402 resubcl ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑢 ∈ ℝ ) → ( 𝑤 − 𝑢 ) ∈ ℝ )
403 402 ancoms ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( 𝑤 − 𝑢 ) ∈ ℝ )
404 403 3adant3 ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( 𝑤 − 𝑢 ) ∈ ℝ )
405 401 404 eqeltrd ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ∈ ℝ )
406 elrege0 ⊢ ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ( 0 [,) +∞ ) ↔ ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ ∧ 0 ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
407 243 310 406 sylanbrc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ( 0 [,) +∞ ) )
408 ge0addcl ⊢ ( ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ( 0 [,) +∞ ) ∧ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ( 0 [,) +∞ ) ) → ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,) +∞ ) )
409 407 407 408 syl2anc ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) + sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,) +∞ ) )
410 304 409 eqeltrd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,) +∞ ) )
411 itg2const ⊢ ( ( ( 𝑢 (,) 𝑤 ) ∈ dom vol ∧ ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ∈ ℝ ∧ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) = ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) )
412 42 411 mp3an1 ⊢ ( ( ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ∈ ℝ ∧ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) = ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) )
413 405 410 412 syl2anr ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) , 0 ) ) ) = ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) )
414 397 413 breqtrd ⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) )
415 414 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) )
416 415 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) )
417 90 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
418 405 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ∈ ℝ )
419 266 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
420 419 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
421 417 418 420 ledivmuld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) · ( vol ‘ ( 𝑢 (,) 𝑤 ) ) ) ) )
422 416 421 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( vol ‘ ( 𝑢 (,) 𝑤 ) ) )
423 abssubge0 ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) = ( 𝑤 − 𝑢 ) )
424 400 423 eqtr4d ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( vol* ‘ ( 𝑢 (,) 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝑢 ) ) )
425 399 424 syl5eq ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) → ( vol ‘ ( 𝑢 (,) 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝑢 ) ) )
426 425 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( vol ‘ ( 𝑢 (,) 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝑢 ) ) )
427 422 426 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( abs ‘ ( 𝑤 − 𝑢 ) ) )
428 295 427 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( abs ‘ ( 𝑤 − 𝑢 ) ) )
429 428 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( abs ‘ ( 𝑤 − 𝑢 ) ) )
430 429 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( abs ‘ ( 𝑤 − 𝑢 ) ) )
431 430 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ≤ ( abs ‘ ( 𝑤 − 𝑢 ) ) )
432 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) )
433 270 283 289 431 432 lelttrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) )
434 90 adantl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
435 434 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
436 130 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ )
437 419 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
438 437 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
439 435 436 438 ltdiv1d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ↔ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) )
440 439 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ↔ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) )
441 433 440 mpbird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
442 201 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
443 442 3adantr3 ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
444 443 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
445 91 207 208 208 441 444 lt2addd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) < ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) )