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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ ℂ )
126 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑢 ) ∈ ℂ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
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 ffvelcdmda ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
173 172 recnd ⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℂ )
174 ax-icn ⊢ i ∈ ℂ
175 20 ffvelcdmda ⊢ ( ( 𝑔 ∈ 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→ ℂ ) )