Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anc Structured version   Visualization version   GIF version

Theorem ftc1anc 35083
 Description: ftc1a 24643 holds for functions that obey the triangle inequality in the absence of ax-cc 9855. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)
Hypotheses
Ref Expression
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
Ref Expression
ftc1anc (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Distinct variable groups:   𝑡,𝑠,𝑥,𝐴   𝐵,𝑠,𝑡,𝑥   𝐷,𝑠,𝑡,𝑥   𝐹,𝑠,𝑡,𝑥   𝜑,𝑠,𝑡,𝑥   𝐺,𝑠
Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anc
Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑟 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ftc1anc.g . . 3 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
2 ftc1anc.a . . 3 (𝜑𝐴 ∈ ℝ)
3 ftc1anc.b . . 3 (𝜑𝐵 ∈ ℝ)
4 ftc1anc.le . . 3 (𝜑𝐴𝐵)
5 ftc1anc.s . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
6 ftc1anc.d . . 3 (𝜑𝐷 ⊆ ℝ)
7 ftc1anc.i . . 3 (𝜑𝐹 ∈ 𝐿1)
8 ftc1anc.f . . 3 (𝜑𝐹:𝐷⟶ℂ)
91, 2, 3, 4, 5, 6, 7, 8ftc1lem2 24642 . 2 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
10 rphalfcl 12413 . . . . . 6 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
111, 2, 3, 4, 5, 6, 7, 8ftc1anclem6 35080 . . . . . 6 ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1210, 11sylan2 595 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1312adantrl 715 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1410ad2antll 728 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈ ℝ+)
15 2rp 12391 . . . . . . . . . . . 12 2 ∈ ℝ+
16 i1ff 24283 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
1716frnd 6510 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
1817adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
19 i1ff 24283 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
2019frnd 6510 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
2120adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
2218, 21unssd 4148 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
23 ax-resscn 10592 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
2422, 23sstrdi 3965 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
25 i1f0rn 24289 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
26 elun1 4138 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
2725, 26syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
2827adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
29 absf 14697 . . . . . . . . . . . . . . . . . . 19 abs:ℂ⟶ℝ
30 ffn 6503 . . . . . . . . . . . . . . . . . . 19 (abs:ℂ⟶ℝ → abs Fn ℂ)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . . 18 abs Fn ℂ
32 fnfvima 6987 . . . . . . . . . . . . . . . . . 18 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3331, 32mp3an1 1445 . . . . . . . . . . . . . . . . 17 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3424, 28, 33syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3534ne0d 4284 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
36 imassrn 5927 . . . . . . . . . . . . . . . . 17 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
37 frn 6509 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
3829, 37ax-mp 5 . . . . . . . . . . . . . . . . 17 ran abs ⊆ ℝ
3936, 38sstri 3962 . . . . . . . . . . . . . . . 16 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
40 ffun 6506 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → Fun abs)
4129, 40ax-mp 5 . . . . . . . . . . . . . . . . 17 Fun abs
42 i1frn 24284 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
43 i1frn 24284 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
44 unfi 8782 . . . . . . . . . . . . . . . . . 18 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
4542, 43, 44syl2an 598 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
46 imafi 8814 . . . . . . . . . . . . . . . . 17 ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
4741, 45, 46sylancr 590 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
48 fimaxre2 11583 . . . . . . . . . . . . . . . 16 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
4939, 47, 48sylancr 590 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
50 suprcl 11597 . . . . . . . . . . . . . . . 16 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5139, 50mp3an1 1445 . . . . . . . . . . . . . . 15 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5235, 49, 51syl2anc 587 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5352adantr 484 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
54 0red 10642 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
5524sselda 3953 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
5655abscld 14796 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
5756adantrr 716 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
5852adantr 484 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
59 absgt0 14684 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
6055, 59syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
6160biimpd 232 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 → 0 < (abs‘𝑟)))
6261impr 458 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟))
6339a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ)
6463, 35, 493jca 1125 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
6564adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
66 fnfvima 6987 . . . . . . . . . . . . . . . . . . . 20 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
6731, 66mp3an1 1445 . . . . . . . . . . . . . . . . . . 19 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
6824, 67sylan 583 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
69 suprub 11598 . . . . . . . . . . . . . . . . . 18 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7065, 68, 69syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7170adantrr 716 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7254, 57, 58, 62, 71ltletrd 10798 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7372rexlimdvaa 3277 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
7473imp 410 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7553, 74elrpd 12425 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76 rpmulcl 12409 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
7715, 75, 76sylancr 590 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78 rpdivcl 12411 . . . . . . . . . . 11 (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
7914, 77, 78syl2an 598 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8079anassrs 471 . . . . . . . . 9 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8180adantlr 714 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82 ancom 464 . . . . . . . . . . . 12 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+𝑢 ∈ (𝐴[,]𝐵)))
8382anbi2i 625 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 ∈ 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) ∧ (𝑦 ∈ ℝ+𝑢 ∈ (𝐴[,]𝐵))))
84 an32 645 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8584anbi1i 626 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)))
86 an32 645 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8785, 86bitri 278 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8887anbi1i 626 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ 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))
89 an32 645 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ 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) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
9088, 89bitri 278 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ 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 anass 472 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑓 ∈ 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) ∧ (𝑦 ∈ ℝ+𝑢 ∈ (𝐴[,]𝐵))))
9283, 90, 913bitr4i 306 . . . . . . . . . 10 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ 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 oveq12 7158 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑤𝑎 = 𝑢) → (𝑏𝑎) = (𝑤𝑢))
9493ancoms 462 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑢𝑏 = 𝑤) → (𝑏𝑎) = (𝑤𝑢))
9594fveq2d 6665 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑤) → (abs‘(𝑏𝑎)) = (abs‘(𝑤𝑢)))
9695breq1d 5062 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑤) → ((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
97 fveq2 6661 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (𝐺𝑏) = (𝐺𝑤))
98 fveq2 6661 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑢 → (𝐺𝑎) = (𝐺𝑢))
9997, 98oveqan12rd 7169 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑢𝑏 = 𝑤) → ((𝐺𝑏) − (𝐺𝑎)) = ((𝐺𝑤) − (𝐺𝑢)))
10099fveq2d 6665 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑤) → (abs‘((𝐺𝑏) − (𝐺𝑎))) = (abs‘((𝐺𝑤) − (𝐺𝑢))))
101100breq1d 5062 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑤) → ((abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦 ↔ (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
10296, 101imbi12d 348 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑤) → (((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦) ↔ ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
103 oveq12 7158 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑢𝑎 = 𝑤) → (𝑏𝑎) = (𝑢𝑤))
104103ancoms 462 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑤𝑏 = 𝑢) → (𝑏𝑎) = (𝑢𝑤))
105104fveq2d 6665 . . . . . . . . . . . . . 14 ((𝑎 = 𝑤𝑏 = 𝑢) → (abs‘(𝑏𝑎)) = (abs‘(𝑢𝑤)))
106105breq1d 5062 . . . . . . . . . . . . 13 ((𝑎 = 𝑤𝑏 = 𝑢) → ((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
107 fveq2 6661 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑢 → (𝐺𝑏) = (𝐺𝑢))
108 fveq2 6661 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → (𝐺𝑎) = (𝐺𝑤))
109107, 108oveqan12rd 7169 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑤𝑏 = 𝑢) → ((𝐺𝑏) − (𝐺𝑎)) = ((𝐺𝑢) − (𝐺𝑤)))
110109fveq2d 6665 . . . . . . . . . . . . . 14 ((𝑎 = 𝑤𝑏 = 𝑢) → (abs‘((𝐺𝑏) − (𝐺𝑎))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
111110breq1d 5062 . . . . . . . . . . . . 13 ((𝑎 = 𝑤𝑏 = 𝑢) → ((abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦 ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦))
112106, 111imbi12d 348 . . . . . . . . . . . 12 ((𝑎 = 𝑤𝑏 = 𝑢) → (((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦) ↔ ((abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
113 iccssre 12816 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
1142, 3, 113syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
115114ad4antr 731 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ)
116 simp-4l 782 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
117114, 23sstrdi 3965 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
118117sselda 3953 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
119117sselda 3953 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
120 abssub 14686 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
121118, 119, 120syl2anr 599 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
122121anandis 677 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
123122breq1d 5062 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
1249ffvelrnda 6842 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐺𝑤) ∈ ℂ)
1259ffvelrnda 6842 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐺𝑢) ∈ ℂ)
126 abssub 14686 . . . . . . . . . . . . . . . . 17 (((𝐺𝑤) ∈ ℂ ∧ (𝐺𝑢) ∈ ℂ) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
127124, 125, 126syl2anr 599 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
128127anandis 677 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
129128breq1d 5062 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦 ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦))
130123, 129imbi12d 348 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦) ↔ ((abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
131116, 130sylan 583 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑓 ∈ 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‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
1322rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℝ*)
1333rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐵 ∈ ℝ*)
134132, 133jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
135 df-icc 12742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥𝑡𝑡𝑦)})
136135elixx3g 12748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑢 ∈ ℝ*) ∧ (𝐴𝑢𝑢𝐵)))
137136simprbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 ∈ (𝐴[,]𝐵) → (𝐴𝑢𝑢𝐵))
138137simpld 498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ∈ (𝐴[,]𝐵) → 𝐴𝑢)
139135elixx3g 12748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐴𝑤𝑤𝐵)))
140139simprbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (𝐴[,]𝐵) → (𝐴𝑤𝑤𝐵))
141140simprd 499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ (𝐴[,]𝐵) → 𝑤𝐵)
142138, 141anim12i 615 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴𝑢𝑤𝐵))
143 ioossioo 12828 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑢𝑤𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
144134, 142, 143syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
1455adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
146144, 145sstrd 3963 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
147146sselda 3953 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
1488ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
149148abscld 14796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ ℝ)
150149rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ ℝ*)
151148absge0d 14804 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡𝐷) → 0 ≤ (abs‘(𝐹𝑡)))
152 elxrge0 12844 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((abs‘(𝐹𝑡)) ∈ (0[,]+∞) ↔ ((abs‘(𝐹𝑡)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐹𝑡))))
153150, 151, 152sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
154153adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
155147, 154syldan 594 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
156 0e0iccpnf 12846 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ (0[,]+∞)
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
158155, 157ifclda 4484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
159158adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
160159fmpttd 6870 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
161 itg2cl 24339 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
1631623adantr3 1168 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
164116, 163sylan 583 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
165164adantr 484 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
166 simplll 774 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
167148adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
168147, 167syldan 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
169168adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
170 elioore 12765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
17116ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
172171recnd 10667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
173 ax-icn 10594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 i ∈ ℂ
17419ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
175174recnd 10667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
176 mulcl 10619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
177173, 175, 176sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
178 addcl 10617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
179172, 177, 178syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
180179anandirs 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
181170, 180sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
182181adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
183182adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
184169, 183subcld 10995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
185184abscld 14796 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
186181abscld 14796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
187186adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
188187adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
189185, 188readdcld 10668 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
190189rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
191184absge0d 14804 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
192180absge0d 14804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
193170, 192sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
194193adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
195194adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
196185, 188, 191, 195addge0d 11214 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
197 elxrge0 12844 . . . . . . . . . . . . . . . . . . . . . . 23 (((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ (((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))))
198190, 196, 197sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
199156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
200198, 199ifclda 4484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
201200adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
202201fmpttd 6870 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
203 itg2cl 24339 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
204202, 203syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
2052043adantr3 1168 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
206166, 205sylan 583 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
207206adantr 484 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ 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))) ∈ ℝ*)
208 rpxr 12395 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
209208ad3antlr 730 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → 𝑦 ∈ ℝ*)
210158adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
211210adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
212211fmpttd 6870 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
213169, 183npcand 10999 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡)))) = (𝐹𝑡))
214213fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘(𝐹𝑡)))
215184, 183abstrid 14816 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
216214, 215eqbrtrrd 5076 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹𝑡)) ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
217 iftrue 4456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = (abs‘(𝐹𝑡)))
218217adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = (abs‘(𝐹𝑡)))
219 iftrue 4456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
220219adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
221216, 218, 2203brtr4d 5084 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
222221ex 416 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
223 0le0 11735 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
225 iffalse 4459 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = 0)
226 iffalse 4459 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = 0)
227224, 225, 2263brtr4d 5084 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
228222, 227pm2.61d1 183 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
229228ralrimivw 3178 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
230 reex 10626 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ℝ ∈ V)
232 fvex 6674 . . . . . . . . . . . . . . . . . . . . . . . 24 (abs‘(𝐹𝑡)) ∈ V
233 c0ex 10633 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
234232, 233ifex 4498 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ V
235234a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ V)
236 ovex 7182 . . . . . . . . . . . . . . . . . . . . . . . 24 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V
237236, 233ifex 4498 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V)
239 eqidd 2825 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))
240 eqidd 2825 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
241231, 235, 238, 239, 240ofrfval2 7421 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
242241ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
243229, 242mpbird 260 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
244 itg2le 24346 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ 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))))
245212, 202, 243, 244syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
2462453adantr3 1168 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
247166, 246sylan 583 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
248247adantr 484 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ 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))))
2491, 2, 3, 4, 5, 6, 7, 8ftc1anclem8 35082 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ 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))) < 𝑦)
250165, 207, 209, 248, 249xrlelttrd 12550 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦)
251 simplll 774 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑)
252 simpr2 1192 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑤 ∈ (𝐴[,]𝐵))
253 oveq2 7157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤))
254 itgeq1 24379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
255253, 254syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
256 itgex 24377 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡 ∈ V
257255, 1, 256fvmpt 6759 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (𝐴[,]𝐵) → (𝐺𝑤) = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
258252, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑤) = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
2592adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝐴 ∈ ℝ)
260114sselda 3953 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ)
2612603ad2antr2 1186 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑤 ∈ ℝ)
262114sselda 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ)
263262rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*)
2642633ad2antr1 1185 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ ℝ*)
265 elicc1 12779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵)))
266132, 133, 265syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵)))
267266biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵))
268267simp2d 1140 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝐴𝑢)
2692683ad2antr1 1185 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝐴𝑢)
270 simpr3 1193 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢𝑤)
271132adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
272260rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*)
273 elicc1 12779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
274271, 272, 273syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
2752743ad2antr2 1186 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
276264, 269, 270, 275mpbir3and 1339 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ (𝐴[,]𝑤))
277 iooss2 12771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ ℝ*𝑤𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
278133, 141, 277syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
2795adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷)
280278, 279sstrd 3963 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷)
2812803ad2antr2 1186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷)
282281sselda 3953 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡𝐷)
283148adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
284282, 283syldan 594 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
285 eleq1w 2898 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵)))
286285anbi2d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑢 → ((𝜑𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑢 ∈ (𝐴[,]𝐵))))
287 oveq2 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢))
288287mpteq1d 5141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)))
289288eleq1d 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1))
290286, 289imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑢 → (((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1) ↔ ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)))
291 ioombl 24172 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝑤) ∈ dom vol
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol)
293148adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
2948feqmptd 6724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
295294, 7eqeltrrd 2917 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
296295adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
297280, 292, 293, 296iblss 24411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
298290, 297chvarvv 2006 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)
2992983ad2antr1 1185 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)
300 ioombl 24172 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢(,)𝑤) ∈ dom vol
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol)
302 fvexd 6676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ V)
303295adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
304146, 301, 302, 303iblss 24411 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
3053043adantr3 1168 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
306259, 261, 276, 284, 299, 305itgsplitioo 24444 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
307258, 306eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑤) = (∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
308 simpr1 1191 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ (𝐴[,]𝐵))
309 oveq2 7157 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢))
310 itgeq1 24379 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
311309, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
312 itgex 24377 . . . . . . . . . . . . . . . . . . . . . . . 24 ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ V
313311, 1, 312fvmpt 6759 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ (𝐴[,]𝐵) → (𝐺𝑢) = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
314308, 313syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑢) = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
315307, 314oveq12d 7167 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((𝐺𝑤) − (𝐺𝑢)) = ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡))
316 fvexd 6676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹𝑡) ∈ V)
317316, 298itgcl 24390 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ ℂ)
318317adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ ℂ)
319 fvexd 6676 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ V)
320319, 304itgcl 24390 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡 ∈ ℂ)
321318, 320pncan2d 10997 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
3223213adantr3 1168 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
323315, 322eqtrd 2859 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((𝐺𝑤) − (𝐺𝑢)) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
324323fveq2d 6665 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
325 ftc1anc.t . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))))
326 df-ov 7152 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
327 opelxpi 5579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))
328 ioof 12834 . . . . . . . . . . . . . . . . . . . . . . . . 25 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
329 ffn 6503 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
330328, 329ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (,) Fn (ℝ* × ℝ*)
331 iccssxr 12817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴[,]𝐵) ⊆ ℝ*
332 xpss12 5557 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) → ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*))
333331, 331, 332mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*)
334 fnfvima 6987 . . . . . . . . . . . . . . . . . . . . . . . 24 (((,) Fn (ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*) ∧ ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
335330, 333, 334mp3an12 1448 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
336327, 335syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
337326, 336eqeltrid 2920 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
338 itgeq1 24379 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
339338fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
340 eleq2 2904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑢(,)𝑤) → (𝑡𝑠𝑡 ∈ (𝑢(,)𝑤)))
341340ifbid 4472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑢(,)𝑤) → if(𝑡𝑠, (abs‘(𝐹𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))
342341mpteq2dv 5148 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))
343342fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
344339, 343breq12d 5065 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))))
345344rspccva 3608 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
346325, 337, 345syl2an 598 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
3473463adantr3 1168 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
348324, 347eqbrtrd 5074 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
349348adantlr 714 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
350 subcl 10883 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺𝑤) ∈ ℂ ∧ (𝐺𝑢) ∈ ℂ) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
351124, 125, 350syl2anr 599 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
352351anandis 677 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
353352abscld 14796 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
354353rexrd 10689 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
3553543adantr3 1168 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
356355adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
357163adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
358208ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑦 ∈ ℝ*)
359 xrlelttr 12546 . . . . . . . . . . . . . . . . . 18 (((abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ* ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*𝑦 ∈ ℝ*) → (((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
360356, 357, 358, 359syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
361349, 360mpand 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
362251, 361sylanl1 679 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
363362adantr 484 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ (𝑓 ∈ 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‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
364250, 363mpd 15 . . . . . . . . . . . . 13 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)
365364ex 416 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
366102, 112, 115, 131, 365wlogle 11171 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
367366anassrs 471 . . . . . . . . . 10 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
36892, 367sylanb 584 . . . . . . . . 9 ((((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
369368ralrimiva 3177 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
370 breq2 5056 . . . . . . . . 9 (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → ((abs‘(𝑤𝑢)) < 𝑧 ↔ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
371370rspceaimv 3614 . . . . . . . 8 ((((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
37281, 369, 371syl2anc 587 . . . . . . 7 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
373 ralnex 3230 . . . . . . . . 9 (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)
374 nne 3018 . . . . . . . . . 10 𝑟 ≠ 0 ↔ 𝑟 = 0)
375374ralbii 3160 . . . . . . . . 9 (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
376373, 375bitr3i 280 . . . . . . . 8 (¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
37716ffnd 6504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 ∈ dom ∫1𝑓 Fn ℝ)
378 fnfvelrn 6839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
379377, 378sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
380 elun1 4138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑡) ∈ ran 𝑓 → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
382 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑓𝑡) → (𝑟 = 0 ↔ (𝑓𝑡) = 0))
383382rspcva 3607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
384381, 383sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
385384adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
38619ffnd 6504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
387 fnfvelrn 6839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
388386, 387sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
389 elun2 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑡) ∈ ran 𝑔 → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
390388, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
391 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑔𝑡) → (𝑟 = 0 ↔ (𝑔𝑡) = 0))
392391rspcva 3607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔𝑡) = 0)
393392oveq2d 7165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = (i · 0))
394 it0e0 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (i · 0) = 0
395393, 394syl6eq 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
396390, 395sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
397396adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
398385, 397oveq12d 7167 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓𝑡) + (i · (𝑔𝑡))) = (0 + 0))
399398an32s 651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = (0 + 0))
400 00id 10813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 + 0) = 0
401399, 400syl6eq 2875 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = 0)
402401adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = 0)
403402oveq2d 7165 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (if(𝑡𝐷, (𝐹𝑡), 0) − 0))
404 0cnd 10632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
405148, 404ifclda 4484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
406405subid1d 10984 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (if(𝑡𝐷, (𝐹𝑡), 0) − 0) = if(𝑡𝐷, (𝐹𝑡), 0))
407406ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − 0) = if(𝑡𝐷, (𝐹𝑡), 0))
408403, 407eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = if(𝑡𝐷, (𝐹𝑡), 0))
409408fveq2d 6665 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘if(𝑡𝐷, (𝐹𝑡), 0)))
410 fvif 6677 . . . . . . . . . . . . . . . . . . . . . 22 (abs‘if(𝑡𝐷, (𝐹𝑡), 0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), (abs‘0))
411 abs0 14645 . . . . . . . . . . . . . . . . . . . . . . 23 (abs‘0) = 0
412 ifeq2 4455 . . . . . . . . . . . . . . . . . . . . . . 23 ((abs‘0) = 0 → if(𝑡𝐷, (abs‘(𝐹𝑡)), (abs‘0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
413411, 412ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑡𝐷, (abs‘(𝐹𝑡)), (abs‘0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)
414410, 413eqtri 2847 . . . . . . . . . . . . . . . . . . . . 21 (abs‘if(𝑡𝐷, (𝐹𝑡), 0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)
415409, 414syl6eq 2875 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
416415mpteq2dva 5147 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
417416fveq2d 6665 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
418417breq1d 5062 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)))
419418biimpd 232 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)))
420419ex 416 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))))
421420com23 86 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))))
422421imp32 422 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
423422anasss 470 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
424423adantlr 714 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
425 1rp 12390 . . . . . . . . . . . . 13 1 ∈ ℝ+
426425ne0ii 4286 . . . . . . . . . . . 12 + ≠ ∅
427352anassrs 471 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
428427abscld 14796 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
429428adantlrr 720 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
430429adantlr 714 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
431 rpre 12394 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
432431rehalfcld 11881 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
433432adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434433ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ)
435431adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
436435ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
437430rexrd 10689 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
438156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ (0[,]+∞))
439153, 438ifclda 4484 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
440439adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
441440fmpttd 6870 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
442 itg2cl 24339 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
443441, 442syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
444443ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
445434rexrd 10689 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ*)
446108, 107oveqan12rd 7169 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑢𝑎 = 𝑤) → ((𝐺𝑎) − (𝐺𝑏)) = ((𝐺𝑤) − (𝐺𝑢)))
447446fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑢𝑎 = 𝑤) → (abs‘((𝐺𝑎) − (𝐺𝑏))) = (abs‘((𝐺𝑤) − (𝐺𝑢))))
448447breq1d 5062 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑢𝑎 = 𝑤) → ((abs‘((𝐺𝑎) − (𝐺𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
44998, 97oveqan12rd 7169 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑤𝑎 = 𝑢) → ((𝐺𝑎) − (𝐺𝑏)) = ((𝐺𝑢) − (𝐺𝑤)))
450449fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑤𝑎 = 𝑢) → (abs‘((𝐺𝑎) − (𝐺𝑏))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
451450breq1d 5062 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑤𝑎 = 𝑢) → ((abs‘((𝐺𝑎) − (𝐺𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
452128breq1d 5062 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
453320abscld 14796 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ∈ ℝ)
454453rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ∈ ℝ*)
455443adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
456441adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
457 breq2 5056 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((abs‘(𝐹𝑡)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
458 breq2 5056 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
459149leidd 11204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)))
460 breq1 5055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((abs‘(𝐹𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) → ((abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡))))
461 breq1 5055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) → (0 ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡))))
462460, 461ifboth 4488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)) ∧ 0 ≤ (abs‘(𝐹𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
463459, 151, 462syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
464463adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
465146ssneld 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤)))
466465imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
467225, 223eqbrtrdi 5091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0)
468466, 467syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0)
469457, 458, 464, 468ifbothda 4487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
470469ralrimivw 3178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
471232, 233ifex 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ V
472471a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ V)
473 eqidd 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
474231, 235, 472, 239, 473ofrfval2 7421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
475474adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
476470, 475mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
477 itg2le 24346 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
478160, 456, 476, 477syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
479454, 162, 455, 346, 478xrletrd 12552 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
4804793adantr3 1168 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
481324, 480eqbrtrd 5074 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
482448, 451, 114, 452, 481wlogle 11171 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
483482anassrs 471 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
484483adantlrr 720 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
485484adantlr 714 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
486 simplr 768 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
487437, 444, 445, 485, 486xrlelttrd 12550 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < (𝑦 / 2))
488 rphalflt 12415 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
489488adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦)
490489ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦)
491430, 434, 436, 487, 490lttrd 10799 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)
492491a1d 25 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
493492ralrimiva 3177 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
494493ralrimivw 3178 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
495 r19.2z 4423 . . . . . . . . . . . 12 ((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
496426, 494, 495sylancr 590 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
497424, 496syldan 594 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
498497anassrs 471 . . . . . . . . 9 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
499498anassrs 471 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
500376, 499sylan2b 596 . . . . . . 7 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
501372, 500pm2.61dan 812 . . . . . 6 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
502501ex 416 . . . . 5 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
503502rexlimdvva 3286 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
50413, 503mpd 15 . . 3 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
505504ralrimivva 3186 . 2 (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
506 ssid 3975 . . 3 ℂ ⊆ ℂ
507 elcncf2 23498 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))))
508117, 506, 507sylancl 589 . 2 (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))))
5099, 505, 508mpbir2and 712 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ∪ cun 3917   ⊆ wss 3919  ∅c0 4276  ifcif 4450  𝒫 cpw 4522  ⟨cop 4556   class class class wbr 5052   ↦ cmpt 5132   × cxp 5540  dom cdm 5542  ran crn 5543   “ cima 5545  Fun wfun 6337   Fn wfn 6338  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149   ∘r cofr 7402  Fincfn 8505  supcsup 8901  ℂcc 10533  ℝcr 10534  0cc0 10535  1c1 10536  ici 10537   + caddc 10538   · cmul 10540  +∞cpnf 10670  ℝ*cxr 10672   < clt 10673   ≤ cle 10674   − cmin 10868   / cdiv 11295  2c2 11689  ℝ+crp 12386  (,)cioo 12735  [,]cicc 12738  abscabs 14593  –cn→ccncf 23484  volcvol 24070  ∫1citg1 24222  ∫2citg2 24223  𝐿1cibl 24224  ∫citg 24225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-symdif 4204  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-n0 11895  df-z 11979  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-rlim 14846  df-sum 15043  df-rest 16696  df-topgen 16717  df-psmet 20537  df-xmet 20538  df-met 20539  df-bl 20540  df-mopn 20541  df-top 21502  df-topon 21519  df-bases 21554  df-cmp 21995  df-cncf 23486  df-ovol 24071  df-vol 24072  df-mbf 24226  df-itg1 24227  df-itg2 24228  df-ibl 24229  df-itg 24230  df-0p 24277 This theorem is referenced by:  ftc2nc  35084
 Copyright terms: Public domain W3C validator