Metamath Proof Explorer


Theorem ftc1anc

Description: ftc1a holds for functions that obey the triangle inequality in the absence of ax-cc . Theorem 565Ma of Fremlin5 p. 220. (Contributed by Brendan Leahy, 11-May-2018)

Ref Expression
Hypotheses ftc1anc.g 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹𝑡 ) d 𝑡 )
ftc1anc.a ( 𝜑𝐴 ∈ ℝ )
ftc1anc.b ( 𝜑𝐵 ∈ ℝ )
ftc1anc.le ( 𝜑𝐴𝐵 )
ftc1anc.s ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
ftc1anc.d ( 𝜑𝐷 ⊆ ℝ )
ftc1anc.i ( 𝜑𝐹 ∈ 𝐿1 )
ftc1anc.f ( 𝜑𝐹 : 𝐷 ⟶ ℂ )
ftc1anc.t ( 𝜑 → ∀ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ( abs ‘ ∫ 𝑠 ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
Assertion ftc1anc ( 𝜑𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )

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 ftc1anc.t ( 𝜑 → ∀ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ( abs ‘ ∫ 𝑠 ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
10 1 2 3 4 5 6 7 8 ftc1lem2 ( 𝜑𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
11 rphalfcl ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
12 1 2 3 4 5 6 7 8 ftc1anclem6 ( ( 𝜑 ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) )
13 11 12 sylan2 ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) )
14 13 adantrl ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) )
15 11 ad2antll ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑦 / 2 ) ∈ ℝ+ )
16 2rp 2 ∈ ℝ+
17 i1ff ( 𝑓 ∈ dom ∫1𝑓 : ℝ ⟶ ℝ )
18 17 frnd ( 𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ )
19 18 adantr ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ran 𝑓 ⊆ ℝ )
20 i1ff ( 𝑔 ∈ dom ∫1𝑔 : ℝ ⟶ ℝ )
21 20 frnd ( 𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ )
22 21 adantl ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ran 𝑔 ⊆ ℝ )
23 19 22 unssd ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℝ )
24 ax-resscn ℝ ⊆ ℂ
25 23 24 sstrdi ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ )
26 i1f0rn ( 𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓 )
27 elun1 ( 0 ∈ ran 𝑓 → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
28 26 27 syl ( 𝑓 ∈ dom ∫1 → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
29 28 adantr ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
30 absf abs : ℂ ⟶ ℝ
31 ffn ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
32 30 31 ax-mp abs Fn ℂ
33 fnfvima ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
34 32 33 mp3an1 ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
35 25 29 34 syl2anc ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
36 35 ne0d ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ )
37 imassrn ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ran abs
38 frn ( abs : ℂ ⟶ ℝ → ran abs ⊆ ℝ )
39 30 38 ax-mp ran abs ⊆ ℝ
40 37 39 sstri ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ
41 ffun ( abs : ℂ ⟶ ℝ → Fun abs )
42 30 41 ax-mp Fun abs
43 i1frn ( 𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin )
44 i1frn ( 𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin )
45 unfi ( ( ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin ) → ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin )
46 43 44 45 syl2an ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin )
47 imafi ( ( Fun abs ∧ ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin )
48 42 46 47 sylancr ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin )
49 fimaxre2 ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 )
50 40 48 49 sylancr ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 )
51 suprcl ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
52 40 51 mp3an1 ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
53 36 50 52 syl2anc ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
54 53 adantr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
55 0red ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 ∈ ℝ )
56 25 sselda ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → 𝑟 ∈ ℂ )
57 56 abscld ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ℝ )
58 57 adantrr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → ( abs ‘ 𝑟 ) ∈ ℝ )
59 53 adantr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ )
60 absgt0 ( 𝑟 ∈ ℂ → ( 𝑟 ≠ 0 ↔ 0 < ( abs ‘ 𝑟 ) ) )
61 56 60 syl ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( 𝑟 ≠ 0 ↔ 0 < ( abs ‘ 𝑟 ) ) )
62 61 biimpd ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( 𝑟 ≠ 0 → 0 < ( abs ‘ 𝑟 ) ) )
63 62 impr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 < ( abs ‘ 𝑟 ) )
64 40 a1i ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ )
65 64 36 50 3jca ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 ) )
66 65 adantr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 ) )
67 fnfvima ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
68 32 67 mp3an1 ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
69 25 68 sylan ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) )
70 suprub ( ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦𝑥 ) ∧ ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
71 66 69 70 syl2anc ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
72 71 adantrr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
73 55 58 59 63 72 ltletrd ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
74 73 rexlimdvaa ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) → ( ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) )
75 74 imp ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) )
76 54 75 elrpd ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ )
77 rpmulcl ( ( 2 ∈ ℝ+ ∧ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
78 16 76 77 sylancr ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ )
79 rpdivcl ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ )
80 15 78 79 syl2an ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ )
81 80 anassrs ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ )
82 81 adantlr ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ )
83 ancom ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ↔ ( 𝑦 ∈ ℝ+𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) )
84 83 anbi2i ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ+𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
85 an32 ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ↔ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) )
86 85 anbi1i ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) )
87 an32 ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) )
88 86 87 bitri ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) )
89 88 anbi1i ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) )
90 an32 ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) )
91 89 90 bitri ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) )
92 anass ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ+𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
93 84 91 92 3bitr4i ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) )
94 oveq12 ( ( 𝑏 = 𝑤𝑎 = 𝑢 ) → ( 𝑏𝑎 ) = ( 𝑤𝑢 ) )
95 94 ancoms ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( 𝑏𝑎 ) = ( 𝑤𝑢 ) )
96 95 fveq2d ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( abs ‘ ( 𝑏𝑎 ) ) = ( abs ‘ ( 𝑤𝑢 ) ) )
97 96 breq1d ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( ( abs ‘ ( 𝑏𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ↔ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) )
98 fveq2 ( 𝑏 = 𝑤 → ( 𝐺𝑏 ) = ( 𝐺𝑤 ) )
99 fveq2 ( 𝑎 = 𝑢 → ( 𝐺𝑎 ) = ( 𝐺𝑢 ) )
100 98 99 oveqan12rd ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) = ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) )
101 100 fveq2d ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( abs ‘ ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) ) = ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) )
102 101 breq1d ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( ( abs ‘ ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
103 97 102 imbi12d ( ( 𝑎 = 𝑢𝑏 = 𝑤 ) → ( ( ( abs ‘ ( 𝑏𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) )
104 oveq12 ( ( 𝑏 = 𝑢𝑎 = 𝑤 ) → ( 𝑏𝑎 ) = ( 𝑢𝑤 ) )
105 104 ancoms ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( 𝑏𝑎 ) = ( 𝑢𝑤 ) )
106 105 fveq2d ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( abs ‘ ( 𝑏𝑎 ) ) = ( abs ‘ ( 𝑢𝑤 ) ) )
107 106 breq1d ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( ( abs ‘ ( 𝑏𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ↔ ( abs ‘ ( 𝑢𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) )
108 fveq2 ( 𝑏 = 𝑢 → ( 𝐺𝑏 ) = ( 𝐺𝑢 ) )
109 fveq2 ( 𝑎 = 𝑤 → ( 𝐺𝑎 ) = ( 𝐺𝑤 ) )
110 108 109 oveqan12rd ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) = ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) )
111 110 fveq2d ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( abs ‘ ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) ) = ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) )
112 111 breq1d ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( ( abs ‘ ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) < 𝑦 ) )
113 107 112 imbi12d ( ( 𝑎 = 𝑤𝑏 = 𝑢 ) → ( ( ( abs ‘ ( 𝑏𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑏 ) − ( 𝐺𝑎 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑢𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) < 𝑦 ) ) )
114 iccssre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
115 2 3 114 syl2anc ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
116 115 ad4antr ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
117 simp-4l ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → 𝜑 )
118 115 24 sstrdi ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
119 118 sselda ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℂ )
120 118 sselda ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℂ )
121 abssub ( ( 𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( abs ‘ ( 𝑤𝑢 ) ) = ( abs ‘ ( 𝑢𝑤 ) ) )
122 119 120 121 syl2anr ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑤𝑢 ) ) = ( abs ‘ ( 𝑢𝑤 ) ) )
123 122 anandis ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑤𝑢 ) ) = ( abs ‘ ( 𝑢𝑤 ) ) )
124 123 breq1d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ↔ ( abs ‘ ( 𝑢𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) )
125 10 ffvelrnda ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺𝑤 ) ∈ ℂ )
126 10 ffvelrnda ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺𝑢 ) ∈ ℂ )
127 abssub ( ( ( 𝐺𝑤 ) ∈ ℂ ∧ ( 𝐺𝑢 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) = ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) )
128 125 126 127 syl2anr ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) = ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) )
129 128 anandis ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) = ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) )
130 129 breq1d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) < 𝑦 ) )
131 124 130 imbi12d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑢𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) < 𝑦 ) ) )
132 117 131 sylan ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑢𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) < 𝑦 ) ) )
133 2 rexrd ( 𝜑𝐴 ∈ ℝ* )
134 3 rexrd ( 𝜑𝐵 ∈ ℝ* )
135 133 134 jca ( 𝜑 → ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) )
136 df-icc [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑡 ∈ ℝ* ∣ ( 𝑥𝑡𝑡𝑦 ) } )
137 136 elixx3g ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑢 ∈ ℝ* ) ∧ ( 𝐴𝑢𝑢𝐵 ) ) )
138 137 simprbi ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴𝑢𝑢𝐵 ) )
139 138 simpld ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → 𝐴𝑢 )
140 136 elixx3g ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ* ) ∧ ( 𝐴𝑤𝑤𝐵 ) ) )
141 140 simprbi ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴𝑤𝑤𝐵 ) )
142 141 simprd ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → 𝑤𝐵 )
143 139 142 anim12i ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴𝑢𝑤𝐵 ) )
144 ioossioo ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐴𝑢𝑤𝐵 ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
145 135 143 144 syl2an ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
146 5 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
147 145 146 sstrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ 𝐷 )
148 147 sselda ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡𝐷 )
149 8 ffvelrnda ( ( 𝜑𝑡𝐷 ) → ( 𝐹𝑡 ) ∈ ℂ )
150 149 abscld ( ( 𝜑𝑡𝐷 ) → ( abs ‘ ( 𝐹𝑡 ) ) ∈ ℝ )
151 150 rexrd ( ( 𝜑𝑡𝐷 ) → ( abs ‘ ( 𝐹𝑡 ) ) ∈ ℝ* )
152 149 absge0d ( ( 𝜑𝑡𝐷 ) → 0 ≤ ( abs ‘ ( 𝐹𝑡 ) ) )
153 elxrge0 ( ( abs ‘ ( 𝐹𝑡 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( 𝐹𝑡 ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( 𝐹𝑡 ) ) ) )
154 151 152 153 sylanbrc ( ( 𝜑𝑡𝐷 ) → ( abs ‘ ( 𝐹𝑡 ) ) ∈ ( 0 [,] +∞ ) )
155 154 adantlr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡𝐷 ) → ( abs ‘ ( 𝐹𝑡 ) ) ∈ ( 0 [,] +∞ ) )
156 148 155 syldan ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( 𝐹𝑡 ) ) ∈ ( 0 [,] +∞ ) )
157 0e0iccpnf 0 ∈ ( 0 [,] +∞ )
158 157 a1i ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) )
159 156 158 ifclda ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
160 159 adantr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
161 160 fmpttd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
162 itg2cl ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
163 161 162 syl ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
164 163 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
165 117 164 sylan ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
166 165 adantr ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
167 simplll ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) )
168 149 adantlr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡𝐷 ) → ( 𝐹𝑡 ) ∈ ℂ )
169 148 168 syldan ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹𝑡 ) ∈ ℂ )
170 169 adantllr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹𝑡 ) ∈ ℂ )
171 elioore ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 𝑡 ∈ ℝ )
172 17 ffvelrnda ( ( 𝑓 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑓𝑡 ) ∈ ℝ )
173 172 recnd ( ( 𝑓 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑓𝑡 ) ∈ ℂ )
174 ax-icn i ∈ ℂ
175 20 ffvelrnda ( ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑔𝑡 ) ∈ ℝ )
176 175 recnd ( ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑔𝑡 ) ∈ ℂ )
177 mulcl ( ( i ∈ ℂ ∧ ( 𝑔𝑡 ) ∈ ℂ ) → ( i · ( 𝑔𝑡 ) ) ∈ ℂ )
178 174 176 177 sylancr ( ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) → ( i · ( 𝑔𝑡 ) ) ∈ ℂ )
179 addcl ( ( ( 𝑓𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔𝑡 ) ) ∈ ℂ ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ∈ ℂ )
180 173 178 179 syl2an ( ( ( 𝑓 ∈ dom ∫1𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ∈ ℂ )
181 180 anandirs ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ∈ ℂ )
182 171 181 sylan2 ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ∈ ℂ )
183 182 adantll ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ∈ ℂ )
184 183 adantlr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ∈ ℂ )
185 170 184 subcld ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ∈ ℂ )
186 185 abscld ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ ℝ )
187 182 abscld ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ∈ ℝ )
188 187 adantll ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ∈ ℝ )
189 188 adantlr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ∈ ℝ )
190 186 189 readdcld ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ ℝ )
191 190 rexrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ ℝ* )
192 185 absge0d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) )
193 181 absge0d ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) )
194 171 193 sylan2 ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) )
195 194 adantll ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) )
196 195 adantlr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) )
197 186 189 192 196 addge0d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) )
198 elxrge0 ( ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) )
199 191 197 198 sylanbrc ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
200 157 a1i ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) )
201 199 200 ifclda ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
202 201 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
203 202 fmpttd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
204 itg2cl ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
205 203 204 syl ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
206 205 3adantr3 ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
207 167 206 sylan ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
208 207 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 · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* )
209 rpxr ( 𝑦 ∈ ℝ+𝑦 ∈ ℝ* )
210 209 ad3antlr ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → 𝑦 ∈ ℝ* )
211 159 adantlr ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
212 211 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
213 212 fmpttd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
214 170 184 npcand ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) + ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) = ( 𝐹𝑡 ) )
215 214 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) + ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) = ( abs ‘ ( 𝐹𝑡 ) ) )
216 185 184 abstrid ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) + ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) )
217 215 216 eqbrtrrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( 𝐹𝑡 ) ) ≤ ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) )
218 iftrue ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) = ( abs ‘ ( 𝐹𝑡 ) ) )
219 218 adantl ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) = ( abs ‘ ( 𝐹𝑡 ) ) )
220 iftrue ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) = ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) )
221 220 adantl ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) = ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) )
222 217 219 221 3brtr4d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) )
223 222 ex ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) )
224 0le0 0 ≤ 0
225 224 a1i ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 0 ≤ 0 )
226 iffalse ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) = 0 )
227 iffalse ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) = 0 )
228 225 226 227 3brtr4d ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) )
229 223 228 pm2.61d1 ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) )
230 229 ralrimivw ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) )
231 reex ℝ ∈ V
232 231 a1i ( 𝜑 → ℝ ∈ V )
233 fvex ( abs ‘ ( 𝐹𝑡 ) ) ∈ V
234 c0ex 0 ∈ V
235 233 234 ifex if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ V
236 235 a1i ( ( 𝜑𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ V )
237 ovex ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ∈ V
238 237 234 ifex if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ∈ V
239 238 a1i ( ( 𝜑𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ∈ V )
240 eqidd ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
241 eqidd ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) )
242 232 236 239 240 241 ofrfval2 ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) )
243 242 ad2antrr ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) )
244 230 243 mpbird ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) )
245 itg2le ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) )
246 213 203 244 245 syl3anc ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) )
247 246 3adantr3 ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) )
248 167 247 sylan ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) )
249 248 adantr ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) )
250 1 2 3 4 5 6 7 8 ftc1anclem8 ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹𝑡 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) , 0 ) ) ) < 𝑦 )
251 166 208 210 249 250 xrlelttrd ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < 𝑦 )
252 simplll ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → 𝜑 )
253 simpr2 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑤 ∈ ( 𝐴 [,] 𝐵 ) )
254 oveq2 ( 𝑥 = 𝑤 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑤 ) )
255 itgeq1 ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑤 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
256 254 255 syl ( 𝑥 = 𝑤 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
257 itgex ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ∈ V
258 256 1 257 fvmpt ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺𝑤 ) = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
259 253 258 syl ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝐺𝑤 ) = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
260 2 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝐴 ∈ ℝ )
261 115 sselda ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℝ )
262 261 3ad2antr2 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑤 ∈ ℝ )
263 115 sselda ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℝ )
264 263 rexrd ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℝ* )
265 264 3ad2antr1 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑢 ∈ ℝ* )
266 elicc1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵 ) ) )
267 133 134 266 syl2anc ( 𝜑 → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵 ) ) )
268 267 biimpa ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵 ) )
269 268 simp2d ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴𝑢 )
270 269 3ad2antr1 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝐴𝑢 )
271 simpr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑢𝑤 )
272 133 adantr ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ* )
273 261 rexrd ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℝ* )
274 elicc1 ( ( 𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ↔ ( 𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤 ) ) )
275 272 273 274 syl2anc ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ↔ ( 𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤 ) ) )
276 275 3ad2antr2 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ↔ ( 𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤 ) ) )
277 265 270 271 276 mpbir3and ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑢 ∈ ( 𝐴 [,] 𝑤 ) )
278 iooss2 ( ( 𝐵 ∈ ℝ*𝑤𝐵 ) → ( 𝐴 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
279 134 142 278 syl2an ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
280 5 adantr ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
281 279 280 sstrd ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑤 ) ⊆ 𝐷 )
282 281 3ad2antr2 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝐴 (,) 𝑤 ) ⊆ 𝐷 )
283 282 sselda ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ) → 𝑡𝐷 )
284 149 adantlr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ 𝑡𝐷 ) → ( 𝐹𝑡 ) ∈ ℂ )
285 283 284 syldan ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ) → ( 𝐹𝑡 ) ∈ ℂ )
286 eleq1w ( 𝑤 = 𝑢 → ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ↔ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) )
287 286 anbi2d ( 𝑤 = 𝑢 → ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
288 oveq2 ( 𝑤 = 𝑢 → ( 𝐴 (,) 𝑤 ) = ( 𝐴 (,) 𝑢 ) )
289 288 mpteq1d ( 𝑤 = 𝑢 → ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹𝑡 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹𝑡 ) ) )
290 289 eleq1d ( 𝑤 = 𝑢 → ( ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 ) )
291 287 290 imbi12d ( 𝑤 = 𝑢 → ( ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 ) ↔ ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 ) ) )
292 ioombl ( 𝐴 (,) 𝑤 ) ∈ dom vol
293 292 a1i ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑤 ) ∈ dom vol )
294 149 adantlr ( ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡𝐷 ) → ( 𝐹𝑡 ) ∈ ℂ )
295 8 feqmptd ( 𝜑𝐹 = ( 𝑡𝐷 ↦ ( 𝐹𝑡 ) ) )
296 295 7 eqeltrrd ( 𝜑 → ( 𝑡𝐷 ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
297 296 adantr ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡𝐷 ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
298 281 293 294 297 iblss ( ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
299 291 298 chvarvv ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
300 299 3ad2antr1 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
301 ioombl ( 𝑢 (,) 𝑤 ) ∈ dom vol
302 301 a1i ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ∈ dom vol )
303 fvexd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡𝐷 ) → ( 𝐹𝑡 ) ∈ V )
304 296 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡𝐷 ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
305 147 302 303 304 iblss ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
306 305 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
307 260 262 277 285 300 306 itgsplitioo ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 = ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) )
308 259 307 eqtrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝐺𝑤 ) = ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) )
309 simpr1 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑢 ∈ ( 𝐴 [,] 𝐵 ) )
310 oveq2 ( 𝑥 = 𝑢 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑢 ) )
311 itgeq1 ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑢 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 )
312 310 311 syl ( 𝑥 = 𝑢 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 )
313 itgex ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 ∈ V
314 312 1 313 fvmpt ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺𝑢 ) = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 )
315 309 314 syl ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( 𝐺𝑢 ) = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 )
316 308 315 oveq12d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) = ( ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 ) )
317 fvexd ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ) → ( 𝐹𝑡 ) ∈ V )
318 317 299 itgcl ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 ∈ ℂ )
319 318 adantrr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 ∈ ℂ )
320 fvexd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹𝑡 ) ∈ V )
321 320 305 itgcl ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ∈ ℂ )
322 319 321 pncan2d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 ) = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
323 322 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹𝑡 ) d 𝑡 ) = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
324 316 323 eqtrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
325 324 fveq2d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) = ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) )
326 df-ov ( 𝑢 (,) 𝑤 ) = ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ )
327 opelxpi ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ⟨ 𝑢 , 𝑤 ⟩ ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) )
328 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
329 ffn ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
330 328 329 ax-mp (,) Fn ( ℝ* × ℝ* )
331 iccssxr ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
332 xpss12 ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ* ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ⊆ ( ℝ* × ℝ* ) )
333 331 331 332 mp2an ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ⊆ ( ℝ* × ℝ* )
334 fnfvima ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ⊆ ( ℝ* × ℝ* ) ∧ ⟨ 𝑢 , 𝑤 ⟩ ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
335 330 333 334 mp3an12 ( ⟨ 𝑢 , 𝑤 ⟩ ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
336 327 335 syl ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
337 326 336 eqeltrid ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑢 (,) 𝑤 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
338 itgeq1 ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ∫ 𝑠 ( 𝐹𝑡 ) d 𝑡 = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 )
339 338 fveq2d ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( abs ‘ ∫ 𝑠 ( 𝐹𝑡 ) d 𝑡 ) = ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) )
340 eleq2 ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( 𝑡𝑠𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) )
341 340 ifbid ( 𝑠 = ( 𝑢 (,) 𝑤 ) → if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) )
342 341 mpteq2dv ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
343 342 fveq2d ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
344 339 343 breq12d ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( ( abs ‘ ∫ 𝑠 ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ) )
345 344 rspccva ( ( ∀ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ( abs ‘ ∫ 𝑠 ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝑠 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∧ ( 𝑢 (,) 𝑤 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
346 9 337 345 syl2an ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
347 346 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
348 325 347 eqbrtrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
349 348 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
350 subcl ( ( ( 𝐺𝑤 ) ∈ ℂ ∧ ( 𝐺𝑢 ) ∈ ℂ ) → ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ∈ ℂ )
351 125 126 350 syl2anr ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ∈ ℂ )
352 351 anandis ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ∈ ℂ )
353 352 abscld ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ )
354 353 rexrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ* )
355 354 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ* )
356 355 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ* )
357 164 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
358 209 ad2antlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → 𝑦 ∈ ℝ* )
359 xrlelttr ( ( ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ* ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ*𝑦 ∈ ℝ* ) → ( ( ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
360 356 357 358 359 syl3anc ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
361 349 360 mpand ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
362 252 361 sylanl1 ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
363 362 adantr ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
364 251 363 mpd ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) ∧ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 )
365 364 ex ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
366 103 113 116 132 365 wlogle ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
367 366 anassrs ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
368 93 367 sylanb ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
369 368 ralrimiva ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
370 breq2 ( 𝑧 = ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) )
371 370 rspceaimv ( ( ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
372 82 369 371 syl2anc ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
373 ralnex ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ¬ 𝑟 ≠ 0 ↔ ¬ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 )
374 nne ( ¬ 𝑟 ≠ 0 ↔ 𝑟 = 0 )
375 374 ralbii ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ¬ 𝑟 ≠ 0 ↔ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 )
376 373 375 bitr3i ( ¬ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ↔ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 )
377 17 ffnd ( 𝑓 ∈ dom ∫1𝑓 Fn ℝ )
378 fnfvelrn ( ( 𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑓𝑡 ) ∈ ran 𝑓 )
379 377 378 sylan ( ( 𝑓 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑓𝑡 ) ∈ ran 𝑓 )
380 elun1 ( ( 𝑓𝑡 ) ∈ ran 𝑓 → ( 𝑓𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
381 379 380 syl ( ( 𝑓 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑓𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
382 eqeq1 ( 𝑟 = ( 𝑓𝑡 ) → ( 𝑟 = 0 ↔ ( 𝑓𝑡 ) = 0 ) )
383 382 rspcva ( ( ( 𝑓𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑓𝑡 ) = 0 )
384 381 383 sylan ( ( ( 𝑓 ∈ dom ∫1𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑓𝑡 ) = 0 )
385 384 adantllr ( ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑓𝑡 ) = 0 )
386 20 ffnd ( 𝑔 ∈ dom ∫1𝑔 Fn ℝ )
387 fnfvelrn ( ( 𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑔𝑡 ) ∈ ran 𝑔 )
388 386 387 sylan ( ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑔𝑡 ) ∈ ran 𝑔 )
389 elun2 ( ( 𝑔𝑡 ) ∈ ran 𝑔 → ( 𝑔𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
390 388 389 syl ( ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) → ( 𝑔𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) )
391 eqeq1 ( 𝑟 = ( 𝑔𝑡 ) → ( 𝑟 = 0 ↔ ( 𝑔𝑡 ) = 0 ) )
392 391 rspcva ( ( ( 𝑔𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑔𝑡 ) = 0 )
393 392 oveq2d ( ( ( 𝑔𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔𝑡 ) ) = ( i · 0 ) )
394 it0e0 ( i · 0 ) = 0
395 393 394 eqtrdi ( ( ( 𝑔𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔𝑡 ) ) = 0 )
396 390 395 sylan ( ( ( 𝑔 ∈ dom ∫1𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔𝑡 ) ) = 0 )
397 396 adantlll ( ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔𝑡 ) ) = 0 )
398 385 397 oveq12d ( ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) = ( 0 + 0 ) )
399 398 an32s ( ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) = ( 0 + 0 ) )
400 00id ( 0 + 0 ) = 0
401 399 400 eqtrdi ( ( ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) = 0 )
402 401 adantlll ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) = 0 )
403 402 oveq2d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) = ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − 0 ) )
404 0cnd ( ( 𝜑 ∧ ¬ 𝑡𝐷 ) → 0 ∈ ℂ )
405 149 404 ifclda ( 𝜑 → if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) ∈ ℂ )
406 405 subid1d ( 𝜑 → ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − 0 ) = if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) )
407 406 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − 0 ) = if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) )
408 403 407 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) = if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) )
409 408 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) = ( abs ‘ if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) ) )
410 fvif ( abs ‘ if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) ) = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , ( abs ‘ 0 ) )
411 abs0 ( abs ‘ 0 ) = 0
412 ifeq2 ( ( abs ‘ 0 ) = 0 → if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , ( abs ‘ 0 ) ) = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) )
413 411 412 ax-mp if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , ( abs ‘ 0 ) ) = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 )
414 410 413 eqtri ( abs ‘ if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) ) = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 )
415 409 414 eqtrdi ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) )
416 415 mpteq2dva ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
417 416 fveq2d ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
418 417 breq1d ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) )
419 418 biimpd ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) )
420 419 ex ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) → ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ) )
421 420 com23 ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ) )
422 421 imp32 ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
423 422 anasss ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
424 423 adantlr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
425 1rp 1 ∈ ℝ+
426 425 ne0ii + ≠ ∅
427 352 anassrs ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ∈ ℂ )
428 427 abscld ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ )
429 428 adantlrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ )
430 429 adantlr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ )
431 rpre ( 𝑦 ∈ ℝ+𝑦 ∈ ℝ )
432 431 rehalfcld ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
433 432 adantl ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ )
434 433 ad3antlr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 / 2 ) ∈ ℝ )
435 431 adantl ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
436 435 ad3antlr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ℝ )
437 430 rexrd ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ∈ ℝ* )
438 157 a1i ( ( 𝜑 ∧ ¬ 𝑡𝐷 ) → 0 ∈ ( 0 [,] +∞ ) )
439 154 438 ifclda ( 𝜑 → if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
440 439 adantr ( ( 𝜑𝑡 ∈ ℝ ) → if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
441 440 fmpttd ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
442 itg2cl ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
443 441 442 syl ( 𝜑 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
444 443 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
445 434 rexrd ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 / 2 ) ∈ ℝ* )
446 109 108 oveqan12rd ( ( 𝑏 = 𝑢𝑎 = 𝑤 ) → ( ( 𝐺𝑎 ) − ( 𝐺𝑏 ) ) = ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) )
447 446 fveq2d ( ( 𝑏 = 𝑢𝑎 = 𝑤 ) → ( abs ‘ ( ( 𝐺𝑎 ) − ( 𝐺𝑏 ) ) ) = ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) )
448 447 breq1d ( ( 𝑏 = 𝑢𝑎 = 𝑤 ) → ( ( abs ‘ ( ( 𝐺𝑎 ) − ( 𝐺𝑏 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ) )
449 99 98 oveqan12rd ( ( 𝑏 = 𝑤𝑎 = 𝑢 ) → ( ( 𝐺𝑎 ) − ( 𝐺𝑏 ) ) = ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) )
450 449 fveq2d ( ( 𝑏 = 𝑤𝑎 = 𝑢 ) → ( abs ‘ ( ( 𝐺𝑎 ) − ( 𝐺𝑏 ) ) ) = ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) )
451 450 breq1d ( ( 𝑏 = 𝑤𝑎 = 𝑢 ) → ( ( abs ‘ ( ( 𝐺𝑎 ) − ( 𝐺𝑏 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ) )
452 129 breq1d ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ( ( 𝐺𝑢 ) − ( 𝐺𝑤 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ) )
453 321 abscld ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ∈ ℝ )
454 453 rexrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ∈ ℝ* )
455 443 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ∈ ℝ* )
456 441 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
457 breq2 ( ( abs ‘ ( 𝐹𝑡 ) ) = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
458 breq2 ( 0 = if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ 0 ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
459 150 leidd ( ( 𝜑𝑡𝐷 ) → ( abs ‘ ( 𝐹𝑡 ) ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) )
460 breq1 ( ( abs ‘ ( 𝐹𝑡 ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) → ( ( abs ‘ ( 𝐹𝑡 ) ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) ) )
461 breq1 ( 0 = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( 𝐹𝑡 ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) ) )
462 460 461 ifboth ( ( ( abs ‘ ( 𝐹𝑡 ) ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) ∧ 0 ≤ ( abs ‘ ( 𝐹𝑡 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) )
463 459 152 462 syl2anc ( ( 𝜑𝑡𝐷 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) )
464 463 adantlr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡𝐷 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹𝑡 ) ) )
465 147 ssneld ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ¬ 𝑡𝐷 → ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) )
466 465 imp ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡𝐷 ) → ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) )
467 226 224 eqbrtrdi ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ 0 )
468 466 467 syl ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡𝐷 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ 0 )
469 457 458 464 468 ifbothda ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) )
470 469 ralrimivw ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) )
471 233 234 ifex if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ V
472 471 a1i ( ( 𝜑𝑡 ∈ ℝ ) → if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ∈ V )
473 eqidd ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
474 232 236 472 240 473 ofrfval2 ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
475 474 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ≤ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
476 470 475 mpbird ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) )
477 itg2le ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
478 161 456 476 477 syl3anc ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
479 454 163 455 346 478 xrletrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
480 479 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
481 325 480 eqbrtrd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢𝑤 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
482 448 451 115 452 481 wlogle ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
483 482 anassrs ( ( ( 𝜑𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
484 483 adantlrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
485 484 adantlr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) )
486 simplr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) )
487 437 444 445 485 486 xrlelttrd ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < ( 𝑦 / 2 ) )
488 rphalflt ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) < 𝑦 )
489 488 adantl ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) < 𝑦 )
490 489 ad3antlr ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 / 2 ) < 𝑦 )
491 430 434 436 487 490 lttrd ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 )
492 491 a1d ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
493 492 ralrimiva ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
494 493 ralrimivw ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
495 r19.2z ( ( ℝ+ ≠ ∅ ∧ ∀ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
496 426 494 495 sylancr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡𝐷 , ( abs ‘ ( 𝐹𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
497 424 496 syldan ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
498 497 anassrs ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
499 498 anassrs ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
500 376 499 sylan2b ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ¬ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
501 372 500 pm2.61dan ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
502 501 ex ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) )
503 502 rexlimdvva ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( ∃ 𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡𝐷 , ( 𝐹𝑡 ) , 0 ) − ( ( 𝑓𝑡 ) + ( i · ( 𝑔𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) )
504 14 503 mpd ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
505 504 ralrimivva ( 𝜑 → ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) )
506 ssid ℂ ⊆ ℂ
507 elcncf2 ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) ) )
508 118 506 507 sylancl ( 𝜑 → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺𝑤 ) − ( 𝐺𝑢 ) ) ) < 𝑦 ) ) ) )
509 10 505 508 mpbir2and ( 𝜑𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )